PhysProver：推動物理自動定理證明

PhysProver：推動物理自動定理證明

PhysProver: Advancing Automatic Theorem Proving for Physics

https://arxiv.org/pdf/2601.15737

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

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

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

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

盡管在數學定理證明方面已取得顯著進展，形式化物理領域卻在很大程度上被忽視。物理學依賴于嚴謹的數學基礎和形式化推導，為形式化推理提供了一個自然而尚未充分探索的延伸方向。Li 等人（2025）指出，當前最先進的（SOTA）定理證明模型在物理相關任務中表現不佳，但未能提出改進方法。

為填補這一空白，據我們所知，我們邁出了增強物理學領域定理證明能力的第一步：通過構建一個專用的數據管道，并采用“帶可驗證獎勵的強化學習”（Reinforcement Learning with Verifiable Rewards, RLVR）。

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

基于該數據集，我們采用 RLVR（Lambert 等，2025）并結合 GRPO 算法來增強模型的物理定理證明能力。我們的評估表明，模型在多個物理子領域均取得持續提升，在測試集上相較當前最先進的數學證明器整體提升了 2.4%。此外，在分布外（Out-of-Distribution, OOD）的 MiniF2F 基準（Zheng 等，2022）上測試時，PhysProver 在 pass@16 指標下相較基線模型提升了超過 1%。這不僅驗證了我們方法的有效性，也表明物理數據集的訓練能夠增強模型的形式化數學能力。

我們的貢獻總結如下：

1. 首次提出專門用于訓練物理學形式化定理證明器的方法。
2. 構建并開源一個緊湊而全面的小規模數據集，以及一個面向物理定理的猜想合成管道，以惠及研究社區。
3. 訓練出一個形式化物理證明器，其性能超越當前最先進的模型，在物理和數學定理證明任務中均表現出更優性能。

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

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

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

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

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

3 方法
3.1 種子數據集構建

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

3.2 合成數據生成

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

3.3 自進化流程
我們在物理領域采用強化學習（Reinforcement Learning, RL）來提升性能。
具體而言，我們的實驗主要基于 Group Relative Policy Optimization（GRPO）（Shao 等，2024）。
對于訓練集中的每個提示 x，在 rollout 階段會采樣 G（組大小）個響應，
并優化以下目標函數：

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

4 實驗
為評估我們的方法，我們使用 PhysLeanData 數據集來訓練主流的基于 Lean 的形式化數學證明器。實驗結果表明，即使強大的數學推理模型在處理形式化物理問題時也表現出顯著的局限性，這凸顯了領域特定形式化數據集和自進化策略的重要性。

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

為進行更細粒度的分析，我們將測試樣本劃分為四個物理類別：經典與基礎物理（Classical & Foundational Physics）、粒子與弦物理（Particle & String Physics）、相對論與時空（Relativity & Spacetime）以及量子場論（Quantum Field Theory）。這一分類反映了不同的理論框架以及對領域專業知識的不同要求。更多細節見附錄 B。

4.1.2 模型與基線
我們比較了若干流行的開源證明器模型，包括 DeepSeek-Prover-V2-7B（Ren 等，2025）、Kimina-Prover-Distill-8B（Wang 等，2025a）和 Goedel-Prover-V2-8B（Lin 等，2025b），這些模型均為針對數學領域優化的強形式化定理證明器。由于 DeepSeek-Prover-V2-7B 在其中表現最佳，我們的實驗將聚焦于對該 DeepSeek 證明器進行訓練，以推動開源模型的能力邊界。

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

4.2 實現細節
我們直接從 DeepSeek-Prover-V2-7B 出發，使用 verl 框架（Sheng 等，2025）進行強化學習。具體而言，我們應用 GRPO 算法，并結合基于規則的獎勵機制（Lambert 等，2025；DeepSeek-AI 等，2025）來指導自進化訓練過程。特別地，我們將 Lean 驗證器（版本 4.20.0）集成到 verl 框架中，用于驗證所生成的證明。每條軌跡（trajectory）的獎勵分數按如下方式計算：

此外，如果證明中包含 “sorry”、“admit” 或 “apply?” 等關鍵詞，我們直接將其獎勵分數設為 0，以避免獎勵作弊。此外，為了在學習過程中實現難度的平滑過渡，我們采用課程學習（Parashar 等，2025），即根據引理對應的真實證明長度對其進行排序。

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

4.3 實驗結果

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

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

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

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

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

相比之下，基礎模型雖然最初正確應用了 timeContract_eq_superCommute，但隨后生成了幻覺內容，包括不存在的引理，如 normalOrder_ofFieldOp_pair_eq_zero 和 timeOrderRel_of_isContraction（以紅色標記）。這些觀察表明，基于 PhysLeanData 的強化學習過程通過使模型更有效地利用上下文信息并理解領域特定術語，從而提升了性能。這一發現也解釋了為何所有基礎模型準確率普遍偏低：它們對物理領域特有的引理和上下文結構不熟悉，因而難以有效利用這些資源完成證明。

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

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

6 重新審視監督微調的作用
我們進一步研究了是否可以通過在 PhysLeanData 上進行監督微調（Supervised Fine-tuning, SFT）來提升模型在物理任務上的性能——這是訓練專用大語言模型的標準做法。然而，我們在測試集上并未觀察到 SFT 帶來的任何改進，反而一致地出現了性能下降。

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

如表 3 所示，對于 DS-Prover-SFT，我們在所有類別中均觀察到一致的性能下降，平均準確率降低了 6.4%。相比之下，DS-Prover-RAFT 整體提升了 1.6%，除經典物理（Classical Physics）外，其余三個類別均有提高。

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

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

該指標反映了模型自身的不確定性：數值越低，表明模型生成的響應是其認為更可能、更貼合輸入的內容；數值越高，則表明模型對提示的響應具有更大的變異性或不熟悉度。

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

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

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

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