神经形式化验证：智能体的语言无关形式化程序推理
Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
浏览论文内容
中文总结 AI 辅助
该研究提出神经形式化验证（NFV），让AI编码智能体与成熟验证器结合，为主流语言开发者实现一键式程序验证，在Python编程问题数据集上取得了良好的验证效果。
中文摘要 AI 辅助
形式化验证为软件提供了现有最强的保证，支持验证的语言已使其自动化成为现实。然而，这种好处惠及的主流开发者很少，他们使用的大多数语言都没有验证支持。此外，指定属性和对环境建模需要形式化方法专业知识，因此证明仅保留给少数知名制品，而发布的生产代码仅通过审查和测试得到验证。我们引入神经形式化验证（NFV），将这种自动化用于主流编程语言的开发者：AI编码智能体进行翻译，成熟的验证器做出判断，用主流语言提出的问题可一键得到答案，基于经验准确率而非可靠性，附带机器检查的证明。在包含Python编程问题正确与错误解答的数据集上的结果令人鼓舞：NFV为57%的条目返回了Dafny正确性证明或错误证明，精度达92%；为63%的有错误程序返回了CBMC反例，精度达90%。
英文摘要
Formal verification provides the strongest correctness guarantees for software, and verification-aware languages can produce sound, machine-checked proofs. Recent AI coding agents have sharply lowered the cost of constructing such proofs. Yet few mainstream developers benefit: most use languages without formal-verification support, and formalizing properties and modeling execution environments demand formal-methods expertise. Proof therefore remains reserved for a few notable artifacts, while production software is attested mainly through review and testing. We introduce neuro-formal verification (NFV), which brings this automation to mainstream languages. An AI coding agent formalizes a source-level verification problem into a proof obligation in a verification-aware language, discharged by an established sound verifier aided by agentic proof search. Staged, goal-blind transformations reduce the risk of proving an artifact that does not faithfully represent the source program, property, or environment. Since NFV cannot ensure the soundness of this formalization, it optimizes for empirical accuracy rather than end-to-end soundness, while insisting on machine-checked evidence for every verdict. Experiments with current frontier models on a balanced dataset of correct and buggy Python solutions demonstrate the effectiveness of our approach. NFV with Dafny correctly resolves 57% of all entries, at 92% precision among its verdicts; with a CBMC backend, it produces a counterexample for 63% of the buggy programs at 90% precision. In contrast, an LLM-as-judge baseline achieves only 72% precision while answering every entry without any checkable artifact, and an unstaged agent-verifier combination proves 98% of both the correct and the known-buggy programs, yielding only 50% precision. Together, they confirm that both proofs and staging benefit an AI agent's formal program reasoning.
发表机构
- Microsoft Research（微软研究院）
机构由 AI 辅助整理，请以论文原文为准。
