发表机构
Nankai University; Peking University（南开大学; 北京大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
ProofLoom是一个全自动LLM智能体系统，通过证明义务驱动理论构建，在Lean中形式化研究级随机优化，自主构建模型和理论，并在15个任务上获得6.3/7和6.4/7的高评分，同时发现28处已发表错误。
AI 中文摘要
在Lean中形式化研究级随机优化，既需要算法模型，也需要将基础库与收敛性证明连接起来的领域理论。为了恢复可证明性而修改模型可能会改变数学论断。我们提出了ProofLoom，一个用于证明义务驱动理论构建的全自动LLM智能体系统。给定已发表的算法、目标定理和源证明，ProofLoom自主构建Lean模型和支持性理论。开放的证明义务驱动定义、接口、引理和证明计划的开发。签名契约记录模型修订的证据和义务；一个独立的评审者拒绝无根据的假设和弱化的结论。规划器将已发表的论证扩展为中间论断，审计器检查Lean证明是否遵循该论证。在各项任务中，SOptLib积累已验证的数学和构建经验：可重用的结果被提取、泛化和验证，而建模决策和失败的证明路径被记录。后续任务检索这些结果和记录并贡献新的进展，形成构建、积累和重用的循环。在十五个教科书和研究论文任务上，ProofLoom获得的平均人工评分为6.3/7和6.4/7，而六个基线中最强者的评分为4.9/7和5.0/7。在33个开发中，它生成了490,693行算法局部的Lean代码，且没有sorry。这些形式化还暴露了22个开发中已发表来源里的28个错误公式、证明缺口和算法分析不匹配，每个都有经过检查的证据。
英文摘要
Formalizing research-level stochastic optimization in Lean requires both an algorithm model and domain theory connecting foundational libraries to convergence proofs. Revising a model to restore provability can change the mathematical claim. We introduce ProofLoom, a fully automated LLM-agent system for Proof-Obligation-Driven Theory Construction. Given a published algorithm, target theorem, and source proof, ProofLoom autonomously constructs the Lean model and supporting theory. Open proof obligations drive the development of definitions, interfaces, lemmas, and proof plans. Signature contracts record evidence and obligations for model revisions; an independent Judge rejects unsupported assumptions and weakened conclusions. Planner expands the published argument into intermediate claims, and Audit checks whether the Lean proof follows it. Across tasks, SOptLib accumulates verified mathematics and construction experience: reusable results are extracted, generalized, and verified, while modeling decisions and failed proof routes are recorded. Later tasks retrieve these results and records and contribute new developments, forming a cycle of construction, accumulation, and reuse. On fifteen textbook and research-paper tasks, ProofLoom obtains mean human ratings of 6.3/7 and 6.4/7, compared with 4.9/7 and 5.0/7 for the strongest of six baselines. Across 33 developments, it produces 490,693 lines of algorithm-local Lean code with no sorry. The formalizations also expose 28 incorrect formulas, proof gaps, and algorithm-analysis mismatches in published sources across 22 developments, each with checked evidence.
Comments38 pages, 5 figures. Code and supplementary materials: https://github.com/Trace231/ProofLoom
