用智能体树搜索提升大模型自动验证代码能力，关键突破在效率与难度平衡。
Automating Formal Verification with Agent-Guided Tree Search
- 设计双路径搜索结构：基于状态和上下文的智能体调度机制。
- 在423个规范上，GPT-5.4达95.0%正确率，仅需50次调用。
- 适合形式化验证、自动化编程研究者，推动可信软件落地。
形式化验证可实现可证明正确的软件，但编写验证代码成本过高，难以在生产中应用。近期大语言模型（LLM）加速了该工作，现有基准测试评估其将规格转换为代码及机器可检查正确性证明的能力。本文评估了当前基于Lean的LLM驱动验证代码生成（vericoding）水平，并提出基于搜索的方法以提升验证性能。我们复现了部分vericoding-benchmark Lean排行榜，在跨厂商模型池中发现，美国闭源模型表现稳定，而开源权重模型略有进步。通过引入含mathlib搜索的智能体循环，模型性能显著提升且随代理预算增长。GPT-5.4在423个规范上以$K=50$次调用达到95.0%准确率。进一步设计两种智能体引导的树搜索方案：基于状态的编排器在部分证明状态分支，基于上下文的编排器在完整子代理上下文分支。相较基础智能体，上下文方案在中等难度规范上以更低的令牌开销解决更多问题；而基础智能体在最困难规范上仍占优，因连续迭代至关重要。结论：搜索结构在特定场景优于强基线，更具挑战性的现代代码基准对推动自动化形式化验证进展至关重要。代码可联系作者[email protected]获取。
原文摘要 · Abstract (English)
Formal verification offers a path to provably correct software, but writing verified code remains expensive enough that the technique is rarely used in production. Recent large language models can accelerate this work, and recent benchmarks measure their ability to translate specifications into code and machine-checked proofs of correctness. This thesis evaluates the state of such LLM-driven verified-code generation ("vericoding") in Lean and develops search-based methods for improving verification performance. We first reproduce a subset of the vericoding-benchmark Lean leaderboard on a current cross-vendor model pool, finding that non-reasoning performance remains roughly steady on US closed-source models while open-weight models have slightly improved. We update the iterative methodology of vericoding-benchmark with an agentic loop equipped with mathlib search, finding that model performance greatly improves and scales with agent budget. GPT-5.4 nearly saturates the benchmark at 95.0% on 423 specs with $K=50$ LLM calls. We then design two agent-directed tree-search formulations: a state-based orchestrator that branches on partial-proof states, and a context-based orchestrator that branches on full subagent contexts. Compared against the agent baseline, the context-based design solves a wider range of intermediate-difficulty specs at lower token cost, while the agent baseline retains an advantage on the hardest specs, where uninterrupted iteration matters most. We conclude that search structure has selective advantages over a strong agent baseline, and that more challenging benchmarks drawn from modern code are important to measure and drive further progress in automated formal verification. Code available upon request by contacting the author at [email protected].
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。