一种人类战略指导下的自验证开发范式：LLM Agent 全过程构建、调试并形式化验证多项式因式分解库

Presenter: Haokun Li

Abstract: CLPoly 是一个 C++ 计算机代数库，其因式分解模块（4,617 行，10 种算法）完全由 LLM Agent（Claude）开发。开发过程中，在所涉及的复杂数学算法中发现了多个算法错误。为解决这一问题，我们指派同一个 LLM Agent 使用 Lean 4 和 Mathlib 对其编写的算法进行形式化验证——创建了一个自验证开发闭环：LLM 编写算法，然后在机器检查的形式方法下证明其正确性。

关键点：在整个过程（开发和验证）中，人类没有编写任何一行代码、证明或文档。人类的角色仅限于战略决策、质量标准和方向纠偏（约 150 条消息，平均约 8 个词）。Agent 自主完成所有技术工作：Mathlib API 调研、自然语言证明草稿、结构化审查、Lean 4 策略证明和迭代调试。最终成果是 6,276 行经机器检查的 Lean 4 证明（零 sorry），覆盖完整因式分解流程——包括单变量（SQF、DDF、EDF、Hensel、Zassenhaus 重组）和多变量（Wang/EEZ、MTSHL 稀疏 Hensel 提升、MDP 求解器、Vandermonde 恢复）。

本文描述了自验证方法论，量化了人机协作的工作分配，分析了失败模式，并论证了形式化验证是可信赖 LLM 生成数学软件的必要基础设施。