Automatic Textbook Formalization¶
会议: NeurIPS 2026
arXiv: 2604.03071
OpenReview: https://openreview.net/forum?id=dIjnouVokl
代码: https://github.com/facebookresearch/repoprover
领域: LLM Agent
关键词: 自动形式化, 交互式定理证明, 多智能体协同, Lean 4, 软件工程
一句话总结¶
本文提出一套基于工业级软件工程协作范式的多智能体自动化形式化框架，调度约 30,000 个 Claude 4.5 Opus 智能体在 1 周内将逾 500 页的研究生级代数组合学教材完全形式化为包含 13 万行 Lean 4 代码与 5,900 个声明的独立代码库，证明了全部 340 个目标定理与定义。
研究背景与动机¶
现代数学研究正面临前所未有的同行评审与复现危机。由于研究论文体量膨胀与技术细节极度繁琐，学术期刊审稿人往往无法逐行逐式核实论证细节，而仅能凭直觉判断论文采用的方法是否足以支撑其核心主张；正如数学家 Vladimir Voevodsky 与 Kevin Buzzard 所指出的，即使是被广泛研读、由资深权威学者撰写的重要论文，也屡次被发现存在未被察觉的隐蔽错误乃至错误的命题结论。交互式定理证明器（如 Lean 4）通过将信任基底压缩至极其严苛的内核以及少量顶层人工定义，为解决数学正确性验证提供了终极方案。然而，现有形式化数学库（如涵盖约 220 万行代码的 Mathlib）主要依赖人类专家耗费数年手工构建，不仅需要极其深厚的形式化专业素养，且年增长曲线已逐渐趋于线性饱和，严重制约了现代数学文献的全面形式化进程。
将人工智能引入形式化数学构想虽早已有之，但现有自动化形式化（Autoformalization）系统正面临清晰的技术代际瓶颈。第一代系统依赖针对孤立数学命题微调的专用单点模型（主要在 IMO 或 Putnam 竞赛题上评测），缺乏大型软件仓库级别的工程构建与跨文件依赖管理能力；第二代系统虽然引入通用大模型赋能的代码辅助智能体（如基于 Claude Code 形式化本科拓扑学单章节），但在真实长篇幅、高难度教材场景下受限于单一上下文窗口与串行执行的极高延迟，无法在有限时间内完成复杂数学教材的系统性构建。
为此，数学形式化亟需迈向多智能体协同的大规模软件工程体系，然而这一阶段的核心挑战在于多智能体并发协作中的“全局一致性与协调困境”：数百甚至上万个智能体在共享仓库中并行编辑时，极易产生语义重复、定义冲突、无限循环以及错误的证明分支。本文的核心切入点是将形式化数学建模为严格的协作式代码工程，直接移植人类软件工程中历经检验的分布式协作规范。核心 idea：将长篇数学教材形式化解构为基于 Git 主干开发与文件系统 Issue 追踪的多智能体软件工程协同任务，通过草拟、证明、双盲审查与多维维护角色的分工闭环，在无中心化重型调度逻辑下实现安全高并发的端到端定理形式化。
方法详解¶
整体框架¶
本文框架并不设计繁复的中心化 Python 调度器或私有消息总线，而是将 Git 仓库与本地文件系统作为通用通信总线与状态看板。系统将教材形式化任务解构为四大标准软件工程生命周期：草拟阶段（Sketching）、证明阶段（Proving）、双重代码审查阶段（Reviewing）以及持续维护与分流阶段（Triage / Maintain / Scan）。
整个系统支持数百个智能体在独立的轻量级 Git Worktree 中并行工作，所有操作均通过短生命周期的功能分支（Feature Branch）向主干（main）提交 Pull Request（PR）。每个 PR 必须同时通过编译构建测试、无代码冲突验证以及两套相互独立的审查智能体（数学语义审查与工程代码规范审查）的严格把关，方可进入合并队列合并入主干。
%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
A["输入：教材 LaTeX 源码<br/>500+ 页代数组合学"] --> B["草拟智能体：形式化骨架构建<br/>提取定义与定理，证明置 sorry"]
B --> C["议题追踪系统：任务分发看板<br/>基于 UUID 文件系统统一通信"]
C --> D["证明智能体：短分支定理攻关<br/>基于 Git Worktree 独立填充证明"]
D --> E["双重独立审查智能体：质量门禁<br/>数学语义保真度 + 软件工程规范"]
E -->|审查不通过 / 编译失败| D
E -->|审查通过| F["合并队列与集成构建<br/>Trunk-Based 自动化主干合并"]
F --> G["多维扫描与维护智能体<br/>全局去重、依赖重构与阻塞诊断"]
G -->|更新议题状态 / 提出重构 PR| C
F --> H["最终产物：独立 Lean 4 代码库<br/>130K 行代码，340 目标全部获证"]关键设计¶
1. 基于 Git 主干开发与轻量 Worktree 的无畏并发机制
大规模智能体协同以往常因共享状态修改导致严重的代码踩踏或重度加锁。本文采用敏捷软件开发中的主干开发（Trunk-based Development）模式，强制所有工作智能体基于最新的主干拉取短生命周期功能分支。底层执行依托 Git Worktree 技术，每个智能体被分配独立的临时工作树，通过共享只读的全局 Mathlib 预编译产物，使得每个分支极其轻量且隔离。智能体仅被赋予严格白名单约束的 Git 工具（如 git status、diff、commit、rebase），杜绝越权破坏主分支。通过严格限制单次 PR 的粒度（控制在约 100 行代码左右的原子变更），系统大幅削减了潜在的合并冲突几率，使近百个智能体可同时安全发起并行修改。
2. 独立解耦的数学语义与软件工程双盲审查门禁
为了彻底杜绝形式化中常见的“作弊”行为（如将复杂的数学映射偷偷改写为恒等映射占位符、引入不一致的公理或定义退化），每个 PR 提交后均被交由两个职责严格解耦的审查智能体评估。数学审查智能体（Math Reviewer）专注于比对 Lean 代码中的定理与定义是否在数学语义上对齐教材 LaTeX 原始叙述，严禁削弱假设或语义漂移；工程审查智能体（Engineering Reviewer）则严格审核代码风格、命名规范、API 易用性、文档完整度以及与 Mathlib 现有生态的兼容性。审查结果包含批准（Approval）、变更请求（Changes Requested）与直接否决（Rejection）。任何一个审查者否决即压制该 PR，任何一方提出修改要求则将具体报错与修改建议反馈给原智能体迭代。
3. 文件系统 Issue Tracker 架构与多角色协同闭环
为了解决上万次智能体交互中信息碎片化与缺乏中心协调的问题，本文没有采用复杂的微服务或向量数据库，而是在代码库内部建立由 Markdown/文本文件组成的 issues/ 目录。每个 Issue 赋予独立 UUID，记录任务状态、下游依赖阻断（Blockers）与重构建议。围绕此目录部署了专门的维护协作角色：
- 维护智能体（Maintainer）：认领 Issue，执行跨文件层级（最多涉及 14 个文件）的大型重构或打通卡住的中间引理；
- 分流智能体（Triage）：审查现有 Issue，识别已被合并代码实际解决的历史议题并打标关闭；
- 扫描智能体（Scan）与进度智能体（Progress）：周期性全局静态扫描代码库，识别跨章节出现的冗余重复定义与非规范用法，追踪 340 个核心目标的完备度，防止整个系统滑入偏离主线证明目标的无关分支。
4. 模拟退火式的全局一致性调控策略
针对大规模并发时出现的语义漂移（例如在不同章节独立重复定义了 3 套等价的 \(\mathbb{N}\)-分拆（\(\mathbb{N}\)-partition）数据类型，以及 Bender-Knuth 对合在行操作与前缀列操作中的定义分歧），系统探索出一种“项目级模拟退火”（Simulated Annealing）调控机制：在项目前期放宽对提示词与审查层级的约束，赋予 Prover 极大的局部行动自由度以利用高并发迅速铺开定理骨架；在项目中后期当主线目标逼近时，逐步“收紧螺丝”，大幅强化 Scan 与 Maintainer 智能体的干预权重，并升级 Prompt 严禁智能体跳入教材引用的外部前置定理（Rabbit Holes，例如 Kasteleyn 骨牌密铺公式中对 Pfaffian 理论的失控展开），推动局部私有 API 向共享统一 API 全面重构迁移。
一个完整示例：Bender-Knuth 对合的定义分歧与解决¶
在代数组合学形式化中，Bender-Knuth 对合（\(\beta_k\)）是证明斜 Schur 多项式对称性与 Stembridge 引理的核心工具。原文在自然语言中描述为“翻转行内游离的 \(k\) 与 \(k+1\) 之间的不平衡量”，算法定义繁复（教材中长达 5 页并包含多幅配图）。在形式化过程中，两个独立的证明分支产生了定义分歧：一个分支操作于全行并实现了元素匹配，但向右选择了多余的 \(k+1\)；另一个分支仅限制于列前缀且完全忽略了匹配条件。这导致下游 Prover 智能体陷入震荡——遇到利用错误定义恰好能证明的弱化引理时迅速给出证明，遇到数学不成立的断言时则不断报错并在 Issue Tracker 提交阻塞反馈。系统正是依托 Issue Tracker 留存的失败上下文，由 Maintainer 智能体发起全局审查，最终将全行匹配定义修正并重构下游依赖，成功完成斜 Schur 多项式对称性的完整形式化。
损失函数 / 训练策略¶
本系统无需对底层大语言模型进行额外的参数微调（No SFT / RL Training），直接采用具备卓越编程与工具调用能力的基座模型 Claude 4.5 Opus 作为统一部署底座。系统的计算消耗集中于多轮长对话推理与提示词工程优化。为了评估多轮长对话交互下的 Prompt Caching 经济性，论文推导了多轮对话中 Token 缓存开销与未缓存开销的解析关系： 设智能体总数为 \(N\)，单智能体平均对话轮数为 \(T\)，总处理输入 Token 计数为 \(C\)（计入多轮历史累积），单轮新增输入 Token 为 \(m\)，总输入对话长度为 \(L = T \cdot m\)。无缓存与启用缓存的总输入费用分别为： $\(P_{\text{nocache}} = c_{\text{in}} C = N m c_{\text{in}} \left(0.5 T^2 + 0.5 T\right)\)$ $\(P_{\text{cache}} = c_{\text{hit}} C + (c_{\text{in}} + c_{\text{store}}) N L = N m c_{\text{in}} \left(0.05 T^2 + 3.05 T\right)\)$ 其中 \(c_{\text{in}}\) 为基准输入单价，\(c_{\text{store}} = 2 c_{\text{in}}\) 为 1 小时缓存存储单价，\(c_{\text{hit}} = 0.1 c_{\text{in}}\) 为缓存命中读取单价。当平均轮数 \(T \approx 54.8\) 较长时，\(T^2\) 项系数从 \(0.5\) 骤降至 \(0.05\)，使实际总体推理成本从理论无缓存的约 $430,000 大幅压缩至约 $100,000。
实验关键数据¶
主实验：代数组合学教材形式化成果与规模统计¶
系统针对 Darij Grinberg 所著的研究生级教材《An introduction to algebraic combinatorics》（逾 500 页）展开端到端形式化。教材主要涵盖分拆、对称多项式、Pieri 规则、Schur 函数、RSK 对应、Bender-Knuth 对合以及 Jacobi-Trudi 恒等式等现代组合学核心内容。所有 340 个目标定义与定理全部通过 Lean 4 严格机器验证。
| 评估指标 | 本文系统（Multi-Agent RepoProver） | 传统人工专家团队预估 | 早期单智能体（Urban 2026） |
|---|---|---|---|
| 涵盖教材页数 | 500+ 页（研究生级） | 500+ 页 | ~50 页（本科初阶点集拓扑） |
| 目标定理与定义数 | 340 / 340（100% 证明完成） | 340 / 340 | ~20（单一章节局部） |
| 生成 Lean 4 源代码文件数 | 52 个 | 30~50 个 | 1~3 个 |
| Lean 4 代码有效行数 | ~130,000 行 | 100K~150K 行 | ~3,000 行 |
| Lean 声明总数（Declarations） | ~5,900 个 | 4,000~6,000 个 | ~150 个 |
| 消耗时间（Wall-clock Time） | 1 周（7 天） | 6~18 个月 | 1~2 天 |
| 经济成本估算 | ~$100,000 | \(100,000~\)250,000（按专家薪资估算） | <$1,000（无法扩展至整书） |
| 单页形式化成本 | ~$200 / 页 | \(200~\)500 / 页 | — |
| 单定理/定义形式化成本 | ~$300 / 目标 | \(300~\)750 / 目标 | — |
消融实验：各角色智能体计算量与执行产出分布¶
实验全周期共启动了 30,046 个智能体实例。不同角色展现了差异极其显著的行为特征与资源消耗模式：
| 智能体角色类型 | 实例总数（Count） | 累计输入 Tokens (M) | 累计输出 Tokens (M) | 平均单次对话轮数（Avg Turns） | 核心职能与交互表现 |
|---|---|---|---|---|---|
| Sketcher（草拟） | 85 | 6 | 0.0 | 59.8 | 提取全书大纲骨架，生成带 sorry 的定义与命题 |
| Prover（证明） | 8,704 | 25,012 | 194.2 | 50.0 | 单文件专注定理证明，提交原子级 PR（平均约 100 行） |
| Maintainer（维护） | 6,467 | 44,770 | 277.1 | 125.9 | 攻坚复杂 Issue，跨多文件重构（最高跨 14 个文件） |
| Math Reviewer（数学审查） | 6,797 | 3,759 | 42.9 | 21.7 | 严格比对 Lean 代码与 LaTeX 原文语义对齐度 |
| Eng. Reviewer（工程审查） | 6,805 | 1,542 | 20.7 | 12.7 | 检查代码规范、构建正确性与命名风格 |
| Scan（全局扫描） | 307 | 4,395 | 9.6 | 235.1 | 深度遍历代码库，排查重复定义与 API 碎片化 |
| Triage（分流） | 550 | 2,747 | 13.1 | 125.1 | 追踪并关闭已被历史 PR 隐式解决的冗余 Issue |
| Progress（进度监控） | 331 | 944 | 3.4 | 46.8 | 周期性核对 340 个主干目标完成率，防止系统跑偏 |
| 全系统合计 | 30,046 | 83,176 | 561.2 | 54.8 | 形成自组织、可自愈的闭环协同网络 |
关键发现¶
- 计算消耗的高度集中性：Prover 与 Maintainer 智能体占据了全系统超过 83% 的输入 Token 与 84% 的输出 Token；而审查智能体（Reviewers）对话轮数较短（平均 12~22 轮），以较低开销为全系统构筑了至关重要的质量防线。
- 夭折与阻塞的根因分析：在所有智能体运行中，3,490 个 PR 成功合并，589 个 PR 已获批准但因技术重启滞留；而约 6,120 个智能体因初始阶段的网络文件系统（NFS）IO 拥塞与合并队列超时被中止（Aborted），约 4,668 个智能体因遇到未解的先决条件而阻塞退出（No PR - blocked）。这表明工程基础设施（文件 IO 性能与并发合并队列架构）是限制大模型群体发挥潜力的真正物理瓶颈。
- 大幅降本的可行空间：作者明确指出，约一半的无效 Token 浪费在早期工程调试、无先决条件提示词约束导致的兔子洞（Rabbit Holes）以及缺乏任务有向无环图（DAG）调度导致的重复阻塞重试中。通过引入确定性任务 DAG 调度与优化提示词，预计可在不升级模型的前提下实现 3~10 倍的成本下降（降至每页 \(20~\)70）。
亮点与洞察¶
- 将定理证明升华为分布式代码工程：以往研究过度纠结于单步数学推理的启发式搜索，而本文证明，当底层模型代码理解能力达到一定水准后，制约数学自动化的核心是“如何组织数万次原子修改”。采用 Git 分支与 PR 机制天然化解了多智能体记忆膨胀与一致性冲突。
- 极简的文件系统 Issue 追踪哲学：放弃繁杂的多智能体通信协议，仅依靠文件系统中的 Markdown/文本记录 Issue，使得任何智能体均能通过最简单的文件读写工具获取上下文与报告阻断，实现了完全去中心化的松耦合协作。
- 可复用的工业级多智能体启示：从前期“自由发散探索”到后期“紧缩规则重构”的模拟退火策略，不仅适用于数学形式化，对自主软件工程、自动大型代码库迁移重构等场景均具有极高的通用参考价值。
局限与展望¶
- 单线程合并队列与 IO 瓶颈：当前架构下所有经过审查的 PR 均汇入串行合并队列，高并发时分支严重落后主干导致反复 Rebase 失败；未来需引入类似 Bors 机器人的批处理合并与二分故障隔离技术。
- 缺乏显式任务依赖拓扑（DAG）：目前智能体遇到前置缺失时仅能被动标为 Blocked，系统缺乏自上而下的任务拓扑调度，导致大量算力被浪费在无谓的阻塞轮询与死锁竞争中。
- 语义微小偏差的长尾风险：尽管双盲审查与人工抽查保证了高置信度，但长篇形式化中极少数深层定义与引理仍可能存在未完全等价的表述，仍需学术社区通过其开源的 Blueprint 交互式对照网站进行长效检验。
相关工作与启发¶
- vs 单智能体形式化（如 Urban 2026）：单智能体架构仅能在线性序列中处理局部、短篇幅定理，受限于单窗口容量无法应对跨章节大型教材；本文多智能体架构支持万级并发，直接实现百倍规模跃迁。
- vs 闭源/两阶段框架（如 Wang et al. 2026 M2F / Math, Inc. Gauss）：M2F 严重依赖 Mathlib 已有的实分析/复分析重合内容且两阶段割裂，Gauss 系统高度闭源；本文开源了全部代码与完整 13 万行 Lean 4 代码库，且选取的代数组合学内容与 Mathlib 高度正交，杜绝了数据污染争议。
评分¶
- 新颖性: ⭐⭐⭐⭐⭐ 首次成功构建万级通用编码智能体全自动形式化完整研究生教材的实用系统，奠定三代形式化范式。
- 实验充分度: ⭐⭐⭐⭐⭐ 真实落地 130K 行代码、340 个目标全证明、全量 Token 与开销审计，提供了极详尽的工程失效与消融数据。
- 写作质量: ⭐⭐⭐⭐⭐ 论证极其扎实，坦诚揭示了多智能体协作中的混乱期、定义冲突与工程瓶颈，极富洞察力。
- 价值: ⭐⭐⭐⭐⭐ 标志着数学文献大规模形式化从“纯手工小作坊”正式迈向“工业化自动化生产”，对 AI 驱动数学研究具有划时代里程碑意义。