PhysProver：推動(dòng)物理自動(dòng)定理證明

PhysProver: Advancing Automatic Theorem Proving for Physics

https://arxiv.org/pdf/2601.15737

摘要
可驗(yàn)證語言與大語言模型（LLMs）的結(jié)合，因其為定理證明提供了嚴(yán)謹(jǐn)基礎(chǔ)，已對(duì)數(shù)學(xué)和計(jì)算機(jī)科學(xué)界產(chǎn)生顯著影響。該領(lǐng)域的最新進(jìn)展包括基礎(chǔ)模型和復(fù)雜的智能體系統(tǒng)，它們不斷推動(dòng)形式化數(shù)學(xué)推理能力的發(fā)展，使其逐步接近大語言模型在自然語言處理方面的表現(xiàn)（Chen 等，2025b）。然而，形式化物理推理卻鮮受關(guān)注，盡管它同樣高度依賴于類似的解題與定理證明框架。為解決這一問題，本文提出——據(jù)我們所知——首個(gè)旨在提升物理學(xué)領(lǐng)域形式化定理證明能力的方法。我們?yōu)榇巳蝿?wù)構(gòu)建了一個(gè)專用數(shù)據(jù)集 PhysLeanData，該數(shù)據(jù)集由從 PhysLean（Tooby-Smith，2025）中采樣的定理以及通過基于猜想的形式化數(shù)據(jù)生成管道所產(chǎn)生的數(shù)據(jù)組成。在訓(xùn)練流程中，我們利用了 DeepSeek-Prover-V2-7B——一個(gè)強(qiáng)大的開源數(shù)學(xué)定理證明器，并采用“帶可驗(yàn)證獎(jiǎng)勵(lì)的強(qiáng)化學(xué)習(xí)”（Reinforcement Learning with Verifiable Rewards, RLVR）來訓(xùn)練我們的模型 PhysProver。全面實(shí)驗(yàn)表明，僅使用約 5,000 個(gè)訓(xùn)練樣本，PhysProver 在多個(gè)子領(lǐng)域上整體提升了 2.4%。此外，在完成形式化物理訓(xùn)練后，我們?cè)?MiniF2F-Test 基準(zhǔn)上觀察到 1.3% 的性能提升，這表明模型不僅在物理領(lǐng)域外實(shí)現(xiàn)了非平凡的泛化能力，也增強(qiáng)了其形式化數(shù)學(xué)推理能力。這些結(jié)果凸顯了我們方法的有效性與高效性，為將形式化證明器拓展至數(shù)學(xué)以外的領(lǐng)域提供了一種新范式。為促進(jìn)后續(xù)研究，我們將向社區(qū)公開發(fā)布我們的數(shù)據(jù)集和模型。

1 引言
形式化推理長(zhǎng)期以來被視為人類智能的基石，也是機(jī)器學(xué)習(xí)研究中的關(guān)鍵領(lǐng)域（Newell 和 Simon，1956）。隨著大語言模型（LLMs）的近期進(jìn)展，大量研究探索了其在形式化定理證明中的應(yīng)用，涵蓋從基礎(chǔ)模型訓(xùn)練（Lin 等，2025b；Ren 等，2025；Wang 等，2025c）到專用智能體框架（Wang 等，2025d；Chen 等，2025b；Varambally 等，2025）等多個(gè)方向。其中，基于 Lean4（Moura 和 Ullrich，2021a）的數(shù)學(xué)定理證明已成為最受深入研究的領(lǐng)域之一（Wang 等，2024；Lin 等，2025a；Xin 等，2024）。研究人員通常從通用大語言模型出發(fā)，通過監(jiān)督微調(diào)（SFT）和強(qiáng)化學(xué)習(xí)（RL）來增強(qiáng)其形式化推理能力。該方法已在 MiniF2F（Zheng 等，2022）和 PutnamBench（Tsoukalas 等，2024）等形式化數(shù)學(xué)基準(zhǔn)上取得了優(yōu)異成果。

以往研究表明，開發(fā)面向 Lean4 定理證明的專家模型需要大量訓(xùn)練數(shù)據(jù)和巨額 GPU 計(jì)算資源。例如，DeepSeek-Prover（Xin 等，2024）使用了 1200 億個(gè)數(shù)學(xué)相關(guān) token 進(jìn)行持續(xù)預(yù)訓(xùn)練，并基于 800 萬條帶證明的形式化語句訓(xùn)練出一個(gè)專家證明器。類似地，Goedel-Prover（Lin 等，2025a）在超過 100 萬條形式化語句上進(jìn)行了專家迭代訓(xùn)練。

盡管取得上述進(jìn)展，形式化定理證明仍面臨重大挑戰(zhàn)，主要源于高質(zhì)量數(shù)據(jù)的稀缺——這些數(shù)據(jù)應(yīng)能賦予模型通用的形式化推理能力，而非局限于狹窄領(lǐng)域（Li 等，2025）。

盡管在數(shù)學(xué)定理證明方面已取得顯著進(jìn)展，形式化物理領(lǐng)域卻在很大程度上被忽視。物理學(xué)依賴于嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)基礎(chǔ)和形式化推導(dǎo)，為形式化推理提供了一個(gè)自然而尚未充分探索的延伸方向。Li 等人（2025）指出，當(dāng)前最先進(jìn)的（SOTA）定理證明模型在物理相關(guān)任務(wù)中表現(xiàn)不佳，但未能提出改進(jìn)方法。

為填補(bǔ)這一空白，據(jù)我們所知，我們邁出了增強(qiáng)物理學(xué)領(lǐng)域定理證明能力的第一步：通過構(gòu)建一個(gè)專用的數(shù)據(jù)管道，并采用“帶可驗(yàn)證獎(jiǎng)勵(lì)的強(qiáng)化學(xué)習(xí)”（Reinforcement Learning with Verifiable Rewards, RLVR）。

我們框架的概覽見圖1。具體而言，我們從開源倉(cāng)庫(kù) PhysLean（Tooby-Smith, 2025）中收集基礎(chǔ)定理與引理，該倉(cāng)庫(kù)包含基于 Lean4 的先進(jìn)物理領(lǐng)域成果，如量子場(chǎng)論和弦理論。提取出的數(shù)據(jù)及其頭部信息被劃分為訓(xùn)練集和測(cè)試集。為擴(kuò)充訓(xùn)練數(shù)據(jù)集，我們利用 Claude-4.5 基于現(xiàn)有數(shù)據(jù)生成額外的猜想。隨后，我們使用形式化大語言模型（formal LLMs）對(duì)這些猜想進(jìn)行標(biāo)注，從而構(gòu)建出“基礎(chǔ)物理 Lean 訓(xùn)練數(shù)據(jù)集”（Basic Physics Lean training dataset），其中包含約 5,000 個(gè)訓(xùn)練樣本和 250 個(gè)測(cè)試樣本。

基于該數(shù)據(jù)集，我們采用 RLVR（Lambert 等，2025）并結(jié)合 GRPO 算法來增強(qiáng)模型的物理定理證明能力。我們的評(píng)估表明，模型在多個(gè)物理子領(lǐng)域均取得持續(xù)提升，在測(cè)試集上相較當(dāng)前最先進(jìn)的數(shù)學(xué)證明器整體提升了 2.4%。此外，在分布外（Out-of-Distribution, OOD）的 MiniF2F 基準(zhǔn)（Zheng 等，2022）上測(cè)試時(shí)，PhysProver 在 pass@16 指標(biāo)下相較基線模型提升了超過 1%。這不僅驗(yàn)證了我們方法的有效性，也表明物理數(shù)據(jù)集的訓(xùn)練能夠增強(qiáng)模型的形式化數(shù)學(xué)能力。

我們的貢獻(xiàn)總結(jié)如下：

1. 首次提出專門用于訓(xùn)練物理學(xué)形式化定理證明器的方法。
2. 構(gòu)建并開源一個(gè)緊湊而全面的小規(guī)模數(shù)據(jù)集，以及一個(gè)面向物理定理的猜想合成管道，以惠及研究社區(qū)。
3. 訓(xùn)練出一個(gè)形式化物理證明器，其性能超越當(dāng)前最先進(jìn)的模型，在物理和數(shù)學(xué)定理證明任務(wù)中均表現(xiàn)出更優(yōu)性能。

2 相關(guān)工作
2.1 形式化數(shù)學(xué)推理
形式化數(shù)學(xué)推理涉及將數(shù)學(xué)成分以計(jì)算機(jī)可驗(yàn)證的格式進(jìn)行表示，從而減少歧義，并為邏輯推理建立嚴(yán)謹(jǐn)基礎(chǔ)。在過去幾十年中，研究人員基于兩種主要理論框架開發(fā)了眾多形式化語言（Formal Languages, FLs）。第一類依賴于依賴類型語言（dependent type languages），例如 Lean（De Moura 等，2015；Moura 和 Ullrich，2021b）和 Coq（Coq，1996），其形式化驗(yàn)證通過一個(gè)小型內(nèi)核執(zhí)行類型檢查來實(shí)現(xiàn)。第二類則利用高階邏輯（higher-order logic）對(duì)函數(shù)和謂詞進(jìn)行量化，代表性語言包括 Isabelle（Paulson，1994）、HOL 以及 HOL Light（Harrison，2009）。在上述語言中，Lean4（Moura 和 Ullrich，2021b）因其表達(dá)能力強(qiáng)以及擁有涵蓋幾乎所有主要數(shù)學(xué)領(lǐng)域的龐大 Mathlib4 倉(cāng)庫(kù)而受到廣泛關(guān)注。

大語言模型（LLMs）的興起加速了形式化證明任務(wù)的發(fā)展。研究人員已匯編了大量數(shù)學(xué)定理與證明數(shù)據(jù)集（Wang 等，2025c；Lin 等，2025a；Dong 和 Ma，2025），為模型訓(xùn)練提供了堅(jiān)實(shí)基礎(chǔ)。在此基礎(chǔ)上，日益復(fù)雜的模型不斷涌現(xiàn)。早期工作如 Expert Iteration（Polu 等，2022）利用 LLM 進(jìn)行迭代式標(biāo)注以增強(qiáng)訓(xùn)練數(shù)據(jù)。開源框架如 DeepSeek-Prover（Xin 等，2024）和 TheoremLlama（Wang 等，2024）進(jìn)一步推動(dòng)了形式化證明器的發(fā)展。近期，RLVR（帶可驗(yàn)證獎(jiǎng)勵(lì)的強(qiáng)化學(xué)習(xí)）被用于形式化定理證明中的長(zhǎng)鏈思維（Long CoT）訓(xùn)練，相關(guān)工作包括 MA-LoT（Wang 等，2025c）、Kimina-Prover（Wang 等，2025a）、DeepSeek-Prover-V2（Ren 等，2025）和 Goedel-Prover-V2（Lin 等，2025b），均取得了顯著進(jìn)展。

智能體框架（agentic frameworks）的出現(xiàn)，如 Hilbert（Varambally 等，2025）和 Seed-Prover-V1（Chen 等，2025c），通過支持多智能體定理分解與子目標(biāo)證明，也取得了突出成果。最新研究進(jìn)一步將智能體強(qiáng)化學(xué)習(xí)應(yīng)用于推動(dòng) LLM 的形式化推理能力，使其更接近自然語言水平（Chen 等，2025b）。盡管如此，物理學(xué)中的形式化推理仍是一個(gè)未被充分探索的領(lǐng)域，代表著未來研究的重要機(jī)遇。

2.2 大語言模型在物理推理中的應(yīng)用
隨著 LLM 通用推理能力的快速發(fā)展，研究人員正積極將其應(yīng)用于更多樣化的領(lǐng)域（Wang 等，2025b）。其中，物理推理是受到廣泛關(guān)注的關(guān)鍵方向之一。在基準(zhǔn)測(cè)試方面，早期的綜合性基準(zhǔn)如 SciBench（Wang 等，2023）和 GPQA（Rein 等，2024）評(píng)估了模型在包括物理學(xué)在內(nèi)的多個(gè)科學(xué)領(lǐng)域中解決大學(xué)水平科學(xué)問題的能力。近期，不同難度級(jí)別的物理專用基準(zhǔn)相繼出現(xiàn)：UGPhysics（Xu 等，2025）提供了 5,520 道本科級(jí)別的雙語物理問題，當(dāng)前先進(jìn)推理模型仍難以解決；OlympiadBench（He 等，2024）引入了 8,476 道奧賽級(jí)別問題，包含多模塊輸入；而最新的 HiPhO（Yu 等，2025）則匯編了 2024–2025 年最新的 13 套國(guó)際物理奧林匹克競(jìng)賽試題，并采用與人類評(píng)分對(duì)齊的評(píng)估方式。

在模型訓(xùn)練方面，研究人員很早就開始探索 LLM 作為物理推理工具的潛力。早期研究表明，LLM 能夠解決需要計(jì)算與推理的復(fù)雜文字題（Ding 等，2023）。這種能力可通過人類反饋強(qiáng)化學(xué)習(xí)（RLHF）（Anand 等，2024）或簡(jiǎn)單的多智能體協(xié)作（Pang 等，2025）進(jìn)一步增強(qiáng)。近期工作將 RLVR 應(yīng)用于自然語言形式的物理問題，其中 P1（Chen 等，2025a）達(dá)到了國(guó)際物理奧林匹克競(jìng)賽（IPhO）金牌水平的表現(xiàn)。然而，由于缺乏專門的數(shù)據(jù)集和訓(xùn)練方法，面向形式化物理推理的 LLM 開發(fā)目前仍相對(duì)不足（Li 等，2025）。

3 方法
3.1 種子數(shù)據(jù)集構(gòu)建

我們從 PhysLean GitHub 倉(cāng)庫(kù)（Tooby-Smith, 2025）中構(gòu)建了一個(gè)引理–證明數(shù)據(jù)集，方法是從所有 .lean 文件中提取所有可證明的引理及其前置的形式化頭部（formal headers）。帶有上下文的引理陳述作為輸入，對(duì)應(yīng)的證明腳本作為輸出。我們對(duì)樣本進(jìn)行過濾，僅保留總長(zhǎng)度不超過 4,096 個(gè) token 的樣本。最終得到的語料庫(kù)包含超過 3,000 個(gè)示例，按大約 9:1 的比例隨機(jī)劃分為訓(xùn)練集和測(cè)試集，分別得到 2,933 個(gè)訓(xùn)練樣本和 250 個(gè)測(cè)試樣本。該數(shù)據(jù)集覆蓋了廣泛的物理與數(shù)學(xué)領(lǐng)域，包括經(jīng)典與現(xiàn)代物理學(xué)（如經(jīng)典力學(xué)、電磁學(xué)、量子力學(xué)和相對(duì)論），以及量子場(chǎng)論、弦論和數(shù)學(xué)基礎(chǔ)等高級(jí)理論領(lǐng)域。所收集數(shù)據(jù)的一個(gè)示例如圖 3 所示。

3.2 合成數(shù)據(jù)生成

其中 Verify 表示 Lean 驗(yàn)證結(jié)果。
該過程產(chǎn)生了 2,608 個(gè)已驗(yàn)證的猜想，整體流程產(chǎn)出率為 8.9%，
與 STP（Dong 和 Ma，2025）相當(dāng)。
將這些猜想與第 3.1 節(jié)中的 2,933 個(gè)種子訓(xùn)練樣本相結(jié)合，
共得到 5,541 個(gè)訓(xùn)練實(shí)例用于我們的實(shí)驗(yàn)。
值得注意的是，我們還比較了不同的專有模型，包括 GPT-5（OpenAI，2025）
和 Gemini-2.5-Pro（Google，2025）。然而，它們生成的猜想在語法正確率方面
顯著低于 Claude 生成的結(jié)果。我們還探索了另一種方法：
先以自然語言生成猜想，再通過自動(dòng)形式化工具將其轉(zhuǎn)換為 Lean4 語句。
然而，由于物理陳述中存在復(fù)雜的依賴關(guān)系，導(dǎo)致難以識(shí)別統(tǒng)一的頭部結(jié)構(gòu)，
自動(dòng)形式化工具在此任務(wù)上失敗，因此該方法的最終成功率也較低。

3.3 自進(jìn)化流程
我們?cè)谖锢眍I(lǐng)域采用強(qiáng)化學(xué)習(xí)（Reinforcement Learning, RL）來提升性能。
具體而言，我們的實(shí)驗(yàn)主要基于 Group Relative Policy Optimization（GRPO）（Shao 等，2024）。
對(duì)于訓(xùn)練集中的每個(gè)提示 x，在 rollout 階段會(huì)采樣 G（組大小）個(gè)響應(yīng)，
并優(yōu)化以下目標(biāo)函數(shù)：

獎(jiǎng)勵(lì)信號(hào) r ( x , y i )
由 Lean 驗(yàn)證器提供，用于指導(dǎo)強(qiáng)化學(xué)習(xí)過程。具體而言，驗(yàn)證器給出 1 或 0 的分?jǐn)?shù)，以表明證明是否正確。由于 Lean 具有符號(hào)性質(zhì)，所有獲得獎(jiǎng)勵(lì) 1 的已驗(yàn)證證明都是完全正確的，不存在任何幻覺（hallucination），這使得模型能夠以具體且嚴(yán)謹(jǐn)?shù)姆绞綄W(xué)習(xí)物理學(xué)的基礎(chǔ)。為進(jìn)一步降低學(xué)習(xí)過程的難度，采用了課程學(xué)習(xí)（curriculum learning）策略，即根據(jù)輸入語句（猜想）對(duì)應(yīng)的真實(shí)證明長(zhǎng)度對(duì)其進(jìn)行排序。這種由易到難的學(xué)習(xí)方式鼓勵(lì)證明器模型以自底向上的方式進(jìn)行學(xué)習(xí)。

4 實(shí)驗(yàn)
為評(píng)估我們的方法，我們使用 PhysLeanData 數(shù)據(jù)集來訓(xùn)練主流的基于 Lean 的形式化數(shù)學(xué)證明器。實(shí)驗(yàn)結(jié)果表明，即使強(qiáng)大的數(shù)學(xué)推理模型在處理形式化物理問題時(shí)也表現(xiàn)出顯著的局限性，這凸顯了領(lǐng)域特定形式化數(shù)據(jù)集和自進(jìn)化策略的重要性。

4.1 實(shí)驗(yàn)設(shè)置
4.1.1 數(shù)據(jù)集與任務(wù)
模型性能在 PhysLeanData 的測(cè)試集上進(jìn)行評(píng)估，該測(cè)試集與訓(xùn)練集來自相同的數(shù)據(jù)源，并采用 9:1 的訓(xùn)練-測(cè)試劃分比例。為確保不同上下文長(zhǎng)度模型之間的公平比較，我們僅保留提示長(zhǎng)度不超過 4,096 個(gè) token 的樣本，最終評(píng)估集包含 250 個(gè)引理（lemmas）。

為進(jìn)行更細(xì)粒度的分析，我們將測(cè)試樣本劃分為四個(gè)物理類別：經(jīng)典與基礎(chǔ)物理（Classical & Foundational Physics）、粒子與弦物理（Particle & String Physics）、相對(duì)論與時(shí)空（Relativity & Spacetime）以及量子場(chǎng)論（Quantum Field Theory）。這一分類反映了不同的理論框架以及對(duì)領(lǐng)域?qū)I(yè)知識(shí)的不同要求。更多細(xì)節(jié)見附錄 B。

4.1.2 模型與基線
我們比較了若干流行的開源證明器模型，包括 DeepSeek-Prover-V2-7B（Ren 等，2025）、Kimina-Prover-Distill-8B（Wang 等，2025a）和 Goedel-Prover-V2-8B（Lin 等，2025b），這些模型均為針對(duì)數(shù)學(xué)領(lǐng)域優(yōu)化的強(qiáng)形式化定理證明器。由于 DeepSeek-Prover-V2-7B 在其中表現(xiàn)最佳，我們的實(shí)驗(yàn)將聚焦于對(duì)該 DeepSeek 證明器進(jìn)行訓(xùn)練，以推動(dòng)開源模型的能力邊界。

在基線方面，我們首先報(bào)告未經(jīng)任何額外訓(xùn)練的 DeepSeek-Prover-V2-7B、Kimina-Prover-Distill-8B 和 Goedel-Prover-V2-8B 的性能。我們還將其與強(qiáng)大的專有系統(tǒng)進(jìn)行比較，即 GPT-5（OpenAI，2025）和 Claude-4.5-Sonnet（Anthropic，2025）。對(duì)于所有基線模型，我們采用固定的采樣預(yù)算，并報(bào)告 pass@16 準(zhǔn)確率，以確保在一致的推理預(yù)算下進(jìn)行公平比較。
對(duì)于開源證明器，我們使用附錄 D.1 中提供的提示模板；對(duì)于專有模型，則采用定制的思維鏈（Chain-of-Thought, CoT）（Wei 等，2023）提示，以鼓勵(lì)其在生成最終證明前進(jìn)行逐步推理。

4.2 實(shí)現(xiàn)細(xì)節(jié)
我們直接從 DeepSeek-Prover-V2-7B 出發(fā)，使用 verl 框架（Sheng 等，2025）進(jìn)行強(qiáng)化學(xué)習(xí)。具體而言，我們應(yīng)用 GRPO 算法，并結(jié)合基于規(guī)則的獎(jiǎng)勵(lì)機(jī)制（Lambert 等，2025；DeepSeek-AI 等，2025）來指導(dǎo)自進(jìn)化訓(xùn)練過程。特別地，我們將 Lean 驗(yàn)證器（版本 4.20.0）集成到 verl 框架中，用于驗(yàn)證所生成的證明。每條軌跡（trajectory）的獎(jiǎng)勵(lì)分?jǐn)?shù)按如下方式計(jì)算：

此外，如果證明中包含 “sorry”、“admit” 或 “apply?” 等關(guān)鍵詞，我們直接將其獎(jiǎng)勵(lì)分?jǐn)?shù)設(shè)為 0，以避免獎(jiǎng)勵(lì)作弊。此外，為了在學(xué)習(xí)過程中實(shí)現(xiàn)難度的平滑過渡，我們采用課程學(xué)習(xí)（Parashar 等，2025），即根據(jù)引理對(duì)應(yīng)的真實(shí)證明長(zhǎng)度對(duì)其進(jìn)行排序。

我們?cè)?8 塊 H200 GPU 上訓(xùn)練所有模型，學(xué)習(xí)率恒定為 1e??，批次大小為 256，共訓(xùn)練 2 個(gè)輪次（epochs），整個(gè)訓(xùn)練過程耗時(shí)約 8 小時(shí)。值得注意的是，我們未使用監(jiān)督微調(diào)（SFT）的預(yù)熱階段，因?yàn)檫@會(huì)降低性能。該行為已在第 6 節(jié)中進(jìn)行了研究和進(jìn)一步分析。我們還在第 6 節(jié)中探討了拒絕采樣微調(diào)方法（Yuan 等，2023；Dong 等，2023）。

4.3 實(shí)驗(yàn)結(jié)果

我們的實(shí)驗(yàn)結(jié)果如表 1 所示。首先我們觀察到，盡管現(xiàn)有模型在數(shù)學(xué)定理證明方面表現(xiàn)出色，但在物理任務(wù)上的得分普遍較低，沒有任何模型的準(zhǔn)確率超過 40%。值得注意的是，即使是小型開源定理證明器模型，其準(zhǔn)確率也與最新的專有系統(tǒng)（如 Claude-4.5-Sonnet 和 GPT-5）具有可比性。然而，專有模型與開源模型在不同物理領(lǐng)域展現(xiàn)出不同的優(yōu)勢(shì)。例如，所有開源證明器在量子場(chǎng)論（Quantum Field Theory）上的準(zhǔn)確率均低于 30%，而專有模型則超過了 35%。這表明專有模型和開源模型可能是在不同組合的物理數(shù)據(jù)上進(jìn)行訓(xùn)練的。我們還調(diào)查了量子場(chǎng)論類別中的上下文長(zhǎng)度，發(fā)現(xiàn)其平均長(zhǎng)度比其他領(lǐng)域長(zhǎng)約三分之一。這些發(fā)現(xiàn)與 Li 等人（2025）的研究一致，表明像 Claude 這樣的大模型具備更強(qiáng)的上下文學(xué)習(xí)能力，從而在性能上優(yōu)于開源模型。

我們訓(xùn)練的模型 PhysProver 顯著超越了現(xiàn)有的形式化數(shù)學(xué)證明器，在所有類別中均持續(xù)取得提升。具體而言，在最具挑戰(zhàn)性的領(lǐng)域——粒子與弦物理（Particle & String Physics）——所有基線模型的準(zhǔn)確率都很低，而我們的模型仍實(shí)現(xiàn)了 3.0% 的顯著提升。這些結(jié)果表明，僅使用少量高質(zhì)量數(shù)據(jù)集，就能有效將數(shù)學(xué)證明器擴(kuò)展至物理領(lǐng)域。此外，性能的持續(xù)提升表明當(dāng)前的證明器遠(yuǎn)未達(dá)到性能飽和，說明構(gòu)建高質(zhì)量的物理專用數(shù)據(jù)集仍是一個(gè)極具前景的研究方向。

此外，小型的 7B 規(guī)模 PhysProver 模型在整體性能上優(yōu)于 GPT-5 和 Claude-4.5-Sonnet，這表明小型專家模型在形式化物理定理證明的特定領(lǐng)域中具有巨大潛力。這為高效訓(xùn)練物理證明器模型提供了一條富有前景的路徑。

5 分析
5.1 通過強(qiáng)化學(xué)習(xí)提升上下文學(xué)習(xí)能力
在本小節(jié)中，我們通過對(duì)基線模型與我們的模型所生成證明的對(duì)比分析，詳細(xì)探討 PhysProver 所取得的性能提升。圖2展示了測(cè)試集中一個(gè)具有代表性的示例及其對(duì)應(yīng)的生成結(jié)果。其中，頭部（header）和引理（lemmas）構(gòu)成了物理定理證明的上下文，而這些引理在證明過程中充當(dāng)輔助工具。

我們觀察到，PhysProver 能持續(xù)正確使用函數(shù)和引理，成功調(diào)用的部分以藍(lán)色高亮顯示。例如，為證明給定猜想，它首先應(yīng)用了 timeContract_eq_superCommute，接著調(diào)用函數(shù) timeContract；隨后，模型正確調(diào)用了 superCommute_anPart_ofFieldOpF_diff_grade_zero，體現(xiàn)出其對(duì)上下文信息的有效利用。通過綜合上下文提供的知識(shí)，PhysProver 成功完成了證明。

相比之下，基礎(chǔ)模型雖然最初正確應(yīng)用了 timeContract_eq_superCommute，但隨后生成了幻覺內(nèi)容，包括不存在的引理，如 normalOrder_ofFieldOp_pair_eq_zero 和 timeOrderRel_of_isContraction（以紅色標(biāo)記）。這些觀察表明，基于 PhysLeanData 的強(qiáng)化學(xué)習(xí)過程通過使模型更有效地利用上下文信息并理解領(lǐng)域特定術(shù)語，從而提升了性能。這一發(fā)現(xiàn)也解釋了為何所有基礎(chǔ)模型準(zhǔn)確率普遍偏低：它們對(duì)物理領(lǐng)域特有的引理和上下文結(jié)構(gòu)不熟悉，因而難以有效利用這些資源完成證明。

5.2 分布外泛化能力
令人驚訝的是，我們還發(fā)現(xiàn)，在以物理為中心的問題上進(jìn)行訓(xùn)練，能顯著提升形式化數(shù)學(xué)定理證明的泛化能力。在本小節(jié)中，我們?cè)?MiniF2F-Test 數(shù)據(jù)集（Zheng 等，2022）上評(píng)估了訓(xùn)練后的模型。該數(shù)據(jù)集包含 244 條 Lean4 語句，涵蓋從高中競(jìng)賽題到本科初級(jí)水平的證明問題。我們依照 Ren 等人（2025）的方法將數(shù)據(jù)集劃分為若干類別。對(duì)于 MiniF2F-Test 中的每條語句，我們提示基線模型與訓(xùn)練后的模型各自生成 16 條軌跡，并計(jì)算 pass@16 準(zhǔn)確率。我們使用 DeepSeek 官網(wǎng)提供的相同提示模板。

如表2所示，PhysProver 整體表現(xiàn)與基礎(chǔ)版本相當(dāng)，甚至在某些方面超越了基礎(chǔ)版本。值得注意的是，這種提升并非在所有類別中均一致。例如，我們的模型在 MATH 數(shù)據(jù)集（Hendrycks 等，2021）中的中等難度問題上表現(xiàn)出顯著提升。相反，更具挑戰(zhàn)性的奧林匹克級(jí)別問題可能無法從 GRPO 訓(xùn)練中受益，因?yàn)樵?AIME 類別中性能反而下降。這些結(jié)果揭示了 Lean4 中數(shù)學(xué)與物理定理證明之間既存在內(nèi)在聯(lián)系，又存在明顯差異�？傮w而言，在物理問題上的訓(xùn)練能夠增強(qiáng)數(shù)學(xué)推理能力；然而，困難的數(shù)學(xué)問題可能需要截然不同的解題技巧，這些技巧無法直接從基于物理的訓(xùn)練中獲得。

6 重新審視監(jiān)督微調(diào)的作用
我們進(jìn)一步研究了是否可以通過在 PhysLeanData 上進(jìn)行監(jiān)督微調(diào)（Supervised Fine-tuning, SFT）來提升模型在物理任務(wù)上的性能——這是訓(xùn)練專用大語言模型的標(biāo)準(zhǔn)做法。然而，我們?cè)跍y(cè)試集上并未觀察到 SFT 帶來的任何改進(jìn)，反而一致地出現(xiàn)了性能下降。

具體而言，我們首先在 PhysLeanData 上對(duì) DeepSeek-Prover-V2-7B 進(jìn)行微調(diào)，其中真實(shí)答案（ground-truth answers）要么來自人類編寫的 PhysLean 庫(kù)，要么由開源證明器生成并經(jīng)后續(xù)驗(yàn)證確認(rèn)。訓(xùn)練樣本模板遵循附錄 D.1 中的強(qiáng)化學(xué)習(xí)提示模板，并將損失計(jì)算限制在補(bǔ)全（completion）部分。接著，我們還嘗試了拒絕采樣微調(diào)（Rejection Sampling Fine-tuning），即獎(jiǎng)勵(lì)排序微調(diào)（Reward-Ranked Fine-tuning, RAFT）（Dong 等，2023；Yuan 等，2023）：我們?cè)谟?xùn)練集上對(duì) DeepSeek-Prover-V2-7B 進(jìn)行采樣，僅保留正確的證明作為新的訓(xùn)練集。我們分別在這兩個(gè)訓(xùn)練集上對(duì) DeepSeek-Prover-V2-7B 進(jìn)行單輪微調(diào)，學(xué)習(xí)率為 5e??，批次大小為 32。這兩個(gè)模型分別記為 DS-Prover-SFT 和 DS-Prover-RAFT。

如表 3 所示，對(duì)于 DS-Prover-SFT，我們?cè)谒蓄悇e中均觀察到一致的性能下降，平均準(zhǔn)確率降低了 6.4%。相比之下，DS-Prover-RAFT 整體提升了 1.6%，除經(jīng)典物理（Classical Physics）外，其余三個(gè)類別均有提高。

我們將這種性能差異歸因于訓(xùn)練數(shù)據(jù)的分布特性。原始的 PhysLeanData 由人類編寫，相對(duì)于模型自身的生成能力而言屬于分布外（Out-of-Distribution, OOD）數(shù)據(jù)；而拒絕采樣所得到的數(shù)據(jù)則屬于分布內(nèi)（In-Distribution, ID）數(shù)據(jù)，更貼近模型的輸出分布。因此，ID 數(shù)據(jù)可能更容易被模型學(xué)習(xí)，從而帶來性能提升。

為更深入理解這一現(xiàn)象，我們開展了探針實(shí)驗(yàn)，比較 SFT 模型、RAFT 模型（見表 3）以及我們主實(shí)驗(yàn)中的 GRPO 模型的不確定性。為了評(píng)估模型在訓(xùn)練集和測(cè)試集上的不確定性，我們測(cè)量了在給定輸入提示條件下采樣響應(yīng)的平均困惑度（perplexity）。具體而言，對(duì)于來自訓(xùn)練集或測(cè)試集的任一提示 x x，我們從模型中采樣 K = 16
個(gè)響應(yīng) y k ，并計(jì)算這些樣本的平均困惑度。我們從訓(xùn)練集和測(cè)試集中各隨機(jī)選取 50 個(gè)樣本。該計(jì)算定義如下：

該指標(biāo)反映了模型自身的不確定性：數(shù)值越低，表明模型生成的響應(yīng)是其認(rèn)為更可能、更貼合輸入的內(nèi)容；數(shù)值越高，則表明模型對(duì)提示的響應(yīng)具有更大的變異性或不熟悉度。

如表 4 所示，結(jié)果表明，DS-Prover-GRPO 和 DS-Prover-RAFT 在訓(xùn)練集和測(cè)試集上的平均困惑度均顯著低于 DS-Prover-SFT，這解釋了為何 GRPO 和 RAFT 能提升性能，而 SFT 卻不能。這些結(jié)果表明，盡管監(jiān)督微調(diào)（SFT）直接最大化目標(biāo) token 的概率，但它并不必然降低模型的不確定性，尤其對(duì)于 DeepSeek-Prover 這類已經(jīng)經(jīng)過大量領(lǐng)域特定（數(shù)學(xué)）訓(xùn)練的模型而言更是如此。這一觀察為未來改進(jìn)專家模型提供了重要啟示：監(jiān)督微調(diào)并非總是必要或最優(yōu)的選擇。相反，采用拒絕采樣微調(diào)（Rejection Sampling Fine-tuning）方法收集并微調(diào)分布內(nèi)（In-Distribution, ID）數(shù)據(jù)，可能是一種更實(shí)用的解決方案。此外，在資源有限的場(chǎng)景下，直接應(yīng)用強(qiáng)化學(xué)習(xí)也可作為一種可行的替代方案。我們還在附錄 C 中探索了在拒絕采樣微調(diào)之后再進(jìn)行強(qiáng)化學(xué)習(xí)的方法，但未觀察到進(jìn)一步的性能提升。

7 結(jié)論
本文首次系統(tǒng)性地推進(jìn)了物理領(lǐng)域的形式化定理證明。我們首先提出了 PhysLeanData——一個(gè)在 Lean4 中形式化表述的物理定理數(shù)據(jù)集，并配套設(shè)計(jì)了一套猜想生成流程，用于生成有效且正確的猜想。通過對(duì)當(dāng)前最先進(jìn)的開源定理證明器應(yīng)用基于可驗(yàn)證獎(jiǎng)勵(lì)的強(qiáng)化學(xué)習(xí)（Reinforcement Learning with Verifiable Rewards, RLVR），我們的 PhysProver 模型僅使用約 5,000 個(gè)樣本，就在量子場(chǎng)論等物理子領(lǐng)域上實(shí)現(xiàn)了平均 2.4% 的持續(xù)性能提升。該模型在分布外的 MiniF2F 測(cè)試基準(zhǔn)上也展現(xiàn)出超過 1% 的提升，凸顯了其強(qiáng)大的泛化能力。我們的工作彌合了數(shù)學(xué)形式化定理證明與其在物理科學(xué)中應(yīng)用之間的一個(gè)關(guān)鍵鴻溝。我們將公開發(fā)布所構(gòu)建的數(shù)據(jù)集與模型，以促進(jìn)該方向的后續(xù)研究。

8 局限性
我們的工作存在若干局限性，我們對(duì)此予以承認(rèn)，并希望在未來研究中加以解決。首先，受限于計(jì)算資源，我們未能收集更多數(shù)據(jù)，也無法將猜想生成過程大規(guī)模擴(kuò)展。如第 3.2 節(jié)所述，我們的合成數(shù)據(jù)流程產(chǎn)出率僅為 8.9%，意味著大量生成的猜想在有效性與正確性驗(yàn)證階段被過濾掉。擴(kuò)大生成規(guī)模將需要顯著更多的算力，既包括基于大語言模型的猜想生成，也包括多證明器驗(yàn)證階段，而這超出了我們當(dāng)前的預(yù)算。此外，我們的數(shù)據(jù)集完全源自 PhysLean 代碼庫(kù)；盡管該庫(kù)內(nèi)容較為全面，但可能并未均勻覆蓋物理學(xué)的所有領(lǐng)域。某些專門領(lǐng)域可能存在代表性不足的問題，這可能會(huì)限制模型在更廣泛物理定理證明任務(wù)中的適用性。

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