AI4Math · Invited Talk 06 · Emily First

来源： Invited Talk 06 · Emily First 播客： ICML 2026 · AI4Math 分类： AI 研究 原文发表： 2026-07-11 纪要生成： 2026-07-13

基本信息

• Workshop：3rd AI for Math Workshop — Toward Self-Evolving Scientific Agents
• 类型：Invited Talk（远程 Virtual；讲者因参加婚礼无法到场）
• 题目：Model Diversity for Theorem Proving, Lemma Conjecturing, and Algorithmic Reasoning（模型多样性用于定理证明、引理猜想与算法推理）
• 讲者：Emily First（Rutgers University 助理教授，刚结束助理教授第一年；研究 AI × 软件工程 × 形式方法，聚焦定理证明与形式验证；UMass Amherst 博士，UC San Diego 博士后）
• 真实时段：约 14:47–15:22（KST，7/11；此前有咖啡休息，主持人宣布 2:50 PM 回来）

一句话概括

主张"不必只追求单一最优模型"：在有外部验证器（定理证明器）的形式化场景中，模型多样性本身是可利用的资源。通过三组研究说明——多样模型可协作证明更多/更快定理（ProofCoop/DIVA）；神经符号结合在引理猜想上稳定优于纯神经与纯符号（Lemonade）；用"强制输出格式/推理轨迹"可研究模型的鲁棒性与机理（形式文法解析）。

背景与动机

训练一个模型完成特定任务，涉及大量设计决策：模型架构、训练算法、超参、数据格式、数据来源等，我们常想优化出"最好的方式/最好的模型"（如某任务上最高准确率）。但这未必实际、也未必必要：算力有限、无法穷尽整个设计空间。这一点在形式数学里尤为突出——因为这里我们能获得输出正确性的形式保证、有可用的外部工具帮弥合差距、"有趣性（interestingness）"常无良定且主观、且泛化是我们想要的。因此本讲论证：研究"模型多样性"在多种形式设定与任务中是有利的，并通过若干针对性研究展开。三个部分：多样模型协作证明；神经符号 vs 纯神经做引理猜想；以及关于"多样性与算法推理如何揭示模型鲁棒性"的极初步工作（形式文法解析）。

主要内容

一、多样模型协作做定理证明（DIVA → ProofCoop）

设定：用交互式定理证明器（Rocq / Lean / Isabelle）做证明合成——一个神经模型做下一 tactic 预测 + 某种搜索（如 step 搜索）。搜索树每个节点是一个 proof state、每条边是模型预测、可在证明助手里执行得到下一状态再喂回模型；有的预测导致验证器报错或没到达新状态（即没推进证明），但通过在每个岔口尝试多个可能 tactic，最终可能完成证明（无目标可证）。这是如今相当标准的设置。很多工作问"如何改进 proof search 以证更多定理"——要么改偏置搜索的模型、要么改搜索过程本身。

从模型角度，有很多（甚至很朴素的）方法可"榨取更多"：不同训练集、不同架构、不同超参、乃至随机噪声；可以枚举各种组合、训一堆模型让它们各自搜索。因为我们有 Oracle（定理证明器本身），能看每次搜索是否有成果、不同搜索是否互补（多样模型能证不同的定理集）。

• DIVA（讲者"看似很久以前"的前作）：正是研究这一点——聚合各模型结果、看哪些多样性维度带来最强互补。这里各模型的搜索尝试分开保留、每次搜索同一最大预算；对一个集成（ensemble），只要1 个模型成功、该定理就算集成成功。

• ProofCoop：进一步研究"在搜索中让模型协作"。动机：设两个模型 A、B 都证不出某定理，但 A 能在搜索中取得一些进展、B 立刻卡住；若组合它们，也许 B 能在 A 引入的某个 proof state 上取得进展，最终导向证出定理。该工作考察多个"带来互补性"的多样性维度；用一组 5 个模型，发现用来自不相交项目的不同训练集带来（DIVA 式聚合下的）互补性。用 RNN 模型（可从零训练、无测试泄漏之虞；且推理在 CPU 上，可便宜地探索多种协作方式）。把一个大规模训练集切分训 5 个多样模型，在 12000 个定理上评测。它探索了 6 种协作方式，讲者概述其中 3 种（相对"非协作基线"）：

• Union tactic prediction（并集预测，最暴力）：对两个模型，每个 proof state 同时尝试 A 的预测和 B 的预测（在每个岔口都试两模型的预测）。这会让搜索树很快变宽，可用 tactic subsumption 和自动化 tactic 自然剪枝。结果：该法比非协作基线多约 20% 概率证出定理，相当有效；且有趣的是——把两个各自表现差的模型这样组合，可达到"最佳单模型"的水平，说明协作能从次优训练中恢复（这很棒，因为"训一个最优模型"本身是高风险高投入的事）。代价：union 预测虽平均更有效，但合成证明的证明步数多于非协作基线。

• Shared sub-goal access（共享子目标）：概念上类似 SMT 求解器里的 clause sharing。A、B 各自在搜索；若一方闭合某子目标，另一方可获得该子目标的子证明，在遇到同一子目标时使用。结果：对证明成功率有些帮助，但更主要是让证明快 50%（更偏效率）。
• Ensemble vote（每步投票）：让集成对每步预测投票。结果：比非协作基线效果差，但比它更高效，也比单个模型自搜更高效。

总体：多样模型协作可视为增强证明生成能力的方式，"增强"可指更有效或更高效。自然要问"是什么在驱动性能"——但难以确切说清：我们只在末端按"最终表现"测多样性，不可解释（不知模型为何不同、学到并执行了什么策略）。故余下部分转向"在输出格式上强制多样性"。

二、引理猜想：神经符号 vs 纯神经（Lemonade）

任务（bottom-up conjecturing，自底向上猜想），很探索性：给一些符号及其定义，试图发现关联它们的有趣定理/引理。存在符号技术可搜索"匹配给定引理形状"的猜想——用一个模板（template）定义理想引理的形状，从而限制符号工具的搜索空间。给定这些信息后，符号工具很擅长这个发现过程。但大问题是：谁来提供高质量、相关的模板？观察到：跨理论、在 Isabelle 里，少数模板占了绝大多数引理——模板可作为一种抽象，让我们发现跨理论的类比。而"擅长学类比与泛化"的正是——LLM。

于是：用 LLM 生成模板，再构建模板导向的合成器（template-directed synthesizer）去实例化模板、生成引理——即神经与符号引擎结合，而非只用其一直接猜想（纯神经会在猜想时幻觉符号）。整体流程：给定一个形式化，从中抽取上下文 → 用神经引擎预测模板 → 把模板与符号信息交给符号引擎生成猜想 → 评测。这里"成功"=能从原形式化中复原一个 gold-standard 引理（人类自己觉得足够有趣才写下并在其形式化中反复使用，故可视为"有趣引理"）；对那些不匹配 gold-standard 的猜想，可用 Isabelle 自身的自动化工具看是否有反例、或是否可证。

评测（Lemonade 在多个大规模基准、跨多领域）：

• 在 whole library（Isabelle 核心库，较同质的设定）：神经符号法优于纯神经法，且在不同微调后端模型上都成立（从 1.3B 到 6.7B 参数）。
• 在更多样的 Archive of Formal Proofs（AFP）（形式化主题与风格极其多样）上有类似优势——神经符号法能克服纯神经法的一些困难，尤其面对形式化中引入的新符号时。
• 在可另跑纯符号工具 QuickSpec 的若干特定项目上做定向对比：Lemonade 与神经法都大幅优于 QuickSpec。
• 用前沿模型（Claude/GPT）做 Lemonade 式 few-shot 时，相对"用同样模型直接猜想"优势不大；但小的微调变体在该设定下优于前沿变体；总体上，若把所有变体的猜想结果聚合，互补性很强。

三、算法推理：形式文法解析中的多样性与鲁棒性（极初步）

Lemonade 展示了"强制输出格式"如何帮助模型生成不同猜想；可以更进一步——在更受控的设定里强制输出推理轨迹本身，即形式文法解析。任务：考虑 mix-fix、闭算符文法（无歧义），可枚举产生式规则（把结构性终结符放在递归占位/洞的周围）；因文法已知，可生成合法句子、结构、精确解析轨迹（保持任务固定）。给定句子可生成对应的解析结构（一棵展平的推导树）；对固定文法，可训模型做解析（只见"句子—结构"对，训练时不显式给完整文法）。

存在确定性解析算法，按"人类认知负荷"排难度：

• 难度 1（最易，sequential matching）：从左到右扫描，遇局部结构 token、把递归暴露为嵌套的局部匹配；
• leftmost substitution（最左替换）：反复扩展最左的剩余非终结符，每次扩展可引入后续递归子问题；
• greedy substitution（贪心替换）：在移到下一前沿前，先解析当前所有前沿非终结符（一步推导可应用多条产生式规则）。

因为是确定性算法，可表现为不同的思维链（CoT）（用自然语言描述执行该算法的步骤）。可训模型输出"算法推理轨迹 + 最终答案"，每个推导步让模型 emit 显式产生式规则（e）或隐式（i）。

发现：

• 分布内（in-distribution）：所有算法格式（e / i），乃至无 CoT 的"直接从句子生成结构"格式，表现都很相似且很好——基本都解决了任务。
• 但机理分析显示：表现相同的模型内部表征不同——编码递归特征（如产生式规则）时，不同模型沿不同方向编码同一特征；就隐藏态几何而言，早/中层高度相似、但越往后越发散；就注意力而言，多样模型依赖不同的关键 attention head 集合与数量。
• 长度分布外（length OOD，句子比训练更长）：greedy substitution（记为 D3）与"直接解析"变体（仅句子→结构）的最终结构准确率下降；而 leftmost substitution 出现"最终结构准确率与 CoT 轨迹准确率之间的大差距"——即模型能从 CoT 中途的错误中恢复。深入分析并建了错误分类：模型的 CoT 未正确记录句子中的"当前索引"——当两个非终结符之间距离超过某阈值时（该情形在训练中欠表示）。有趣的是，这个"索引记账"其实是人类的辅助记账工具、算法执行本身并不需要——模型自己也发现不需要它。于是，用"该类型、但对所有模型变体仍在分布内"的样本增广训练数据后，该格式的 CoT 轨迹准确率大幅提升，同时提升所有模型变体的表现。随着继续看越来越长的序列（延伸 OOD 任务），这一趋势与有用的增广程序大体保持——因此有些模型变体比另一些更鲁棒；为一个变体揭示的错误，可帮助设计对其他变体的干预。

关键结论 / Takeaways

• 不必执着"单一最优模型"：在有外部工具/验证器时，模型多样性可让整体表现超过任一单变体，也可用于研究方法的鲁棒性。
• 协作证明：union 预测多 20% 证明率、可让弱模型组合达到最佳单模型；共享子目标快 50%；投票更高效但更弱。各有"更有效/更高效"的取舍。
• 引理猜想：神经符号结合稳定优于纯神经与纯符号（QuickSpec），小微调变体甚至优于前沿变体，聚合互补性强。
• 算法推理：同表现、不同机理；OOD 下差异显现（leftmost 能从 CoT 错误恢复），针对性的分布内数据增广能整体提升——一个变体的错误可指导对其他变体的干预。

Q&A / 讨论亮点

• 讲者为虚拟远程（因参加婚礼），演讲末尾开放提问；主持人（Speaker 5）随即致谢"感谢 Emily 熬夜陪我们"，现场无实质提问，之后衔接闭幕演讲（Zheng Yuan）。

名词 / 引用

• DIVA / ProofCoop / Lemonade：多样模型互补聚合、协作证明、神经符号引理猜想三项工作。
• union tactic prediction / shared sub-goal access / ensemble vote：ProofCoop 的三种协作机制（另有共 6 种）。
• QuickSpec / Archive of Formal Proofs (AFP) / Isabelle：纯符号猜想工具 / 大型证明库 / 证明助手。
• mix-fix 闭算符文法 / leftmost·greedy substitution / sequential matching：形式文法解析的算法与 CoT 格式（e=显式规则、i=隐式）。
• RNN 模型 / CPU 推理 / 12000 定理 / 5 模型：ProofCoop 实验规模。

原文发表：2026-07-11  ·  纪要生成：2026-07-13