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 輸出，以檢測驗證失?。?br/>其次，通過一個提取流水線將每個問題引理解析為其簽名、前提條件（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