Neurosymbolic Auditing of Natural-Language Software Requirements
本文介绍了 VERIMED，这是一种神经符号流水线，它利用大型语言模型和 SMT 求解器来审计自然语言软件需求，通过随机形式化变体检测歧义，并通过反例引导的修复验证一致性和安全性，从而在医疗器械安全需求方面实现了显著的准确率提升。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你是一位生命拯救机器的架构师，比如一台为患者净化血液的透析设备。你用通俗易懂的英语写下这台机器应遵循的行为规则：“如果血流停止，则发出警报。”
问题在于，人类语言是混乱的。词语可能含糊不清，句子可能相互矛盾，或者某条规则可能在无人察觉的情况下根本无法执行。如果计算机程序试图根据你这些混乱的笔记来构建这台机器，它可能会造出一个在纸面上看起来完美、但在现实中却极其危险的装置。
本文介绍了一种名为VERIMED的新型“神经符号”系统（这是一个时髦的术语，指创意人工智能与严格逻辑机器人之间的协作），旨在充当这些安全规则的超级审计员。
以下是 VERIMED 的工作原理，通过日常类比进行解释：
1. 翻译官与逻辑机器人
可以将该系统想象为包含两个部分：
- 翻译官（大语言模型 LLM）： 这是一位富有创意的人工智能，它阅读你的英语规则，并尝试将其翻译成计算机可验证的严格数学语言（SMT）。
- 逻辑机器人（SMT 求解器）： 这是一台僵化、不可动摇的机器，负责检查数学逻辑。它不在乎“情感”或“意图”，只关心规则在逻辑上是否成立。
2. 规则的“压力测试”
在机器被建造之前，VERIMED 会对翻译后的规则运行四项具体测试，以发现隐藏的缺陷：
- “它能发生吗？”测试（空洞性）： 想象一条规则说：“如果机器被淹没在水中，则切断电源。”如果这台机器绝不应该被淹没在水中，那么这条规则就是无用的。逻辑机器人会检查：“机器被淹没在水中实际上可能发生吗？”如果答案是“不”，机器人就会将该规则标记为“幽灵”——它存在，但从未产生任何作用。
- “它能被破坏吗？”测试（可违反性）： 机器人试图破坏规则。它会问：“我能否让机器在遵守规则的同时，做出不安全的事情？”如果它找到了破坏安全的方法，它会向你展示具体路径（即“反例”），就像一份证明，上面写着：“看？如果你将旋钮调至 50，警报就不会响起，尽管你说过它应该响起。”
- “重复记账”测试（冗余性）： 有时，你会写下两条表达完全相同意思的规则。一条可能是：“不要让压力超过 200"，另一条说：“不要让压力超过 200"。机器人会发现这些重复项，并指出：“你在重复自己。你是打算保留两条，还是其中一条有误？”
- “全局和谐”测试（一致性）： 机器人检查所有规则是否相互冲突。如果规则 A 说“启动泵”，而规则 B 说“泵必须关闭”，且这两者本应同时发生，机器人就会大喊：“这不可能！”
3. “歧义检测器”（魔法技巧）
这是本文最具创意的想法。有时，一个句子如此模糊，以至于可以有两种不同的解释。
- 类比： 想象你告诉厨师：“把牛排煮到‘熟’为止。”厨师可能认为“熟”是指三分熟，而你指的是全熟。
- VERIMED 如何捕捉这一点： 它不是让 AI 只翻译一次规则，而是让 AI 将同一条规则翻译五次，就像让五位不同的厨师来解读“熟”一样。
- 如果五位厨师写下的食谱完全一致，那么这条规则就是清晰的。
- 如果一位厨师写下“三分熟”，而另一位写下“全熟”，系统就会察觉这种分歧。随后它会向人类指出：“嘿，你的规则有歧义！你的这句话可能有两种不同的解读方式。请予以澄清。”
4. “维修车间”
当逻辑机器人发现错误或歧义时，它不会只说“错误”。它会像一位乐于助人的机械师那样行动：
- 针对逻辑错误： 它会向 AI 展示规则失败的具体场景（即反例）。AI 随后会重写规则，以修补那个特定的漏洞。
- 针对模糊语言： 它会向人类展示具体的困惑点（例如："200 度是包含在内还是排除在外？”）。人类进行澄清，系统重新翻译，直到所有人达成一致。
他们发现了什么？
研究人员在透析机器的 64 条安全规则集上测试了该系统。
- 结果： 系统发现 2 条规则是冗余的（重复的），12 条规则存在歧义（可以有多种解读方式）。
- 修复： 当他们使用“反例”反馈（向 AI 展示它具体是如何失败的）时，AI 回答安全问题的能力从约55% 的准确率跃升至近 99%。
- 歧义修复： 在系统标记出模糊规则并由人类澄清之后，AI 不再产生相互冲突的翻译。“歧义”降至零。
核心结论
VERIMED 是一张安全网。它利用富有创意的人工智能将人类规则翻译成数学，并利用僵化的逻辑机器人来检查这些数学规则是否一致、无歧义且真正安全。它不仅检查代码是否运行，更在机器被建造之前，检查代码的指令是否合理。
重要提示： 论文明确指出，该系统是在医疗设备要求（透析机）和疼痛管理泵的测试中进行的。作者警告，该系统是供专家审查要求的工具，而非人类专家的替代品，在没有独立人工审查的情况下，不应将其用于现实生活。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。