发表机构
Astrio Labs（阿斯特里奥实验室）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出 FORALL-LEAN-AGENT 框架，通过隔离工作区、公理审计和独立检查实现可审计的 Lean 证明验证，在 VeriSoftBench 和 PutnamBench 上提升成功率并降低成本。
AI 中文摘要
编码智能体日益自动化地开发 Lean 证明，但仅凭成功编译并不能证明候选证明在可接受的假设下证明了预期命题。我们提出 FORALL-LEAN-AGENT，一个前端无关的框架，用于形式数学与软件验证中的可审计推理。该框架结合了隔离工作区、Lean 工具、以及带有语句比较、公理审计和（在支持的情况下）独立证明检查的全新审查。验证证据和审查者决策被绑定到同一候选工件上，使得验收具有可追溯性。我们在 VeriSoftBench、PutnamBench 以及 Lean Eval 软件验证赛道中的两个问题上评估了该框架。在 100 个任务的 VeriSoftBench 子集上，与 FORALL-LEAN-AGENT 的集成将 GPT-5.6 Sol 在低努力下的基准规则成功率从 93 提升到 100，同时将成本从 69 美元降至 62 美元。PutnamBench 评估接受了全部 672 个问题，平均每个 4.72 美元。这些结果表明，智能体框架设计可以在提供超越总体解决计数的证据的同时，提高正确性和效率。
英文摘要
Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions. We present FORALL-LEAN-AGENT, a frontend-agnostic framework for auditable reasoning in formal mathematics and software verification. The framework combines isolated workspaces, Lean tools, and fresh review with statement comparison, axiom audits, and independent proof checking where supported. Verification evidence and reviewer decisions are bound to the same candidate artifact, making acceptance traceable. We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track. On the 100-task VeriSoftBench subset, integration with FORALLLEAN-AGENT raises benchmark-rule success from 93 to 100 for GPT-5.6 Sol at low effort while reducing cost from $69 to $62. The PutnamBench evaluation accepts all 672 problems at an average of $4.72 each. These results show that agent harness design can improve correctness and efficiency while providing evidence beyond aggregate solve counts.
CommentsAccepted to NeurIPS 2026 VeriCodeGen
