神经形式验证：与代理语言无关的形式程序推理

形式验证为软件提供了最强的正确性保证，而验证感知语言可以生成可靠的、经过机器检查的证明。最近的人工智能 编码智能体 大大降低了构建此类证明的成本。然而，很少有主流开发人员受益：大多数使用没有形式验证支持的语言，并且形式化属性和建模执行环境需要形式化方法的专业知识。因此，证明仍然保留给一些值得注意的工件，而生产软件主要通过审查和测试来证明。我们引入了神经形式验证（NFV），它将这种自动化引入了主流语言。 AI 编码智能体 将源级验证问题形式化为验证感知语言的证明义务，由已建立的声音验证器在代理证明搜索的帮助下完成。分阶段的、目标盲目的转换降低了证明工件不能忠实地代表源程序、属性或环境的风险。由于 NFV 无法确保这种形式化的健全性，因此它针对经验准确性而不是端到端健全性进行优化，同时坚持为每个判决提供机器检查的证据。在正确和有缺陷的 Python 解决方案的平衡数据集上对当前前沿模型进行的实验证明了我们方法的有效性。 NFV 与 Dafny 正确解析了 57% 的条目，其判决精度为 92%；借助 CBMC 后端，它可以以 90% 的精度为 63% 的错误程序生成反例。相比之下，LLM 作为判断基线仅达到 72% 的精度，同时在没有任何可检查工件的情况下回答每个条目，而未分阶段的代理-验证器组合证明了 98% 的正确程序和已知错误的程序，仅产生 50% 的精度。他们共同证实，证明和分阶段都有利于人工智能代理的正式程序推理。