## 以大型語言模型驅動的數學與科學探索

### 第一章：導論

本篇文章探討了大型語言模型（LLMs）如何應用於形式化數學證明與科學發現，並介紹了目前相關領域的研究進展。從與形式化證明系統如 Lean 的互動、到自動化證明策略（如 COPRA）、再到將 LLM 結合符號回歸（symbolic regression）實作實證科學中的概念抽象與方程探索，本文逐步展示了 LLM 作為代理人（agent）在自動化推理中的潛力。

### 第二章：LLM與形式化證明系統的互動機制

形式化證明助手（proof assistant）如 Lean、Coq 提供了結構化語法與邏輯檢查機制，協助使用者構建嚴謹的數學證明。這些系統基於狀態機設計：每個證明狀態對應一組開放目標（goals），而每一步 tactics 的應用則改變證明狀態。最終目標是將所有目標消解至無剩（即達成 QED 狀態）。

LLM 在此任務中扮演策略預測角色：

1. 接收目前 proof state（證明狀態）作為提示（prompt）。
2. 預測下一步可能的 tactic（策略）。
3. 試圖執行該策略於 proof assistant（如 Lean）中。
4. 根據執行是否成功，回饋結果並更新提示。

這種互動提供即時錯誤回報與可擴展的驗證流程，減少 hallucination 並引導 LLM 調整推理路徑。

### 第三章：COPRA系統設計與實作

COPRA（Conversational Proof Reasoning Agent）是一個以 LLM 為核心，結合 proof assistant 進行互動式數學證明的系統。

核心流程如下：

1. 給定定理的正式描述（formal theorem），可搭配非正式語言提示（optional informal hints）。
2. 建立初始提示，包含目前證明目標、假設與歷史操作堆疊。
3. 使用 frontier LLM（如 GPT-4, o1, o3）預測可能的 tactic。
4. 將 tactic 文本解析為結構化格式並執行。
5. 根據結果（成功或錯誤）更新 prompt 並回饋給 LLM，進入下一回合。

COPRA 實作了深度優先搜尋策略（DFS），並結合類似 retrieval-augmented generation 的 lemma 檢索機制，用以強化推理表現。

### 第四章：分層推理與高階提示策略

COPRA 展現的不僅是低階 tactic 預測能力，也可透過 prompting 策略提升為高階推理代理人。具體作法如下：

1. 針對複雜問題（如 IMO 題），先請 LLM 生成非正式推理步驟。
2. 依據此推理架構，請 LLM 生成對應的子目標（subgoals）。
3. 將子目標分別交由 COPRA 處理，逐一建立子證明。
4. 回收各子證明，統整為主定理證明。

這樣的「問題拆解 - 層級化建構 - 子任務求解 - 全域整合」流程可視為一種階層式規劃（hierarchical planning），進一步發揮 LLM 的語意抽象與概念結構能力。

### 第五章：形式系統驗證的應用案例

LLM + proof assistant 架構可應用於正式系統驗證（formal verification），例如驗證編譯器語義保留性。

步驟如下：

1. 使用 Coq 定義語言的語法與語意（例如簡單四則運算語言）。
2. 定義編譯器函數：將高階語法轉譯為堆疊機器指令。
3. 定義 correctness theorem：編譯後執行結果應與原始語意一致。
4. 透過 COPRA 或類似系統請 LLM 預測並逐步建構證明。

由於完整 correctness theorem 證明過於複雜，COPRA 採用「中繼引理發明 + 逐步求解 + 回填」策略，有效建立證明鏈。

### 第六章：符號回歸與概念抽象 —— LLM於科學發現中的應用

在自然科學中，符號回歸（symbolic regression）是一種試圖從數據中推導出潛在方程的技術。傳統上採用演化演算法（如 PySR）執行，但本文提出將 LLM 引入此任務中，並透過「概念抽象 + LLM引導演化」模式提升表現。

主要架構如下：

* 將程式表示（program hypotheses）與自然語言概念（concepts）建立聯結。
* 定義三個關鍵條件機率：

* P(D|π)：程式 π 解釋資料集 D 的擬合度。
* P(π|C)：程式 π 符合某概念 C 的程度（由 LLM 給予）。
* P(C)：先驗知識中概念 C 的重要性。
* 構成共同目標：推論同時最佳化的 program 與 concept。

該系統稱為 LaSR，能從數據中探索未知公式（例如 Feynman equations、Coulomb's law），並將中繼公式對應至自然語言敘述如「與距離平方成反比」、「呈現指數成長」等。此過程同時結合 genetic mutation 與 LLM-based crossover，實現「可解釋的方程演化流程」。

### 第七章：跨領域整合與未來應用展望

LLM 驅動的代理架構不僅在數學領域展現實用性，其推理能力與結構化互動機制也顯示出極高的跨領域應用潛力。演講中提及的具體範例如下：

1. 天文物理學的歷史演進範例

行星運動觀測與模型建構：從地心說出發，因逆行觀測建構日心說；透過 Tycho Brahe 的火星資料與 Kepler 幾何擬合建立定律，進而推導 Newton 的萬有引力。

2. 形式化系統驗證應用

seL4 作業系統經紅隊滲透測試無效，展示形式驗證在軍用系統中的應用價值。

編譯器正確性證明流程作為可教化且可擴展之自動驗證範式。

3. 自然法則建構與回歸應用

Coulomb’s Law：由純數值資料擬合出標準物理定律。

Feynman equations 與人工合成數據實驗，驗證 LaSR 對未知規律之探索能力。

4. AI 模型效能與超參數對應分析

LaSR 將 shot 數參數導入 LLM scaling law 模型，發現效能轉折規律，進而改寫 chinchilla law 提升預測表現。

5. 概念抽象與語言建模結合

由 LLM 自動從數學表達中萃取如「指數遞減」、「與溫度相關」等概念，有助人類理解模型結果與建構新假設。

使用者提示（hints）能加速方程發現，展現 human-in-the-loop 模式潛力。

6. 高維輸入與多模態模型整合

LLM 可與視覺語言模型結合，處理圖像輸入，推進代理人於高維感知任務中之應用。

### 第八章：總結與研究前景

第八章：總結與研究前景

本篇文章綜觀以 LLM 為核心的數學與科學探索代理系統，展示其在形式化證明、科學定律擬合、概念抽象與跨模態整合上的潛力。研究發現如下：

LLM 結合 proof assistant 可有效提升數學證明效率與正確性。

階層式推理策略與子目標分解是推進複雜命題證明的關鍵。

LaSR 結構將語言模型導入符號回歸與科學概念建模，拓展 LLM 的應用邊界。

概念抽象提供人類理解與模型可解釋性之橋梁，有助於理論構建與知識傳遞。

包含提示訊息與高層語意控制的 human-in-the-loop 模式能進一步提升探索效率。

未來研究可朝以下方向發展：

發展更嚴謹的概念語言或知識表示結構，超越自然語言描述限制。

建立可驗證的中繼知識推論鏈，保障發現之嚴謹性。

擴展代理人架構至包含實驗設計、資料收集與推論整合。

研究在高維輸入（如圖像、感測器資料）下之多模態符號推理流程。

總體而言，LLM 代理架構正逐步成為人工智慧介入科學研究的關鍵典範，未來將在數學、物理、生物醫學等領域帶來深遠影響。

### 參考資料

1. COPRA: Conversational Proof Reasoning Agent – 技術架構與實作案例。
2. Lean 4 與 Coq 語法結構與形式邏輯應用文獻。
3. PySR: Py symbolic regression – 傳統演化回歸框架。
4. LaSR: Language-Guided Symbolic Regression via LLMs and Concept Abstraction, NeurIPS 2023 Poster。
5. FunSearch: LLM-guided program search from DeepMind, 2023。
6. Chinchilla Scaling Law (DeepMind, 2022) – LLM 損失與計算量的對應曲線。
7. Newtonian Mechanics and Kepler's Laws – 天文物理學基礎案例分析。
8. seL4 Formally Verified Microkernel – 軍用級系統驗證代表案例。
9. Feynman Equations Dataset – 物理方程式回歸的評估基準。
10. LeanDojo – 大型語言模型與形式化推理整合研究。
11. LLaMA、GPT 系列與 Frontier Models 輸出特性。
12. Kaiyu Yang 演講逐字稿與技術講解（Formal Reasoning Meets LLMs）。