# LLM 與形式推理的交會：邁向 AI 證明輔助與自動形式化的未來

## 前言

近年來，人工智慧在數學與程式設計領域的表現成為評估智慧程度的核心指標。由於數學問題可驗證、推理明確，使其成為測試 AI 理解與推論能力的重要場域。Kaiyu Yang 的演講《Formal Reasoning Meets LLMs: Towards AI for Mathematics and Verification》詳述了目前大型語言模型（LLMs）在數學與形式邏輯中的應用現況、挑戰與前瞻。本文將依據該演講內容整理出技術重點，提供中文繁體版本的專業導讀。

## 1. AI 於數學與程式設計領域的開發軍備賽

### 全球競逐趨勢

AI 在數學與程式設計的應用已成為科技巨頭的戰略焦點。OpenAI、Google、xAI 等公司不斷推出具備數學推理能力的模型：

* OpenAI 的 o1 與 o3、Google 的 Gemini、xAI 的 Grok 等皆強調其數學與程式設計能力。
* 為激勵技術突破，XTX Markets 提供 1,000 萬美元獎金，獎勵能夠在國際數學奧林匹亞（IMO）中奪得金牌的 AI 系統。
* Google DeepMind 開發的 AlphaProof 與 AlphaGeometry，已在 IMO 水準題目達到銀牌表現。
* Epoch AI 提出的 FrontierMath 基準測試涵蓋研究等級的數學問題，o3 在該測試中解出超過 20% 題目，展現突破性進展。

### 推理與可驗證性作為能力代表

數學與程式設計之所以受重視，主要因其具備以下特性：

* **推理與規劃能力的代表性（Proxy for Reasoning & Planning）**：是實現泛用 AI 的核心能力。
* **易於客觀評估（Evaluatable Tasks）**：

* 數學可直接驗證答案正確性。
* 程式設計可使用單元測試確認功能是否正確。
* 相對於文學創作或音樂生成，具備可量化標準。

因此，數學與程式領域的突破可望帶動更廣泛推理型應用場景，如行程安排、規劃工具、知識推導等。

## 2. 如何訓練 LLM 解數學問題？

訓練能解數學題的大型語言模型需倚賴兩大主流方法：

### 2.1 監督式微調（Supervised Fine-tuning, SFT）

* 核心概念為「好的資料就是一切所需（Good data is all you need）」。
* 將已在文字與程式碼預訓練的 LLM，持續預訓練於數學相關語料上。
* 使用含有題目與詳解步驟的數據集進行微調，建立模型的推理鏈能力。
* 資料準備需仰賴大量人工註解、清理與轉換，目前最大公開資料集規模約為 90 萬題。
* 若結合工具（如計算器、程式執行器）使用，可打造具互動能力的 Tool-integrated LLM。

### 2.2 強化學習（Reinforcement Learning, RL）

* 核心概念為「可驗證性就是一切所需（Verifiability is all you need）」。
* 當訓練資料僅有最終答案時，模型需自行生成包含中間推理的完整解法。
* 將解答與正確答案比較後給予獎勵（正確為 1，錯誤為 0），作為 RL 的回饋訊號。
* DeepSeek-R1 系列為推動此方法的代表。
* 此類訓練流程需確保問題具可驗證性（如具明確數值解），否則獎勵無法計算。
* 對於需撰寫正式證明的高階數學題型不適用。

### 綜合觀察

目前最先進的數學 LLM 結構＝強大預訓練模型 + 精選資料微調 + 可驗證性強化學習 + 高效工程設計。

演算法層面相對直接，但實際成效高度依賴：

* 大規模高品質資料建置
* 工具整合能力（如程式執行器、計算工具）
* 訓練基礎設施與成本考量

## 3. LLM 的推理落差與限制

儘管 LLM 在解題準確率上已有明顯進展，但在數學推理應用上仍存在顯著瓶頸，主要表現於下列兩個方面：

### 3.1 從基礎數學到高階數學的落差

* 目前 LLM 的成功範圍主要集中在學前與高中程度的數學題（如 IMO、AIME）。
* 當問題提升至大學與研究等級，模型表現明顯下滑。
* 研究級數學本質新穎，缺乏可訓練的公開資料集。
* FrontierMath 雖提供可驗證的高階題目，但其偏向具結構的數值解，與真實研究題型仍有落差。

### 3.2 從猜答案到撰寫形式證明的落差

* 多數 LLM 雖能猜出正確數值解，但在撰寫完整且邏輯嚴謹的證明方面表現不佳。
* PutnamBench 與 USAMO 等評測指出，目前 LLM 的證明得分偏低（多為 1–2 分或正確率 5% 以下）。
* 錯誤來源常為簡單邏輯失誤，卻因證明步驟繁複而難以覺察與修正。

### 資料與驗證性的限制

* 現階段的數學 LLM 訓練高度依賴兩要素：資料量與答案可驗證性。
* 多數 LLM 無法處理缺乏數據或需撰寫證明的問題情境。
* 缺乏能處理證明結構與邏輯回饋的訓練環境，限制其泛化能力。

針對這些限制，形式系統（formal systems）與互動式定理證明器（ITPs）正成為突破瓶頸的關鍵路徑。

## 4. 形式推理與 LLM 的整合

形式推理提供了克服資料與驗證性限制的架構。其核心概念是：

* 使用形式系統（如一階邏輯、依賴型別理論等）構建嚴謹推理過程。
* 引入互動式定理證明器（ITPs），如 Lean、Coq 等作為語言與驗證環境。
* 結合 LLM 的語言理解能力與 ITPs 的結構嚴謹性，進行高可靠度的推理。

以 Lean 為例：

* Lean 是定理證明器、互動輔助證明系統與程式語言三合一工具。
* 其開源專案 Mathlib 提供龐大的數學知識庫。
* 每個證明皆以形式表示，並可由編譯器驗證其正確性，完全排除 LLM 的幻覺錯誤。

此類系統建構方式，類似軟體工程中的模組化設計，每個檔案對應一個證明任務，且皆可重現與開源。

## 5. AlphaProof 與 LeanDojo：實作中的 AI 證明器

目前已有數個專案探索將 LLM 應用於定理證明：

### AlphaProof

* 結合 Lean 系統與強化學習，將 Lean 驗證結果作為回饋訊號。
* 使用大規模證明樹搜索與策略學習。

### LeanDojo

* 開源的定理證明研究平台。
* 提供大量 Lean 程式碼作為訓練與測試資料。
* 將證明過程分解為 tactic（推理步驟）、premise（前提選擇）等元素，利於模組化訓練。
* 提出 ReProver 模型，結合檢索式策略與語言模型，顯著提升 Lean 定理的證明成功率。
* 具備低成本（僅需 1 週 GPU 訓練）與可重現性。

這些系統證明了：即使在資料稀缺的形式數學領域，只要設計良好、結構清晰，也能使 LLM 有效執行推理任務。

## 6. 自動形式化的挑戰與進展

自動形式化（Autoformalization）意指將自然語言中的數學敘述轉換為可由定理證明器處理的形式化表示。

### 難點一：定理敘述的形式轉換

* 不同語意表達在邏輯上是否等價，往往無法自動判定。
* 目前尚缺乏可靠的自動評估方法，只能依賴人工標註。

### 難點二：證明內容的邏輯填補

* 自然語言證明常省略步驟（如留給讀者證明）。
* 模型須自行補全邏輯空白，這對於語言模型而言仍具高度挑戰性。

即便使用 GPT-4 與 Vision 模型，自動形式化的準確率仍低於 20%，凸顯此議題仍屬長期挑戰。

## 7. 幾何證明與圖形推理的形式處理

以歐幾里得幾何為例，圖形直觀推理無法在形式系統中直接表達：

* Lean 不理解「圖中明顯」的幾何特性（如兩圓相交）。
* 需建構額外的圖形邏輯規則，例如 Avigad 提出的「圖形隱含公理」。
* 可使用 SMT solver 進行圖形事實的邏輯推導，讓形式證明器具備圖形推理能力。

LeanEuclid 即為一整合自動形式化與圖形推理評測的平台，針對《原本》第一冊與 UniGeo 問題，提供完整的地面真實、圖形與自然語言敘述，協助檢驗自動形式化流程的正確性。

上述七大段落涵蓋 LLM 與形式邏輯交會的最新發展。下一部分將總結關鍵觀察與未來可能的研究方向。

## 8. 結語與未來展望

隨著大型語言模型在自然語言處理與知識推理上的能力持續進展，將其導入數學與邏輯證明領域已成為當前的前沿挑戰。從本文分析可歸納出以下關鍵觀察：

1. LLM 雖具備語言與模式學習優勢，但在邏輯完備性與驗證正確性上仍存在結構性限制。

2. 整合形式系統（如 Lean）與語言模型，可利用驗證機制與開放知識庫提供更嚴謹且可重複的推理基礎。
3. 針對特定數學子領域（如不等式、幾何），能透過引入符號推理與圖形邏輯進行行動空間重塑，改善模型效率與正確率。
4. 自動形式化仍為長期挑戰，需解決語意對齊、邏輯空白補全與等價檢查等根本問題。

未來的研究方向可聚焦於：

1.發展跨領域學習架構，使 LLM 能在語言與形式邏輯之間無縫切換。

2.建立更具標準化與可驗證性的訓練資料集，並拓展至研究等級數學。

3.將互動式證明流程模組化，開發以學習者為中心的 AI 證明輔助工具。

4.深化圖形推理建模與 SMT-based 驗證整合，提升幾何與空間推理效能。

整體而言，形式邏輯與 LLM 的結合為 AI 理性推理帶來嶄新可能。未來的 AI 若能於形式證明中展現與人類相當甚至超越的能力，將重塑我們對人工智慧推理極限的理解。

## 參考來源
1. Kaiyu Yang, Formal Reasoning Meets LLMs: Towards AI for Mathematics and Verification, 2024 演講稿與簡報。

1. AlphaProof – Google DeepMind, Formal Proof Search with Reinforcement Learning in Lean
https://arxiv.org/abs/2312.10407

1. LeanDojo – Open-source framework for theorem proving with LLMs
GitHub: https://github.com/lean-dojo/LeanDojo

1. FrontierMath Benchmark – OpenAI
https://openai.com/research/frontiermath

1. LIPS: An LLM-based Inequality Prover with Symbolic Reasoning – 2023
https://arxiv.org/abs/2311.08912

1. LeanEuclid – Autoformalization and evaluation on Euclidean geometry
https://github.com/lean-dojo/LeanEuclid

1. AlphaGeometry – Symbolic and Neural reasoning for Euclidean geometry
https://arxiv.org/abs/2401.01041

1. Mathlib – The Lean mathematical library
https://github.com/leanprover-community/mathlib4

1. DeepSeek-RL – A Reinforcement Learning framework for reasoning
https://github.com/deepseek-ai/DeepSeek-RL

1. PutnamBench – A benchmark for mathematical reasoning evaluation
https://github.com/OpenLMLab/PutnamBench