arXiv cs.AI· Martim Afonso, In\^es Lynce, Maurizio Morisio, Jo\~ao F. Ferreira·· 10 小时前AI 评分34
ProofCoder：面向自动化软件验证的持续推理系统
ProofCoder: Continuous Reasoning for Automated Software Verification
AI 导读
ProofCoder 是一个面向 Rocq 的智能体式证明合成系统，在 AutoRocq Benchmark 的 280 个验证任务上把证明成功率从 47% 提升到 60%，相对提升 27.7%，成本约为原来的一半。
正文 · AI 翻译
摘要：使用证明助手进行形式化验证可为软件提供强有力的正确性保证，但构造证明仍然是一项劳动密集型工作，且需要大量专业知识。近期基于大语言模型（LLM）的方法在自动化证明合成方面展现出前景。然而，这些方法通常将模型限制在僵化的策略生成循环中，由外围系统控制前提检索、证明状态管理和回溯。我们提出 ProofCoder，一个面向 Rocq 的智能体式证明合成系统，它从编码智能体的视角来处理定理证明。ProofCoder 并非在固定循环中生成策略，而是在整个证明搜索过程中持续推理，并利用证明助手的反馈来决定何时收集额外信息、检查证明状态、修改先前生成的证明片段，或回溯到证明中较早的位置。这使其能够在策略级或完整证明粒度上迭代地构造、修复和精炼证明。我们在 AutoRocq 基准中 280 个具有挑战性的验证任务上评估了 ProofCoder。在表现最佳的配置上，ProofCoder 将证明成功率从 47% 提升至 60%，优于最先进的 AutoRocq 系统，相当于在约一半成本下实现 27.7% 的相对提升。我们的消融实验将持续推理确定为关键设计选择：缺少它时，智能体解决的引理更少且成本大幅更高，回溯频率增加四到六倍，并更频繁地丢弃自己的修订。完整证明生成与策略级生成取得相似的成功率，但遵循不同的搜索与修复策略。这些结果表明，有效的自动化软件验证需要的不仅仅是改进策略选择：持续推理和反馈引导的证明修订是稳健证明合成的关键要素。
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI） |
| 引用为： | arXiv:2611.14106 [cs.SE] |
| （或本版本使用 arXiv:2611.14106v1 [cs.SE]） | |
| https://doi.org/10.48550/arXiv.2611.14106 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Martim Afonso [查看邮箱]
[v1]
2026年11月10日星期二 13:59:49 UTC（665 KB）
来源：arXiv cs.AI · arxiv.org