ProofLoom：用于自动形式化研究级随机优化的证明义务驱动理论构建

在精益中形式化研究级随机优化需要将基础库与收敛证明连接起来的算法模型和领域理论。修改模型以恢复可证明性可以改变数学主张。我们介绍 ProofLoom，一个用于证明义务驱动理论构建的全自动 LLM Agent系统。给定已发布的算法、目标定理和源证明，ProofLoom 自主构建精益模型和支持理论。开放证明义务推动了定义、接口、引理和证明计划的开发。签名合同记录模型修改的证据和义务；独立评审拒绝未经支持的假设和削弱的结论。 Planner 将已发布的论点扩展为中间声明，而 Audit 检查精益证明是否遵循它。在各个任务中，SOptLib 积累了经过验证的数学和构建经验：提取、概括和验证可重用的结果，同时记录建模决策和失败的证明路线。后续任务检索这些结果和记录并贡献新的发展，形成构建、积累和重用的循环。在 15 项教科书和研究论文任务中，ProofLoom 获得的平均人类评分为 6.3/7 和 6.4/7，而六个基线中最强的评分为 4.9/7 和 5.0/7。经过 33 个开发，它毫无遗憾地生成了 490,693 行算法本地精益代码。形式化还暴露了 22 个开发项目中已发布资源中的 28 个不正确的公式、证明差距和算法分析不匹配，每个项目都有经过检查的证据。