神经形式验证：智能体驱动的语言无关程序形式推理
原标题：Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
AI 摘要
本文提出神经形式验证（NFV）方法，利用AI编码代理将主流编程语言程序翻译为Dafny等验证语言，并自动生成形式化证明或反例。在Python编程问题数据集上，NFV对57%的正确/错误条目返回Dafny证明（精度92%），对63%的错误程序返回CBMC反例（精度90%），相比LLM评判基线更具优势。该方法旨在让主流开发者无需形式方法专业知识即可获得机器检查的证明，提升AI生成代码的可信度。
正文节选
Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning Abstract Formal verification offers the strongest assurance available for software, and verification-aware languages have made its automation real. Yet the benefits reach few mainstream developers, most of whose languages have no verification support. Besides, specifying properties and modeling the environment require expertise in formal methods. Proof is therefore reserved for a few celebrated artifacts, while the pro