自然语言软件需求的神经符号审计

自然语言软件需求经常含糊、不一致和不完整；在安全关键领域，这些缺陷会导致形式模型验证错误的规范，并导致实现出 unsafe behavior。我们展示了大型语言模型配合SMT求解器可用于审计此类需求：将其翻译为形式逻辑，通过对生成的形式化进行随机变异检测模糊性，并通过求解器查询暴露不一致性、空洞性和安全违规。我们提出VERIMED，一个神经符号管道，用于针对医疗器械软件需求实现此想法，并报告了两个发现。首先，独立形式化之间的随机变异是模糊性的信号： admitting multiple plausible interpretations的需求会产生SMT不等价的形式化，双向SMT等价性检查将这种 disagreement转化为可由求解器检查的测试。其次，符号反馈的有用性取决于其细粒度：在hemodialysis问答基准的counterexample引导式修复中，具体的SMT counterexample将准确率从55.4%提高到98.5%。在对开源hemodialysis安全需求的广泛实验评估中，我们表明VERIMED中基于LLM的method成功减少了敏感于模糊性的需求，并通过SMT查询实现对软件需求的严格审计。