miniF2F-Dafny:通过自动验证的LLM引导的数学定理证明

miniF2F-Dafny:通过自动验证的LLM引导的数学定理证明

miniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

https://arxiv.org/pdf/2512.10187

摘 要

我们提出了 miniF2F-Dafny——首个将数学推理基准 miniF2F 翻译至自动定理证明器 Dafny 的工作。此前，该基准仅存在于交互式定理证明器中（Lean、Isabelle、HOL Light、Metamath）。我们发现，Dafny 的自动化能力在无需任何人工证明步骤（即空证明）的情况下，验证了测试集 244 题中的 99 题（40.6%）和验证集 244 题中的 109 题（44.7%）。对于空证明失败的问题，我们评估了 12 个现成的大语言模型（LLMs）提供证明提示的能力。所测试的最佳模型通过迭代错误修正，达到了 55.7% 的 pass@4 成功率。这些初步结果凸显了一种高效分工：LLM 提供高层指导，而自动化机制处理底层细节。我们的基准数据已在 GitHub 上发布。

1 引 言

形式化数学推理长期以来被视为人类智能的标志，既需要创造性洞见，也要求严谨的逻辑演绎。大语言模型（LLMs）的出现为自动化数学形式化——即将非形式化的数学陈述与证明翻译为机器可验证的形式系统——开辟了新的可能路径。

早期工作主要聚焦于 Lean、Isabelle 和 Coq 等交互式定理证明器（ITPs），但这些系统需要大量人工构造证明：人类专家或 AI 系统必须为每一步逻辑推理提供显式的证明项。

为评估 AI 辅助形式化定理证明的进展，研究者开发了多个基准。其中，miniF2F 基准最初为 Lean 设计，包含 488 道数学问题，选自 AIME、AMC、IMO 以及高中和大学本科数学课程内容，分为 244 题的测试集和 244 题的验证集。它已成为评估 AI 系统形式化数学推理能力的标准基准。然而，所有现有翻译版本（Lean、Isabelle、HOL Light、Metamath）均面向交互式定理证明器——这些系统自动化程度有限，证明过程需要大量人工干预。尽管近期方法在 Lean 的 miniF2F 上取得了优异成果，但它们要么依赖于在形式化证明语料上大规模训练的专用模型，要么采用复杂的智能体框架来协调多个组件，以生成交互式定理证明器所需的详细证明脚本。

我们提出 miniF2F-Dafny——首个将 miniF2F 基准翻译至自动主动验证语言（auto-active verification language）的工作。与交互式定理证明器不同，Dafny 围绕由 SMT 求解器驱动的自动化推理能力构建，提供了一种根本不同的范式：许多数学问题仅需极少甚至无需人工证明步骤即可被验证。这引发了一个关键问题：在自动主动验证器中降低的证明复杂性，是否能让现成的 LLM 有效提供高层数学洞见——例如关键引理、证明策略或中间断言——而将底层逻辑推理委托给自动化求解器？

我们发现，仅靠 Dafny 的自动化能力，就能在零人工输入的情况下，通过空证明（empty proofs）解决 miniF2F 中 40–45% 的问题。对于剩余问题，我们评估了 12 个现成 LLM 提供证明提示以引导 Dafny 自动化的能力。结果凸显了一种高效的分工模式：LLM 无需生成完整证明，而是提供高层指导，自动化机制则处理底层细节。

我们的主要贡献如下：• 我们提出了 miniF2F-Dafny，这是 miniF2F 首次被翻译至自动主动验证语言。• 我们建立了基线结果：仅凭 Dafny 的自动化能力，在无需任何人工干预的情况下即可解决 40–45% 的问题。• 我们评估了 12 个现成 LLM 在需要人工引导的问题上提供证明提示的能力，最佳模型通过迭代修正达到 55.7% 的 pass@4 成功率。• 我们展示了 AI 辅助定理证明中“分工协作”的价值：自动化求解器处理底层逻辑步骤，而 LLM 专注于高层证明结构。

2 miniF2F-Dafny 基准
2.1 概述
miniF2F-Dafny 基准包含 488 道数学问题（244 道测试题，244 道验证题），从 Lean 版本的 miniF2F 基准翻译而来。每个问题均被表述为一个 Dafny 引理（lemma），包含前提条件（requires 子句）和后置条件（ensures 子句），但证明体为空。任务是在空证明不足以通过 Dafny 验证器时，合成一个有效的证明。

问题陈述可自然地从 Lean 转换至 Dafny，如图 1 所示。问题涵盖多个数学领域，包括代数、数论、不等式、组合数学和分析。每个子集（测试集与验证集）均包含 45 道 AMC 题、15 道 AIME 题和 20 道 IMO 题，其余题目选自大学本科数学课程。该基准同时考察系统提供高层证明策略（如引理调用、分情况讨论、归纳法）和底层证明细节（如代数运算、不等式链）的能力。

两个辅助文件提供了数学基础设施，尽管目前仍处于开发中。definitions.dfy 文件（300 行）对 Dafny 原生不支持的核心数学结构进行了公理化：整数、有理数、实数和复数，及其运算与性质。library.dfy 文件（550 行）包含 108 条公理化的引理，编码了关于指数函数、对数、三角函数、复数和数论的标准数学事实。原则上这些引理可被证明，但我们选择公理化它们，以将评估重点放在利用 SMT 自动化进行证明合成上。我们并未投入大量精力构建深层库，而是旨在测试现代 AI 系统在使用 Dafny 的霍尔逻辑（Hoare-logic）风格规范和 SMT 求解器自动化能力时，能多好地生成证明。

2.2 定义
该基准的数学基础由 definitions.dfy 提供，其中公理化了在 Dafny 中表达所有 miniF2F 问题所需的最小数学基础设施。与 Mathlib [12]（其中数学对象从第一性原理构造）不同，我们的公理化策略体现了 Dafny 的设计哲学：即依赖 SMT 求解器的能力，从一个可信的定义库出发进行自动化推理，而非要求构建庞大的形式化证明库。

这些定义覆盖四个数域：整数、有理数、实数和复数。每个数域均包含标准算术运算及领域特定的函数。

• 整数支持有限集上的求和与求积、模运算以及整除性谓词。
• 有理数被显式表示为分子–分母对，并配备分数算术。
• 实数包含超越函数（指数、对数、三角函数）、幂运算以及数学常数（如 π）。
• 复数提供域运算、范数函数和复指数函数。

该公理化采用 Dafny 的 :axiom 属性，通过规范（specifications）而非具体实现来声明函数。规范的复杂度因函数性质而异：

• 对于对数等超越函数（见图 3），我们公理化其基本值域性质——例如，规定当自变量大于 1 时对数为正，在 0 到 1 之间时为负，在 1 处为零。
• 对于求和等递归函数（见图 2），我们通过后置条件（postconditions）复现归纳定义：明确其在空集上的行为，以及在非空集上通过移除一个元素后的递归行为。
• 数论函数（如 gcd、lcm、素数判定）、组合函数（如 choose、阶乘）和工具函数（如 floor、ceil、abs）也以类似方式公理化。

这些契约（contracts）为 Dafny 基于 SMT 的自动化机制提供了足够的语义信息，使其能在许多问题上仅凭空证明即可完成验证。尽管这些公理化遵循标准数学定义，且我们对其正确性持谨慎信心，但这种实用主义方法仍不可避免地带来公理化本身固有的可靠性（soundness）考量。

2.3 库（Library）

作为定义的补充，library.dfy 提供了 108 条公理化的引理，编码了标准数学事实。该库采用问题驱动的开发方式：通过分析证明尝试过程，识别出所需的事实，再将这些引理与 Mathlib [12] 中的定理进行交叉核对以确保其可靠性，之后才集成进来。

我们并未提供这些引理的构造性证明，而是直接将其公理化，使问题能够调用已确立的结果而无需重新证明——这模仿了数学实践中的常见做法：引用已知定理，而非从头重建。这些引理涵盖多个数学领域：

• 指数/对数（27 条引理）：指数相乘、对数相加、换底公式（见图 4）
• 幂运算（8 条引理）：自然数与实数指数、幂律、平方根
• 三角学（37 条引理）：角加法公式、周期性、特殊值、毕达哥拉斯恒等式
• 复数（19 条引理）：域公理、范数性质、欧拉公式
• 数论（5 条引理）：最大公约数（GCD）交换律、GCD–LCM 乘积公式
• 分析（4 条引理）：极限唯一性、连续性性质
• 数列（8 条引理）：序列求和与求积、集合转换

每条引理均通过前提条件（requires）和后置条件（ensures）进行规范。例如，对数换底公式（图 4）要求底数为正且不等于 1，并确保不同底数对数之间的标准关系成立。此外，某些数学性质（如结合律、可加性）无法自然地编码为单个函数的后置条件，而必须作为独立引理显式陈述。

该库的规模（550 行）相比 Mathlib 的 200 万行有意保持极简，聚焦于奥林匹克级别数学所需的前置知识。这体现了一种务实的平衡：提供足够理论以表达并求解 miniF2F 问题，同时测试 AI 系统能否在紧凑的基础之上，有效利用 SMT 自动化能力构建证明。

该库很可能并不完备，若补充更多引理，评估结果很可能会进一步提升。

2.4 验证
我们基准测试的一个关键组成部分是验证所生成的解是否严格遵循原始问题陈述，而不对其弱化。这可以防止解决方案通过加强前提条件、弱化结论条件或引入不健全的公理来“作弊”——我们在其他基准（如 DafnyBench [11]）中已观察到此类问题，其薄弱的评估脚本允许这类违规行为。

对于一个以 Dafny 引理形式给出的问题，我们的验证器会拒绝以下类型的解：

• 验证过程中出现警告或错误
• 修改或删除原始的 requires 子句
• 弱化或删除原始的 ensures 子句
• 使用 :axiom 属性在无证明的情况下假设事实
• 使用 assume 语句绕过验证

我们的验证流程分为两个阶段：
首先，调用 Dafny 验证器并解析其 JSON 输出，以检测验证失败；
其次，通过一个提取流水线将每个问题引理解析为其签名、前提条件（preconditions）和后置条件（postconditions）。验证器随后比较原始规范与生成规范：

• requires 子句必须完全一致（不允许添加或删除）；
• ensures 子句必须是原始子句的超集（即允许添加更强的结论）。

  
  之所以允许增强后置条件，是因为强化后的引理仍能推出原始陈述——可以从更强版本推导出原引理。

此外，我们还会扫描代码中是否使用了 :axiom 属性或 assume 语句。关键的是，我们按源文件区分验证诊断信息：允许来自库文件（definitions.dfy、library.dfy），但问题文件本身（即提交的解）中的任何警告或错误都会导致拒绝。

当验证失败时，我们会返回结构化反馈，明确指出哪些子句被修改，或使用了哪些不健全的构造，从而支持模型在后续迭代中进行自我修正。

3 评估
我们在 miniF2F-Dafny 上评估了 Dafny 的基础自动化能力以及 12 个现成大语言模型（LLMs），以检验自动主动验证（auto-active verification）在自动化数学推理中的有效性。评估首先衡量 Dafny 基于 SMT 的自动化机制在无人工干预下能解决多少问题，然后评估现代 LLM 是否能为剩余问题提供证明提示以引导验证。

3.1 空证明基线
由 Z3 驱动的 Dafny 验证器在空证明（即无需任何人工证明步骤）的情况下，成功验证了 244 道测试题中的 99 题（40.6%）和 244 道验证题中的 109 题（44.7%）。我们对每道题运行 5 次，每次超时 30 秒，使用 Dafny 4.11.0 版本。该基线展示了 SMT 自动化的能力：那些在 Lean 等交互式定理证明器中需要显式证明项的问题，在 Dafny 中可被自动验证。例如，IMO 1959 第 1 题（图 1）在 Lean 中需要大量证明，但在 Dafny 中仅凭空证明即可通过。

3.2 LLM 引导的证明
对于空证明失败的问题，我们评估了 12 个现成 LLM 提供证明提示的能力。由于时间和算力限制，部分模型仅在问题子集上进行评估；此评估仍在进行中，后续将更新完整结果。

实验设置：每道题最多生成 N = 4
次，初始尝试后进行 E = 3 轮错误修正迭代（温度 T = 0.5 ，每条响应上限 8192 个词元）。验证失败时，我们从 Dafny 输出中提取错误轨迹，并将其追加到对话历史中用于迭代优化。模型通过 AWS Bedrock API 调用，包括：Claude（Sonnet 3.7、Sonnet 4、Sonnet 4.5、Haiku 4.5）、DeepSeek V3.1、Llama 4 Maverick 17B、GPT-OSS（20B、120B）以及 Qwen 3（32B、235B MoE、Coder 30B、Coder 480B MoE）。所有模型均未微调。

结果：表 1 展示了测试集上的 pass@4 结果。Claude Sonnet 4.5 表现最佳，达 55.7%，其次为 Claude Sonnet 3.7（55.2%）和 Qwen 3 235B MoE（54.3%）。多个模型集中在 43–50% 区间。主要在通用代码上训练的模型（如 DeepSeek V3.1、Llama 4 Maverick、GPT-OSS）缺乏 Dafny 特定知识，常混淆 Dafny 与 Lean 语法；相比之下，Claude 和 Qwen 系列的更大模型对 Dafny 的验证惯用法更熟悉。

LLM 生成的证明展现出不同层次的复杂性：

• 一端如 Qwen3 Coder 30B，用简洁的奇偶性论证解决了一道 AMC 12 关于素数乘积的问题（图 6）：通过断言 195 为奇数而相关偶数为偶数，使 Dafny 自动完成验证；
• 另一端如 Claude Sonnet 4，解决了 IMO 1964 一道困难的不等式问题（图 5）：引入了一个辅助的平方和恒等式引理。该证明展现了高阶数学推理：使用 calc 语句代数变换左侧表达式，构造三个非负的平方和项，并调用辅助引理建立不等式。

这些例子表明，现代 LLM 既能生成利用 SMT 自动化的简洁提示，也能提出涉及辅助引理和结构化推理的非平凡证明策略。附录提供了更多示例。

错误分析：对未验证问题的分析揭示了三类主要难点：

• 验证脆弱性（Verification brittleness）：断言顺序或 calc 语句组织的微小变化即可导致验证失败；
• Dafny 训练数据有限：模型对 calc 语句、ghost 变量等语言特有惯用法掌握不足，生成语法正确但语义无效的证明；
• 数学复杂性：问题所需数学事实未包含在库中，需从零开始构建理论。

讨论：结果表明，Dafny 的 SMT 自动化为奥数数学提供了强大基线，而现代 LLM 能有效提供证明提示进一步扩展其能力。顶尖模型在测试集上达到约 55%，相较 40% 的基线实现了超 35% 的相对提升。然而，仍有显著改进空间，尤其是在应对验证脆弱性及增强模型对 Dafny 特定证明模式的熟悉度方面。

4 相关工作
4.1 形式化数学推理基准
形式化数学推理基准通过证明助手提供自动验证机制，与 MATH [7] 和 GSM8K [6] 等非形式化基准形成对比——后者仅评估自然语言数学推理，缺乏对正确性的形式化保证。

miniF2F 基准 [24] 是一个基于 Lean 的基准，包含 488 道数学问题，选自 AIME、AMC、IMO 以及高中和大学本科数学课程内容，并分为各含 244 题的测试集与验证集。该基准已被翻译至 Isabelle、HOL Light 和 Metamath，这些系统均为交互式定理证明器，要求提供显式的证明项。

其他竞赛风格的基准包括：FIMO [10]，包含 IMO 短名单问题的 Lean 形式化；PutnamBench [17]，包含 William Lowell Putnam 数学竞赛的 Lean 问题，难度显著更高；ProofNet [2] 聚焦于大学数学教材中的 Lean 练习题；LeanDojo [23] 则提供了源自 Lean mathlib 库的数据集。

由于其规模适中、问题覆盖多样且支持多语言实现，miniF2F 仍是目前最广泛采用的基准。

4.2 面向交互式定理证明的人工智能
完整证明（whole-proof）方法生成完整的证明，并通过迭代优化直至通过验证。GPT-f [14] 首次在 Metamath 中开创了这一范式，随后 FMS-CL [13] 在 Lean 中跟进。近期的完整证明系统还包括 DeepSeek-Prover [22]、Seed-Prover [5] 和 Kimina-Prover [19]。

逐步式方法（Step-wise approaches）通过树搜索逐步构造证明，包括 HTPS [9]（Lean 和 Metamath）和 LLEMMA [3]（Lean）。在各类基准上的领先方法在完整证明与逐步式范式之间交替更迭。

混合系统（Hybrid systems）将非形式化推理与形式化验证相结合。例如 DSP [8] 和 LEGO-Prover [20] 在 Isabelle 中工作，先将自然语言证明转换为形式化草稿（formal sketches），再完成证明。

智能体框架（Agentic frameworks）通过协调多个组件来生成证明。相关系统包括 Lean 中的 COPRA [15]、ProverAgent [4]、ProofCompass [21] 和 HILBERT [18]。

领域专用方法（Domain-specific approaches）如 AlphaGeometry [16] 则针对特定问题类型，例如 IMO 几何题。

近期成功率显著提升：HILBERT 在 miniF2F 上达到 99.2%，在 PutnamBench 上达到 70.0%。多个系统在 IMO 2025 中实现金牌水平表现，包括提供形式化解答的 Seed-Prover 和 Aristotle [1]，以及 Google DeepMind 和 OpenAI 提供自然语言解答的系统。

5 未来工作
Dafny 专用训练：当前模型对 Dafny 语法和验证惯用法接触有限，常将其与交互式定理证明器混淆。一个关键局限在于它们无法判断 Z3 求解器能否自动解决子目标。在精选的 Dafny 语料上进行预训练，并在验证任务上微调，可提升模型对自动主动验证模式的熟悉度，并学会有效使用 calc 语句、断言位置安排和 ghost 变量。

智能体架构：类比于 Lean 中的 Aristotle [1]、Seed-Prover [5] 和 HILBERT [18] 等系统，可构建 Dafny 专用的智能体框架，协调证明搜索、引理合成与迭代优化，充分发挥程序合成与形式验证之间的协同效应。

可学习的引理库：LEGO-Prover [20] 展示了模型如何提取、泛化并缓存成功的证明策略作为可复用引理。将此方法适配到 Dafny，可实现跨问题的累积学习，从而更贴近人类数学实践。

6 结论
miniF2F-Dafny 是首次在纯数学推理领域探索自动主动验证的尝试——该领域传统上由交互式定理证明器主导。我们的结果展示了一种高效的分工模式：大语言模型提供高层指导，而基于 SMT 的自动化机制处理底层细节。这一范式充分发挥了自动推理与现代语言模型的互补优势。展望未来，我们预期自动主动验证与交互式定理证明将逐步融合——Lean 中近期引入的 grind 策略已体现出这一趋势。本工作指明了一条有前景的路径：通过这种协同效应，实现更易用、AI 辅助的形式化验证。

A 示例解法
本节展示了一些由大语言模型生成的代表性证明解法，以说明在 miniF2F-Dafny 中所采用的多样化证明策略。我们选取了若干示例，这些示例通过引入辅助引理展现了高阶数学推理能力，表明 Dafny 的验证机制与 LLM 生成的精确输出相结合，能够完整解决 IMO 级别的数学问题。

A.1 imo_1964_p2 的完整证明
Claude Sonnet 4 为 IMO 1964 第 2 题（第 4 节中已截断展示）生成的解法，展示了一种基于平方和分解（sum-of-squares decomposition）的高阶证明策略。该证明通过表明 3 a b c − LHS 可表示为若干平方项之和（每项均乘以由三角不等式导出的正系数），从而建立所需的不等式。此过程需要通过系统性的展开与项合并，证明一个辅助代数恒等式。借助这些辅助事实，Dafny 基于 SMT 求解器的后端成功验证了完整证明。

B 提示（Prompts）
B.1 初始证明合成提示
我们设计了一个初始模型提示，用于建立任务上下文与约束条件，如下所示。该提示强调必须保留原始问题规范，禁止使用不健全的构造（如公理、assume 假设），并鼓励策略性地使用 Dafny 惯用法，例如 calc 语句和断言。提示还明确要求模型对其引用的任何数学结论都必须给出证明，不得依赖未声明的“经典定理”。这一设计体现了我们的核心目标：评估模型的 证明合成能力 ，而非对已有库的检索或调用能力。

原文链接： https://arxiv.org/pdf/2512.10187