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%。这不仅验证了我们方法的有效性，也表明物理数据集的训练能够增强模型的形式化数学能力。
我们的贡献总结如下：
- 首次提出专门用于训练物理学形式化定理证明器的方法。
- 构建并开源一个紧凑而全面的小规模数据集，以及一个面向物理定理的猜想合成管道，以惠及研究社区。
- 训练出一个形式化物理证明器，其性能超越当前最先进的模型，在物理和数学定理证明任务中均表现出更优性能。
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
热门跟贴