面向验证条件的神经定理证明：一个真实世界基准

定理证明是程序验证的基础，其中验证条件（VC）的自动证明仍是主要瓶颈。真实世界的程序验证经常遇到现有自动定理证明器（ATP）无法证明的困难VC，导致对大量人工证明的关键需求，加重实际应用负担。虽然神经定理证明（NTP）已在数学竞赛中取得显著成功，展示了机器学习方法在形式推理上的潜力，但其在程序验证——特别是VC证明——中的应用仍未被充分探索。尽管已有关于标注合成和验证相关定理证明的工作，尚无基准专门针对这一基础瓶颈：自动化VC证明。本工作提出面向验证条件的神经定理证明（NTP4VC），呈现首个面向该任务的真实世界多语言基准。来自Linux和Contiki-OS内核等真实项目，我们的基准利用工业流水线（Why3和Frama-C）在Isabelle、Lean和Rocq等形式语言中生成语义等价的测试用例。我们在NTP4VC上评估通用以及针对定理证明微调的LLM。结果表明，尽管LLM在VC证明上展现出前景，程序验证仍存在重大挑战，凸显了未来研究的巨大差距与机遇。