💻 computer science

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4

本文介绍了 AMBER，这是一个针对应用数学的新型 Lean 4 基准测试，它强调在验证之前构建显式解，并揭示了通用推理模型优于专门的定理证明器，因为后者倾向于遭受阻碍复杂指令遵循的“策略过拟合”。

原作者： Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen

发布于 2026-02-03

📖 1 分钟阅读☕ 轻松阅读

原作者： Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen

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

想象一下，你正在教一个机器人做数学题。长期以来，我们给这个机器人的测试就像是在问它：“这个谜题是否存在解法？”机器人可以通过说“我知道它就在某处”来回答“是”，但它从未真正找到那个碎片，也从未向你展示如何将其组装起来。

这篇名为**《构建—验证》（Construction–Verification）的新论文指出，对于应用数学**（即用于建造桥梁、优化物流路线或分析数据的数学）而言，仅仅说“它存在”是不够的。你需要机器人先构建出解决方案，然后再去证明它是有效的。

以下是研究人员的工作内容及发现的简单拆解：

1. 问题所在：“魔杖” vs. “蓝图”

在传统的数学测试中，机器人可能会使用一根“魔杖”（非构造性证明）挥动一下，化解问题并宣布：“解是存在的！”然后就结束了。

旧方式： “我证明了一座桥可以被建造。”（但你并不知道如何建造它）。
新方式 (AMBER 基准测试)： “这是蓝图和材料。请建造这座桥，然后向我证明它不会倒塌。”

研究人员创建了一个名为 AMBER（应用数学推理基准测试）的新测试。它强制 AI 遵循严格的两步工作流：

构建 (Construction)： 你必须编写代码或公式来实际计算出答案。
验证 (Verification)： 你必须证明你的答案是正确的。

他们在四个困难领域测试了 AI：

凸分析 (Convex Analysis)： 在弯曲的山谷中寻找最低点。
优化 (Optimization)： 制定最有效的计划。
数值代数 (Numerical Algebra)： 处理巨型矩阵中的数字。
高维概率 (High-Dimensional Probability)： 预测具有许多变量的结果。

2. 令人惊讶的结果：通用型选手击败了专业型选手

研究人员原以为专门训练成“数学证明者”的机器人会在这项测试中横扫对手。结果他们错了。

专家型选手（“战术过拟合”陷阱）： 那些仅针对数学证明进行训练的机器人陷入了困境。它们过于习惯于仅仅证明事物的存在，以至于忘记了如何遵循指令去“构建”事物。这就像一位国际象棋大师，由于太擅长赢棋，以至于忘记了如何摆放棋盘。它们试图通过“证明”答案存在，而不是实际计算出答案，从而导致测试失败。
通用型选手（“瑞士军刀”）： 接受过通用推理训练（如 DeepSeek 或 GPT）的机器人表现得好得多。因为它们习惯于在各种不同语境下遵循复杂的、多步骤的指令，所以它们能更好地做到：“好的，首先我需要定义这个函数，然后我需要证明它。”它们不会陷入“仅仅证明”的习惯中。

3. 测试的具体形式

论文描述了 AI 面临的三类挑战，这些挑战与标准的数学测试不同：

评估问题 (Evaluation Problems)： 测试不再问“是否存在一个数字 $x$ 满足此方程？”，而是问：“这是 $x$ 的公式。请编写计算它的代码。”
算法设计 (Algorithm Design)： 与其证明一个循环有效，不如要求 AI 亲自编写这个循环本身。这就像要求一位厨师不仅要证明蛋糕可以被烤出来，还要写出精确的食谱和搅拌说明。
表示转换 (Representation Transformation)： 这就像将一个混乱的现实世界问题（例如“我们如何调度这些巴士？”）转化为一种干净的标准数学格式（例如“这是一个线性规划问题”）以便计算机求解。AI 必须扮演翻译者的角色，而不仅仅是求解者。

4. 机器人在哪里失败了

当研究人员观察机器人为何失败时，他们发现了四个主要原因：

幻觉 (47%)： 机器人编造了并不存在的数学定理或库名称。它们听起来很自信，但实际上是在凭空捏造事实。
形式化错误 (33%)： 它们知道正确的数学概念，但无法将其正确地转化为严谨的计算机语言 (Lean 4)。
半途而废 (15%)： 它们开始了代码编写，但留下了未完成的部分，用“抱歉”（占位符）代替了完成最难的部分。
拼写错误 (5%)： 简单的格式错误。

核心结论

论文得出结论：要让 AI 在应用数学领域真正发挥作用，我们不能仅仅训练它成为一台“证明机器”。我们需要能够先构建解决方案，再验证其正确性的系统。目前，通用型 AI 模型在执行这种“构建”任务方面比专门的数学模型表现更好，因为那些专家模型在思维上变得过于僵化。

研究人员建议，未来的 AI 需要是一种混合体：既要足够聪明，能够遵循复杂的指令去构建事物；又要足够严谨，能够证明其正确性。

技术摘要：构建—验证：在 Lean 4 中实现应用数学形式化的基准测试

1. 问题陈述

当前的自动化定理证明基准测试（如 MiniF2F 和 ProofNet）主要侧重于对声明式命题的逻辑验证（即证明解的存在性）。这种范式对于应用数学而言是不充分的，因为应用数学的主要目标通常是推导具体的数值、可执行的算法或结构变换，而非仅仅是存在性证明。

现有数据集在该领域存在两个关键局限性：

范围差距： 它们缺乏对本科及更高水平应用数学的覆盖，包括凸分析、优化、数值代数和高维概率。
构造缺陷： 它们未能强制执行“构建—验证”的工作流。在应用数学中，模型必须在证明其正确性之前，显式地合成一个解（例如，一个算法或特定的值）。目前的基准测试允许模型通过使用非构造性策略（例如，通过极值定理证明存在性而不计算具体的极值点）来绕过这一过程，从而误导了模型进行计算推理能力的评估。

2. 方法论

构建—验证框架

作者提出了一个在 Lean 4 中的形式化范式，该范式在结构上强制执行一个两阶段工作流：构建（Construction） 随后是 验证（Verification）。该框架通过要求在证明之前进行显式定义，防止智能体利用非构造性的捷径。该框架针对三类特定的应用数学任务：

评估问题（Evaluation Problems）： 模型不是证明 $\exists x, Q(x)$ ，而是必须定义一个函数 def x (V) := ... 来根据参数 $V$ 计算解 $x(V)$ ，随后证明定理 $Q(x(V), V)$ 。函数的签名严格限制输入为原始参数，防止模型利用目标属性来为构造过程“作弊”。
算法设计问题（Algorithm Design Problems）： 智能体必须定义一个代表迭代过程（如梯度下降）的递归函数。任务要求填充第 $(n+1)$ 步的转移规则（循环体），随后证明收敛性或单调性等性质。
表示变换（Representation Transformation）： 智能体必须将原始问题实例建模为目标规范形式（例如，将图割问题转化为谱聚类公式）。这涉及定义新领域、约束条件和目标函数，并证明源问题与目标问题之间的松弛或等价关系。
定理证明（Theorem Proving）： 包含了一个传统的演绎任务子集作为基准，用以衡量区别于构造性合成的纯逻辑推理能力。

基准测试策展 (AMBER)

作者引入了 AMBER（应用数学推理基准），该数据集涵盖四个核心领域：

凸分析
优化
数值代数
高维概率

数据来源与难度： 问题源自经典教科书（如 Boyd & Vandenberghe, Vershynin），并按难度分类（简单：标准练习；困难：博士资格考试水平）。
形式化与验证： 每个子领域由经验丰富的 Lean 用户形式化了 50 个问题。验证过程包括两阶段：基于 LLM 的语义检查，随后是 Mathlib 贡献者进行的严格人工交叉验证，以确保与原始数学陈述严格一致。
复杂度指标： 该基准测试具有高语义依赖密度。通过依赖图分析（ $k=3$ ），AMBER 的平均依赖密度为 164.21，显著高于 MiniF2F (29.72)、ProofNet (33.95) 和 FATE (53.14)，这表明它对检索和推理复杂数学概念有着更深层次的要求。

3. 核心贡献

范式转变： 本文提出了一种从验证存在性命题向合成构造性解的转变，使形式化任务与应用数学的计算直觉相一致。
AMBER 基准测试： 一个涵盖核心应用领域且具有不同难度等级的综合数据集，其特点是包含算法设计和表示变换等复杂任务，而非仅仅是定理证明。
形式化模式： 专门的 Lean 4 模板，用于评估、算法设计和表示变换，这些模板通过设置严格的语法屏障来防止非构造性推理。
实证分析： 一项系统性评估揭示了当前神经符号系统中的一个基本权衡：局部策略熟练度（专门的证明器）与高层算法合成（通用模型）之间的张力。

4. 实验结果

模型性能

作者评估了多种模型，包括通用推理智能体（DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro）和专门的定理证明器（Goedel Prover-32B, Kimina Prover-72B）。

整体难度： 所有模型的表现普遍较低。在“困难”子集上，几乎所有模型的成功率都接近于零。
通用型 vs. 专门型： 与纯数学基准测试中的趋势相反，通用推理模型始终优于专门的定理证明器。
- Pass@16 (完整 AMBER)： 通用模型达到了 4.50%–6.00%，而专门证明器为 4.00%。
- Pass@16 (困难子集)： 通用模型达到了 0%–0%（在简单子集中存在变动），而专门证明器同样表现挣扎。
消融研究： “构建—验证”提示策略在 100 个问题的子集上实现了 8% 的成功率，优于标准的代码补全（6%）和传统的仅证明提示（5%）。仅证明提示经常导致模型使用非构造性捷径（例如 Classical.choice）。

错误分析

对 3,189 条来自 DeepSeek-R1 模型的错误消息进行的分析显示：

幻觉 (47.3%)： 最常见的失败模式，模型调用了不存在的定理或定义（例如 convexHull eq sInter）。
形式化能力不足 (32.7%)： 误用有效的策略或未能处理侧条件。
输出不完整 (15.2%)： 未能提供完全可执行的代码，通常在复杂的归纳步骤中留下 sorry 占位符。
格式/语法 (4.8%)： 基础的 Markdown 或语法错误。

5. 意义与主张

本文声称，当前的自动化形式化领域面临着“策略过拟合”现象。经过大量证明语料库微调的专门模型，其通用的指令遵循能力似乎有所下降。它们将每一个结构性挑战视为纯粹的定理证明任务，往往忽略了应用数学的多阶段要求（例如，在证明之前先定义一个函数）。

相比之下，通用模型保留了将非形式化意图转化为形式化语法的多功能性，能够成功地在进入验证阶段之前合成数学对象。作者总结道，推进形式化应用数学需要超越纯粹的证明搜索，转向能够将高层算法推理与严谨形式化验证相结合的神经符号系统。AMBER 基准测试为未来扩展形式化应用数学的前沿研究奠定了基础，因为它提供了一个要求构造性合成而非仅仅是逻辑有效性的标准。