miniF2F-Dafny:通過自動驗(yàn)證的LLM引導(dǎo)的數(shù)學(xué)定理證明

miniF2F-Dafny:通過自動驗(yàn)證的LLM引導(dǎo)的數(shù)學(xué)定理證明

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

https://arxiv.org/pdf/2512.10187

摘 要

我們提出了 miniF2F-Dafny——首個將數(shù)學(xué)推理基準(zhǔn) miniF2F 翻譯至自動定理證明器 Dafny 的工作。此前，該基準(zhǔn)僅存在于交互式定理證明器中（Lean、Isabelle、HOL Light、Metamath）。我們發(fā)現(xiàn)，Dafny 的自動化能力在無需任何人工證明步驟（即空證明）的情況下，驗(yàn)證了測試集 244 題中的 99 題（40.6%）和驗(yàn)證集 244 題中的 109 題（44.7%）。對于空證明失敗的問題，我們評估了 12 個現(xiàn)成的大語言模型（LLMs）提供證明提示的能力。所測試的最佳模型通過迭代錯誤修正，達(dá)到了 55.7% 的 pass@4 成功率。這些初步結(jié)果凸顯了一種高效分工：LLM 提供高層指導(dǎo)，而自動化機(jī)制處理底層細(xì)節(jié)。我們的基準(zhǔn)數(shù)據(jù)已在 GitHub 上發(fā)布。

1 引 言

形式化數(shù)學(xué)推理長期以來被視為人類智能的標(biāo)志，既需要創(chuàng)造性洞見，也要求嚴(yán)謹(jǐn)?shù)倪壿嬔堇[。大語言模型（LLMs）的出現(xiàn)為自動化數(shù)學(xué)形式化——即將非形式化的數(shù)學(xué)陳述與證明翻譯為機(jī)器可驗(yàn)證的形式系統(tǒng)——開辟了新的可能路徑。

早期工作主要聚焦于 Lean、Isabelle 和 Coq 等交互式定理證明器（ITPs），但這些系統(tǒng)需要大量人工構(gòu)造證明：人類專家或 AI 系統(tǒng)必須為每一步邏輯推理提供顯式的證明項(xiàng)。

為評估 AI 輔助形式化定理證明的進(jìn)展，研究者開發(fā)了多個基準(zhǔn)。其中，miniF2F 基準(zhǔn)最初為 Lean 設(shè)計(jì)，包含 488 道數(shù)學(xué)問題，選自 AIME、AMC、IMO 以及高中和大學(xué)本科數(shù)學(xué)課程內(nèi)容，分為 244 題的測試集和 244 題的驗(yàn)證集。它已成為評估 AI 系統(tǒng)形式化數(shù)學(xué)推理能力的標(biāo)準(zhǔn)基準(zhǔn)。然而，所有現(xiàn)有翻譯版本（Lean、Isabelle、HOL Light、Metamath）均面向交互式定理證明器——這些系統(tǒng)自動化程度有限，證明過程需要大量人工干預(yù)。盡管近期方法在 Lean 的 miniF2F 上取得了優(yōu)異成果，但它們要么依賴于在形式化證明語料上大規(guī)模訓(xùn)練的專用模型，要么采用復(fù)雜的智能體框架來協(xié)調(diào)多個組件，以生成交互式定理證明器所需的詳細(xì)證明腳本。

我們提出 miniF2F-Dafny——首個將 miniF2F 基準(zhǔn)翻譯至自動主動驗(yàn)證語言（auto-active verification language）的工作。與交互式定理證明器不同，Dafny 圍繞由 SMT 求解器驅(qū)動的自動化推理能力構(gòu)建，提供了一種根本不同的范式：許多數(shù)學(xué)問題僅需極少甚至無需人工證明步驟即可被驗(yàn)證。這引發(fā)了一個關(guān)鍵問題：在自動主動驗(yàn)證器中降低的證明復(fù)雜性，是否能讓現(xiàn)成的 LLM 有效提供高層數(shù)學(xué)洞見——例如關(guān)鍵引理、證明策略或中間斷言——而將底層邏輯推理委托給自動化求解器？

我們發(fā)現(xiàn)，僅靠 Dafny 的自動化能力，就能在零人工輸入的情況下，通過空證明（empty proofs）解決 miniF2F 中 40–45% 的問題。對于剩余問題，我們評估了 12 個現(xiàn)成 LLM 提供證明提示以引導(dǎo) Dafny 自動化的能力。結(jié)果凸顯了一種高效的分工模式：LLM 無需生成完整證明，而是提供高層指導(dǎo)，自動化機(jī)制則處理底層細(xì)節(jié)。

我們的主要貢獻(xiàn)如下：? 我們提出了 miniF2F-Dafny，這是 miniF2F 首次被翻譯至自動主動驗(yàn)證語言。? 我們建立了基線結(jié)果：僅憑 Dafny 的自動化能力，在無需任何人工干預(yù)的情況下即可解決 40–45% 的問題。? 我們評估了 12 個現(xiàn)成 LLM 在需要人工引導(dǎo)的問題上提供證明提示的能力，最佳模型通過迭代修正達(dá)到 55.7% 的 pass@4 成功率。? 我們展示了 AI 輔助定理證明中“分工協(xié)作”的價值：自動化求解器處理底層邏輯步驟，而 LLM 專注于高層證明結(jié)構(gòu)。

2 miniF2F-Dafny 基準(zhǔn)
2.1 概述
miniF2F-Dafny 基準(zhǔn)包含 488 道數(shù)學(xué)問題（244 道測試題，244 道驗(yàn)證題），從 Lean 版本的 miniF2F 基準(zhǔn)翻譯而來。每個問題均被表述為一個 Dafny 引理（lemma），包含前提條件（requires 子句）和后置條件（ensures 子句），但證明體為空。任務(wù)是在空證明不足以通過 Dafny 驗(yàn)證器時，合成一個有效的證明。

問題陳述可自然地從 Lean 轉(zhuǎn)換至 Dafny，如圖 1 所示。問題涵蓋多個數(shù)學(xué)領(lǐng)域，包括代數(shù)、數(shù)論、不等式、組合數(shù)學(xué)和分析。每個子集（測試集與驗(yàn)證集）均包含 45 道 AMC 題、15 道 AIME 題和 20 道 IMO 題，其余題目選自大學(xué)本科數(shù)學(xué)課程。該基準(zhǔn)同時考察系統(tǒng)提供高層證明策略（如引理調(diào)用、分情況討論、歸納法）和底層證明細(xì)節(jié)（如代數(shù)運(yùn)算、不等式鏈）的能力。

兩個輔助文件提供了數(shù)學(xué)基礎(chǔ)設(shè)施，盡管目前仍處于開發(fā)中。definitions.dfy 文件（300 行）對 Dafny 原生不支持的核心數(shù)學(xué)結(jié)構(gòu)進(jìn)行了公理化：整數(shù)、有理數(shù)、實(shí)數(shù)和復(fù)數(shù)，及其運(yùn)算與性質(zhì)。library.dfy 文件（550 行）包含 108 條公理化的引理，編碼了關(guān)于指數(shù)函數(shù)、對數(shù)、三角函數(shù)、復(fù)數(shù)和數(shù)論的標(biāo)準(zhǔn)數(shù)學(xué)事實(shí)。原則上這些引理可被證明，但我們選擇公理化它們，以將評估重點(diǎn)放在利用 SMT 自動化進(jìn)行證明合成上。我們并未投入大量精力構(gòu)建深層庫，而是旨在測試現(xiàn)代 AI 系統(tǒng)在使用 Dafny 的霍爾邏輯（Hoare-logic）風(fēng)格規(guī)范和 SMT 求解器自動化能力時，能多好地生成證明。

2.2 定義
該基準(zhǔn)的數(shù)學(xué)基礎(chǔ)由 definitions.dfy 提供，其中公理化了在 Dafny 中表達(dá)所有 miniF2F 問題所需的最小數(shù)學(xué)基礎(chǔ)設(shè)施。與 Mathlib [12]（其中數(shù)學(xué)對象從第一性原理構(gòu)造）不同，我們的公理化策略體現(xiàn)了 Dafny 的設(shè)計(jì)哲學(xué)：即依賴 SMT 求解器的能力，從一個可信的定義庫出發(fā)進(jìn)行自動化推理，而非要求構(gòu)建龐大的形式化證明庫。

這些定義覆蓋四個數(shù)域：整數(shù)、有理數(shù)、實(shí)數(shù)和復(fù)數(shù)。每個數(shù)域均包含標(biāo)準(zhǔn)算術(shù)運(yùn)算及領(lǐng)域特定的函數(shù)。

• 整數(shù)支持有限集上的求和與求積、模運(yùn)算以及整除性謂詞。
• 有理數(shù)被顯式表示為分子–分母對，并配備分?jǐn)?shù)算術(shù)。
• 實(shí)數(shù)包含超越函數(shù)（指數(shù)、對數(shù)、三角函數(shù)）、冪運(yùn)算以及數(shù)學(xué)常數(shù)（如 π）。
• 復(fù)數(shù)提供域運(yùn)算、范數(shù)函數(shù)和復(fù)指數(shù)函數(shù)。

該公理化采用 Dafny 的 :axiom 屬性，通過規(guī)范（specifications）而非具體實(shí)現(xiàn)來聲明函數(shù)。規(guī)范的復(fù)雜度因函數(shù)性質(zhì)而異：

• 對于對數(shù)等超越函數(shù)（見圖 3），我們公理化其基本值域性質(zhì)——例如，規(guī)定當(dāng)自變量大于 1 時對數(shù)為正，在 0 到 1 之間時為負(fù)，在 1 處為零。
• 對于求和等遞歸函數(shù)（見圖 2），我們通過后置條件（postconditions）復(fù)現(xiàn)歸納定義：明確其在空集上的行為，以及在非空集上通過移除一個元素后的遞歸行為。
• 數(shù)論函數(shù)（如 gcd、lcm、素數(shù)判定）、組合函數(shù)（如 choose、階乘）和工具函數(shù)（如 floor、ceil、abs）也以類似方式公理化。

這些契約（contracts）為 Dafny 基于 SMT 的自動化機(jī)制提供了足夠的語義信息，使其能在許多問題上僅憑空證明即可完成驗(yàn)證。盡管這些公理化遵循標(biāo)準(zhǔn)數(shù)學(xué)定義，且我們對其正確性持謹(jǐn)慎信心，但這種實(shí)用主義方法仍不可避免地帶來公理化本身固有的可靠性（soundness）考量。

2.3 庫（Library）

作為定義的補(bǔ)充，library.dfy 提供了 108 條公理化的引理，編碼了標(biāo)準(zhǔn)數(shù)學(xué)事實(shí)。該庫采用問題驅(qū)動的開發(fā)方式：通過分析證明嘗試過程，識別出所需的事實(shí)，再將這些引理與 Mathlib [12] 中的定理進(jìn)行交叉核對以確保其可靠性，之后才集成進(jìn)來。

我們并未提供這些引理的構(gòu)造性證明，而是直接將其公理化，使問題能夠調(diào)用已確立的結(jié)果而無需重新證明——這模仿了數(shù)學(xué)實(shí)踐中的常見做法：引用已知定理，而非從頭重建。這些引理涵蓋多個數(shù)學(xué)領(lǐng)域：

• 指數(shù)/對數(shù)（27 條引理）：指數(shù)相乘、對數(shù)相加、換底公式（見圖 4）
• 冪運(yùn)算（8 條引理）：自然數(shù)與實(shí)數(shù)指數(shù)、冪律、平方根
• 三角學(xué)（37 條引理）：角加法公式、周期性、特殊值、畢達(dá)哥拉斯恒等式
• 復(fù)數(shù)（19 條引理）：域公理、范數(shù)性質(zhì)、歐拉公式
• 數(shù)論（5 條引理）：最大公約數(shù)（GCD）交換律、GCD–LCM 乘積公式
• 分析（4 條引理）：極限唯一性、連續(xù)性性質(zhì)
• 數(shù)列（8 條引理）：序列求和與求積、集合轉(zhuǎn)換

每條引理均通過前提條件（requires）和后置條件（ensures）進(jìn)行規(guī)范。例如，對數(shù)換底公式（圖 4）要求底數(shù)為正且不等于 1，并確保不同底數(shù)對數(shù)之間的標(biāo)準(zhǔn)關(guān)系成立。此外，某些數(shù)學(xué)性質(zhì)（如結(jié)合律、可加性）無法自然地編碼為單個函數(shù)的后置條件，而必須作為獨(dú)立引理顯式陳述。

該庫的規(guī)模（550 行）相比 Mathlib 的 200 萬行有意保持極簡，聚焦于奧林匹克級別數(shù)學(xué)所需的前置知識。這體現(xiàn)了一種務(wù)實(shí)的平衡：提供足夠理論以表達(dá)并求解 miniF2F 問題，同時測試 AI 系統(tǒng)能否在緊湊的基礎(chǔ)之上，有效利用 SMT 自動化能力構(gòu)建證明。

該庫很可能并不完備，若補(bǔ)充更多引理，評估結(jié)果很可能會進(jìn)一步提升。

2.4 驗(yàn)證
我們基準(zhǔn)測試的一個關(guān)鍵組成部分是驗(yàn)證所生成的解是否嚴(yán)格遵循原始問題陳述，而不對其弱化。這可以防止解決方案通過加強(qiáng)前提條件、弱化結(jié)論條件或引入不健全的公理來“作弊”——我們在其他基準(zhǔn)（如 DafnyBench [11]）中已觀察到此類問題，其薄弱的評估腳本允許這類違規(guī)行為。

對于一個以 Dafny 引理形式給出的問題，我們的驗(yàn)證器會拒絕以下類型的解：

• 驗(yàn)證過程中出現(xiàn)警告或錯誤
• 修改或刪除原始的 requires 子句
• 弱化或刪除原始的 ensures 子句
• 使用 :axiom 屬性在無證明的情況下假設(shè)事實(shí)
• 使用 assume 語句繞過驗(yàn)證

我們的驗(yàn)證流程分為兩個階段：
首先，調(diào)用 Dafny 驗(yàn)證器并解析其 JSON 輸出，以檢測驗(yàn)證失敗；
其次，通過一個提取流水線將每個問題引理解析為其簽名、前提條件（preconditions）和后置條件（postconditions）。驗(yàn)證器隨后比較原始規(guī)范與生成規(guī)范：

• requires 子句必須完全一致（不允許添加或刪除）；
• ensures 子句必須是原始子句的超集（即允許添加更強(qiáng)的結(jié)論）。

  
  之所以允許增強(qiáng)后置條件，是因?yàn)閺?qiáng)化后的引理仍能推出原始陳述——可以從更強(qiáng)版本推導(dǎo)出原引理。

此外，我們還會掃描代碼中是否使用了 :axiom 屬性或 assume 語句。關(guān)鍵的是，我們按源文件區(qū)分驗(yàn)證診斷信息：允許來自庫文件（definitions.dfy、library.dfy），但問題文件本身（即提交的解）中的任何警告或錯誤都會導(dǎo)致拒絕。

當(dāng)驗(yàn)證失敗時，我們會返回結(jié)構(gòu)化反饋，明確指出哪些子句被修改，或使用了哪些不健全的構(gòu)造，從而支持模型在后續(xù)迭代中進(jìn)行自我修正。

3 評估
我們在 miniF2F-Dafny 上評估了 Dafny 的基礎(chǔ)自動化能力以及 12 個現(xiàn)成大語言模型（LLMs），以檢驗(yàn)自動主動驗(yàn)證（auto-active verification）在自動化數(shù)學(xué)推理中的有效性。評估首先衡量 Dafny 基于 SMT 的自動化機(jī)制在無人工干預(yù)下能解決多少問題，然后評估現(xiàn)代 LLM 是否能為剩余問題提供證明提示以引導(dǎo)驗(yàn)證。

3.1 空證明基線
由 Z3 驅(qū)動的 Dafny 驗(yàn)證器在空證明（即無需任何人工證明步驟）的情況下，成功驗(yàn)證了 244 道測試題中的 99 題（40.6%）和 244 道驗(yàn)證題中的 109 題（44.7%）。我們對每道題運(yùn)行 5 次，每次超時 30 秒，使用 Dafny 4.11.0 版本。該基線展示了 SMT 自動化的能力：那些在 Lean 等交互式定理證明器中需要顯式證明項(xiàng)的問題，在 Dafny 中可被自動驗(yàn)證。例如，IMO 1959 第 1 題（圖 1）在 Lean 中需要大量證明，但在 Dafny 中僅憑空證明即可通過。

3.2 LLM 引導(dǎo)的證明
對于空證明失敗的問題，我們評估了 12 個現(xiàn)成 LLM 提供證明提示的能力。由于時間和算力限制，部分模型僅在問題子集上進(jìn)行評估；此評估仍在進(jìn)行中，后續(xù)將更新完整結(jié)果。

實(shí)驗(yàn)設(shè)置：每道題最多生成 N = 4
次，初始嘗試后進(jìn)行 E = 3 輪錯誤修正迭代（溫度 T = 0.5 ，每條響應(yīng)上限 8192 個詞元）。驗(yàn)證失敗時，我們從 Dafny 輸出中提取錯誤軌跡，并將其追加到對話歷史中用于迭代優(yōu)化。模型通過 AWS Bedrock API 調(diào)用，包括：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）。所有模型均未微調(diào)。

結(jié)果：表 1 展示了測試集上的 pass@4 結(jié)果。Claude Sonnet 4.5 表現(xiàn)最佳，達(dá) 55.7%，其次為 Claude Sonnet 3.7（55.2%）和 Qwen 3 235B MoE（54.3%）。多個模型集中在 43–50% 區(qū)間。主要在通用代碼上訓(xùn)練的模型（如 DeepSeek V3.1、Llama 4 Maverick、GPT-OSS）缺乏 Dafny 特定知識，常混淆 Dafny 與 Lean 語法；相比之下，Claude 和 Qwen 系列的更大模型對 Dafny 的驗(yàn)證慣用法更熟悉。

LLM 生成的證明展現(xiàn)出不同層次的復(fù)雜性：

• 一端如 Qwen3 Coder 30B，用簡潔的奇偶性論證解決了一道 AMC 12 關(guān)于素數(shù)乘積的問題（圖 6）：通過斷言 195 為奇數(shù)而相關(guān)偶數(shù)為偶數(shù)，使 Dafny 自動完成驗(yàn)證；
• 另一端如 Claude Sonnet 4，解決了 IMO 1964 一道困難的不等式問題（圖 5）：引入了一個輔助的平方和恒等式引理。該證明展現(xiàn)了高階數(shù)學(xué)推理：使用 calc 語句代數(shù)變換左側(cè)表達(dá)式，構(gòu)造三個非負(fù)的平方和項(xiàng)，并調(diào)用輔助引理建立不等式。

這些例子表明，現(xiàn)代 LLM 既能生成利用 SMT 自動化的簡潔提示，也能提出涉及輔助引理和結(jié)構(gòu)化推理的非平凡證明策略。附錄提供了更多示例。

錯誤分析：對未驗(yàn)證問題的分析揭示了三類主要難點(diǎn)：

• 驗(yàn)證脆弱性（Verification brittleness）：斷言順序或 calc 語句組織的微小變化即可導(dǎo)致驗(yàn)證失敗；
• Dafny 訓(xùn)練數(shù)據(jù)有限：模型對 calc 語句、ghost 變量等語言特有慣用法掌握不足，生成語法正確但語義無效的證明；
• 數(shù)學(xué)復(fù)雜性：問題所需數(shù)學(xué)事實(shí)未包含在庫中，需從零開始構(gòu)建理論。

討論：結(jié)果表明，Dafny 的 SMT 自動化為奧數(shù)數(shù)學(xué)提供了強(qiáng)大基線，而現(xiàn)代 LLM 能有效提供證明提示進(jìn)一步擴(kuò)展其能力。頂尖模型在測試集上達(dá)到約 55%，相較 40% 的基線實(shí)現(xiàn)了超 35% 的相對提升。然而，仍有顯著改進(jìn)空間，尤其是在應(yīng)對驗(yàn)證脆弱性及增強(qiáng)模型對 Dafny 特定證明模式的熟悉度方面。

4 相關(guān)工作
4.1 形式化數(shù)學(xué)推理基準(zhǔn)
形式化數(shù)學(xué)推理基準(zhǔn)通過證明助手提供自動驗(yàn)證機(jī)制，與 MATH [7] 和 GSM8K [6] 等非形式化基準(zhǔn)形成對比——后者僅評估自然語言數(shù)學(xué)推理，缺乏對正確性的形式化保證。

miniF2F 基準(zhǔn) [24] 是一個基于 Lean 的基準(zhǔn)，包含 488 道數(shù)學(xué)問題，選自 AIME、AMC、IMO 以及高中和大學(xué)本科數(shù)學(xué)課程內(nèi)容，并分為各含 244 題的測試集與驗(yàn)證集。該基準(zhǔn)已被翻譯至 Isabelle、HOL Light 和 Metamath，這些系統(tǒng)均為交互式定理證明器，要求提供顯式的證明項(xiàng)。

其他競賽風(fēng)格的基準(zhǔn)包括：FIMO [10]，包含 IMO 短名單問題的 Lean 形式化；PutnamBench [17]，包含 William Lowell Putnam 數(shù)學(xué)競賽的 Lean 問題，難度顯著更高；ProofNet [2] 聚焦于大學(xué)數(shù)學(xué)教材中的 Lean 練習(xí)題；LeanDojo [23] 則提供了源自 Lean mathlib 庫的數(shù)據(jù)集。

由于其規(guī)模適中、問題覆蓋多樣且支持多語言實(shí)現(xiàn)，miniF2F 仍是目前最廣泛采用的基準(zhǔn)。

4.2 面向交互式定理證明的人工智能
完整證明（whole-proof）方法生成完整的證明，并通過迭代優(yōu)化直至通過驗(yàn)證。GPT-f [14] 首次在 Metamath 中開創(chuàng)了這一范式，隨后 FMS-CL [13] 在 Lean 中跟進(jìn)。近期的完整證明系統(tǒng)還包括 DeepSeek-Prover [22]、Seed-Prover [5] 和 Kimina-Prover [19]。

逐步式方法（Step-wise approaches）通過樹搜索逐步構(gòu)造證明，包括 HTPS [9]（Lean 和 Metamath）和 LLEMMA [3]（Lean）。在各類基準(zhǔn)上的領(lǐng)先方法在完整證明與逐步式范式之間交替更迭。

混合系統(tǒng)（Hybrid systems）將非形式化推理與形式化驗(yàn)證相結(jié)合。例如 DSP [8] 和 LEGO-Prover [20] 在 Isabelle 中工作，先將自然語言證明轉(zhuǎn)換為形式化草稿（formal sketches），再完成證明。

智能體框架（Agentic frameworks）通過協(xié)調(diào)多個組件來生成證明。相關(guān)系統(tǒng)包括 Lean 中的 COPRA [15]、ProverAgent [4]、ProofCompass [21] 和 HILBERT [18]。

領(lǐng)域?qū)Ｓ梅椒ǎ―omain-specific approaches）如 AlphaGeometry [16] 則針對特定問題類型，例如 IMO 幾何題。

近期成功率顯著提升：HILBERT 在 miniF2F 上達(dá)到 99.2%，在 PutnamBench 上達(dá)到 70.0%。多個系統(tǒng)在 IMO 2025 中實(shí)現(xiàn)金牌水平表現(xiàn)，包括提供形式化解答的 Seed-Prover 和 Aristotle [1]，以及 Google DeepMind 和 OpenAI 提供自然語言解答的系統(tǒng)。

5 未來工作
Dafny 專用訓(xùn)練：當(dāng)前模型對 Dafny 語法和驗(yàn)證慣用法接觸有限，常將其與交互式定理證明器混淆。一個關(guān)鍵局限在于它們無法判斷 Z3 求解器能否自動解決子目標(biāo)。在精選的 Dafny 語料上進(jìn)行預(yù)訓(xùn)練，并在驗(yàn)證任務(wù)上微調(diào)，可提升模型對自動主動驗(yàn)證模式的熟悉度，并學(xué)會有效使用 calc 語句、斷言位置安排和 ghost 變量。

智能體架構(gòu)：類比于 Lean 中的 Aristotle [1]、Seed-Prover [5] 和 HILBERT [18] 等系統(tǒng)，可構(gòu)建 Dafny 專用的智能體框架，協(xié)調(diào)證明搜索、引理合成與迭代優(yōu)化，充分發(fā)揮程序合成與形式驗(yàn)證之間的協(xié)同效應(yīng)。

可學(xué)習(xí)的引理庫：LEGO-Prover [20] 展示了模型如何提取、泛化并緩存成功的證明策略作為可復(fù)用引理。將此方法適配到 Dafny，可實(shí)現(xiàn)跨問題的累積學(xué)習(xí)，從而更貼近人類數(shù)學(xué)實(shí)踐。

6 結(jié)論
miniF2F-Dafny 是首次在純數(shù)學(xué)推理領(lǐng)域探索自動主動驗(yàn)證的嘗試——該領(lǐng)域傳統(tǒng)上由交互式定理證明器主導(dǎo)。我們的結(jié)果展示了一種高效的分工模式：大語言模型提供高層指導(dǎo)，而基于 SMT 的自動化機(jī)制處理底層細(xì)節(jié)。這一范式充分發(fā)揮了自動推理與現(xiàn)代語言模型的互補(bǔ)優(yōu)勢。展望未來，我們預(yù)期自動主動驗(yàn)證與交互式定理證明將逐步融合——Lean 中近期引入的 grind 策略已體現(xiàn)出這一趨勢。本工作指明了一條有前景的路徑：通過這種協(xié)同效應(yīng)，實(shí)現(xiàn)更易用、AI 輔助的形式化驗(yàn)證。

A 示例解法
本節(jié)展示了一些由大語言模型生成的代表性證明解法，以說明在 miniF2F-Dafny 中所采用的多樣化證明策略。我們選取了若干示例，這些示例通過引入輔助引理展現(xiàn)了高階數(shù)學(xué)推理能力，表明 Dafny 的驗(yàn)證機(jī)制與 LLM 生成的精確輸出相結(jié)合，能夠完整解決 IMO 級別的數(shù)學(xué)問題。

A.1 imo_1964_p2 的完整證明
Claude Sonnet 4 為 IMO 1964 第 2 題（第 4 節(jié)中已截斷展示）生成的解法，展示了一種基于平方和分解（sum-of-squares decomposition）的高階證明策略。該證明通過表明 3 a b c ? LHS 可表示為若干平方項(xiàng)之和（每項(xiàng)均乘以由三角不等式導(dǎo)出的正系數(shù)），從而建立所需的不等式。此過程需要通過系統(tǒng)性的展開與項(xiàng)合并，證明一個輔助代數(shù)恒等式。借助這些輔助事實(shí)，Dafny 基于 SMT 求解器的后端成功驗(yàn)證了完整證明。

B 提示（Prompts）
B.1 初始證明合成提示
我們設(shè)計(jì)了一個初始模型提示，用于建立任務(wù)上下文與約束條件，如下所示。該提示強(qiáng)調(diào)必須保留原始問題規(guī)范，禁止使用不健全的構(gòu)造（如公理、assume 假設(shè)），并鼓勵策略性地使用 Dafny 慣用法，例如 calc 語句和斷言。提示還明確要求模型對其引用的任何數(shù)學(xué)結(jié)論都必須給出證明，不得依賴未聲明的“經(jīng)典定理”。這一設(shè)計(jì)體現(xiàn)了我們的核心目標(biāo)：評估模型的 證明合成能力 ，而非對已有庫的檢索或調(diào)用能力。

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