ProofCoder：以持续推理实现自动化软件形式化验证
ProofCoder: Continuous Reasoning for Automated Software Verification
AI 导读
ProofCoder 是一个面向 Rocq 的智能体证明合成系统，从编码智能体视角出发，在证明搜索全程持续推理，利用证明助手反馈决定检索信息、检查证明状态、修订或回溯，而非固定在策略生成循环中。
正文 · 原文
Abstract:Formal verification using proof assistants provides strong correctness guarantees for software, but constructing proofs remains labor-intensive and requires significant expertise. Recent approaches based on large language models (LLMs) have shown promise in automating proof synthesis. However, these approaches typically constrain the model to a rigid tactic-generation loop, in which the surrounding system controls premise retrieval, proof-state management, and backtracking. We introduce ProofCoder, an agentic proof-synthesis system for Rocq that approaches theorem proving from a coding-agent perspective. Rather than generating tactics within a fixed loop, ProofCoder reasons continuously throughout proof search and uses proof-assistant feedback to decide when to gather additional information, inspect proof states, revise previously generated proof fragments, or backtrack to an earlier point in the proof. This allows it to iteratively construct, repair, and refine proofs, at either tactic-level or whole-proof granularity. We evaluate ProofCoder on 280 challenging verification tasks from the AutoRocq Benchmark. On the best-performing configurations, ProofCoder increases proof success from 47% to 60% over the state-of-theart AutoRocq system, corresponding to a 27.7% relative improvement at approximately half the cost. Our ablations identify continuous reasoning as a key design choice: without it, the agent solves fewer lemmas at substantially higher cost, backtracks four to six times more often, and more frequently discards its own revisions. Whole-proof and tactic-level generation achieve similar success rates but follow distinct search and repair strategies. These results suggest that effective automated software verification requires more than improved tactic selection: continuous reasoning and feedback-guided proof revision are critical ingredients for robust proof synthesis.
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2611.14106 [cs.SE] |
| (or arXiv:2611.14106v1 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2611.14106 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Martim Afonso [view email]
[v1]
Tue, 10 Nov 2026 13:59:49 UTC (665 KB)
来源：arXiv cs.AI · arxiv.org