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

自然语言软件需求通常是含糊不清、不一致且不明确的；在安全关键领域，这些缺陷会传播到验证错误规范的正式模型中，并传播到带来不安全行为的实现中。我们证明，配备 SMT 求解器的 大语言模型 可以审核此类需求：将它们转换为形式逻辑，通过生成的形式化中的随机变化检测歧义，并通过求解器查询结果规范来暴露不一致、空洞和安全违规。我们提出了 VERIMED，这是一种神经符号管道，可将这一想法应用于医疗设备软件需求，并报告了两项发现。首先，独立形式化之间的随机变化是一个模糊信号：承认多种看似合理的解释的要求会产生 SMT 不等价的形式化，而双向 SMT 等价检查将这种分歧转变为求解器可检查的测试。其次，符号反馈的有用性取决于其粒度：在血液透析问答基准的反例引导修复中，具体的 SMT 反例将验证的准确性从 55.4% 提高到 98.5%。通过对开源血液透析安全要求的广泛实验评估，我们表明 VERIMED 中基于 LLM 的方法成功减少了对歧义敏感的要求，并通过基于 SMT 的查询实现了对软件要求的严格审核。