🤖 AI

Formally Solving Answer-Construction Problems in Lean

本文介绍了 ECP，这是一个在 Lean 中实现的神经符号框架，它结合了用于枚举候选答案的工具辅助型通用大语言模型（LLMs）与用于生成机器检查证明的证明型大语言模型（LLMs），有效地解决了在形式化解决数学答案构建问题方面的空白。

原作者： Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel

发布于 2026-06-02

📖 1 分钟阅读☕ 轻松阅读

原作者： Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你正在参加一场非常困难的数学竞赛。你可能会遇到两种类型的题目：

“证明题” (The "Prove It" Question)： 评委给你一个陈述，比如“天空是蓝色的”，然后问：“你能证明这是真的吗？”你只需要写出一个逻辑严密的论证过程。
“构建题” (The "Build It" Question)： 评委要求：“找到满足这些奇特规则的最小数字。”你必须先发明出这个数字，然后再去证明它为什么有效。

这篇论文专门讨论第二种类型：答案构建 (Answer-Construction)。这体现了成为一名辩护已知案例的律师，与成为一名必须在设计建筑之前先证明其不会坍塌的建筑师之间的区别。

问题：工具的不匹配

作者注意到 AI 在处理这些任务时存在差距。

通用 AI（“大脑袋”）： 可以把它想象成一位才华横溢、能言善辩的教授。它擅长头脑风暴、猜测数字和进行粗略计算。但如果你要求它写出一个正式的、符合机器标准的证明，它往往会变得偷懒、捏造事实，或者编写无法编译的代码。而且，雇佣这样的人成本很高。
证明 AI（“严格的编辑”）： 可以把它想象成一个微小、高度专注的机器人，只接受过编写正式证明的训练。它很便宜，且擅长检查逻辑，但它非常不擅长猜测“答案可能是什么”。如果你问它“找到那个数字”，它可能会对着墙发呆，或者随机猜一个并不成立的数字。

陷阱：
如果仅仅要求“严格的编辑”去解决一个“构建题”，它可能会作弊。它可能会说：“答案是‘满足规则的最小数字’。”从计算机的角度来看，这在技术上是一个有效的答案，但在真正的数学竞赛中，这是一个循环论证的作弊行为。你需要一个具体的数字，比如 245。必须强制计算机停止作弊，并真正找到那个真实的数字。

解决方案：ECP (枚举-猜想-证明)

作者构建了一个名为 ECP (Enumerate-Conjecture-Prove) 的新系统。它像是一个协作团队，利用一种叫做 Lean（一种计算机证明辅助语言）的语言来解决这些“构建题”。

以下是这个团队的工作方式，使用侦探类比：

1. 侦探 (通用 AI + Python 工具)

角色： 这位“大脑袋”教授，但这次他配备了计算器和可以运行代码的电脑。
行动： 他不再只是盲目猜测，而是编写一个 Python 程序来进行暴力搜索以寻找线索。他通过运行循环来测试成千上万个较小的数字，看看哪些符合规则。
“猜想” (The "Conjecture")： 基于数据，侦探提出了一个有根据的猜测：“我打赌答案是 245。”他会用直白的英语写下自己的推理过程。

2. 守门员 (可采纳性检查器)

角色： 这是俱乐部的保镖。
行动： 在侦探的猜想被允许进入下一步之前，守门员会对其进行检查。
- 它是一个真实的数字吗？（是的，245 是一个数字）。
- 它在作弊吗？（侦探只是说“答案就是答案”吗？并没有。）
- 它使用了禁词吗？（他们是否使用了竞赛中不允许使用的复杂数学符号？没有。）
如果猜想未通过检查，守门员会将它退回给侦探，让其重试。

3. 法官 (证明 AI + Lean 自动化)

角色： 这是那位“严格的编辑”机器人。
行动： 一旦守门员批准了猜想（245），法官就会接管工作。法官会忽略“我们是如何找到它的”部分，而完全专注于“为什么它是正确的”部分。它使用形式逻辑来证明，毫无疑问地证明 245 确实是正确答案。
如果证明失败，法官会将它退回给侦探，让其尝试另一个数字。

结果：奏效了吗？

作者在两个著名的数学数据集上测试了这个系统：PutnamBench（大学水平数学）和 MathArena（类似于 AIME 的高中竞赛）。

旧方法： 如果你只是要求“严格的编辑”去解决这些问题，它大多会失败，或者通过给出循环论证的答案来作弊。如果你要求“大脑袋”完成所有工作，它会在正式证明的部分卡住。
ECP 方法： 通过分工协作，该系统解决了 346 个难题中的 17 个，以及 75 个高中问题中的 18 个。
为什么这很重要： 这不仅仅是关于得到正确的数字；它是关于获得一个经过机器验证的证明，证明该数字是正确的，并且答案并非作弊。

总结

可以将 ECP 想象成一个处理数学问题的工厂流水线：

工人 A (通用 AI) 使用工具挖掘答案。
检查员 B (守门员) 确保答案是一个真实的、非作弊的数字。
工人 C (证明 AI) 构建坚不可摧的逻辑之桥，以证明该数字是正确的。

这种方法弥合了“猜测答案”与“证明答案”之间的鸿沟，使 AI 能够解决既需要创造力又需要严密逻辑的数学问题。

技术摘要：在 Lean 中形式化解决答案构造问题

问题定义
数学竞赛题目通常分为两类：定理证明（验证给定命题）和答案构造（构造一个满足特定属性的具体对象）。虽然近期大语言模型（LLM）在形式化定理证明方面取得了显著进展，但形式化答案构造的研究仍相对匮乏。非形式化推理系统（擅长猜想但弱于形式化验证）与形式化证明器 LLM（优化用于证明但难以发现消除存在量词所需的见证者/witness）之间存在着关键的鸿景。

形式化答案构造的一个特定挑战是可容许性（admissibility）。标准的 Lean 检查器仅验证证明项是否具有正确的类型，但并不本质地强制要求构造出的见证者必须是一个规范的、闭式形式的答案。例如，一个证明可以通过返回一个非规范项（如 sInf PropertySet，即所定义集合的下确界）而非显式的自然数（如 245）来满足存在性陈述 $\exists x, P(x)$ 。这类“循环”或非闭式形式的见证在逻辑上是有效的，但在数学竞赛中是不可容许的。

方法论：枚举-猜想-证明 (ECP)
为了应对这些挑战，作者引入了 枚举-猜想-证明 (Enumerate-Conjecture-Prove, ECP)，这是一个专为 Lean 4 中端到端答案构造与形式化证明设计的神经符号框架。ECP 将过程分为不同的阶段，同时保持形式化验证环路：

问题形式化与可容许性检查：
- 将问题形式化为函数合成任务：寻找一个函数 $\Psi$ ，使得 $\forall X, P(X) \to Q(X, \Psi(X))$ 。
- 实现了一个可容许性检查器，以确保合成的答案仅使用预定义的“可容许词汇表”（例如特定的常量、算术运算符和标准构造器）。它从 Lean 项中结构化地提取语义常量，并过滤掉管理类常量（如类型类实例或编译器生成的伪影）以及非规范定义（如 sInf）。
枚举阶段（工具辅助探索）：
- 配备 Python 工具执行能力的通用 LLM（如 GPT-5.4）被用于此阶段。
- LLM 编写并执行 Python 代码，在小规模定义域内进行有界枚举，以寻找满足问题约束的元组。
- 这些执行轨迹作为经验证据，用于识别模式、不变性和函数形式。
猜想阶段（答案合成）：
- 利用来自枚举阶段的证据，同一个通用 LLM 合成候选答案函数 $\Psi'$ 。
- 候选对象在进入下一步前需经过两个过滤器：
  - 语法验证： 该项必须能在 Lean 中编译并通过正确的类型检查。
  - 可容许性验证： 该项必须仅使用允许词汇表中的常量。
- 如果候选对象失败，系统会携带失败信息进行迭代。
证明阶段（形式化验证）：
- 一旦构造出有效的候选对象 $\Psi'$ ，系统会尝试证明实例化后的定理 $Stmt(T)|_{\Psi=\Psi'}$ 。
- 反驳环路： 在尝试证明之前，系统会尝试通过证明其否定命题来反驳该候选对象。如果反驳成功，则丢弃该候选对象并返回猜想阶段。
- 证明生成： 如果反驳失败，系统会结合 Lean 内置的自动化工具（如 simp, aesop, ring, norm_num 等策略）以及专门的证明器 LLM（如 Goedel-Prover-V2）来尝试证明正向命题。如果自动化失败，则调用证明器 LLM 进行修复环路以生成或修正证明。

核心贡献

答案构造框架： ECP 是第一个明确将答案构造与证明生成分离，并在形式化验证环路中强制执行可容许性约束的框架。
可容许性强制执行： 本文引入了一种结构化方法，用于过滤掉标准 Lean 检查器可能会接受的非规范见证（例如循环定义），从而确保输出符合竞赛要求。
神经符号集成： 该框架有效地结合了通用 LLM 的探索性推理、Python 工具以及专门证明器 LLM 的严密证明能力。
自动形式化与基准测试： 作者将 75 道来自 2026 MathArena 最终答案竞赛（AIME, HMMT, APEX）的问题以及 346 道来自 PutnamBench 的答案构造问题进行了自动形式化处理，创建了该类问题的新评估标准。

实验结果
系统在 MathArena 2026（75 道题）和 PutnamBench（346 道题）上针对包括直接证明生成 LLM（GPT-5.4, Goedel-Prover-V2）在内的基线模型进行了评估。

端到端性能： ECP 的表现优于直接证明生成基线。
- MathArena： ECP 解决了 18/75 个问题（Pass@32），而表现最好的纯 LLM 基线（GPT-5.4）为 13/75。
- PutnamBench： ECP 解决了 17/346 个问题（Pass@32），而 GPT-5.4 为 8/346，Goedel-Prover-V2-32B 为 7/346。
仅答案准确率： 工具辅助的答案构造显著提高了通用 LLM 生成正确候选对象的准确率。对于 GPT-5.4，工具使用将其在 PutnamBench 上的正确答案构造数量从 290/346 提升至 303/346。
可容许性影响： 分析显示，许多基线生成的证明虽然可以被 Lean 编译，但包含了不可容许的答案（例如循环见证）。ECP 明确的可容许性检查对于过滤这些内容至关重要。
消融实验：
- 移除证明器 LLM 修正步骤会降低 MathArena（18 $\to$ 16）和 PutnamBench（17 $\to$ 16）的性能。
- 移除 Lean 自动化对 MathArena 的影响严重（18 $\to$ 11），但在本次 PutnamBench 的特定运行中影响较小，这表明 MathArena 问题更依赖自动化策略，而 PutnamBench 更依赖证明器能力。
- 使用较小的证明器（8B）可以维持 MathArena 的性能，但会导致 PutnamBench 结果大幅下降（17 $\to$ 7），表明 Putnam 问题更多受限于证明搜索。

意义与主张
本文声称 ECP 成功弥合了非形式化答案生成与形式化定理证明之间的鸿沟。通过显式处理“答案构造”阶段并强制执行可容许性，ECP 解决了目前直接证明生成方法难以处理的实例。作者强调，对于需要构造特定见证（存在量词）而非仅仅验证固定结论的问题，其方法尤为有效。

这项工作凸显了当前的正式基准测试往往忽略了答案构造的难度，而是侧重于问题的“带答案”版本。ECP 证明了将用于枚举的通用 LLM 与工具执行相结合，随后使用专门的证明器 LLM 进行验证，是解决形式系统中复杂、开放式数学问题的可行路径。作者指出，该方法在可容许词汇表标记的启发式性质以及高度复杂的组合数学问题中枚举阶段可能存在的组合爆炸问题方面仍存在局限性。