PhysProver: Advancing Automatic Theorem Proving for Physics
作者: Hanning Zhang, Ruida Wang, Rui Pan, Wenyuan Wang, Bingxu Meng, Tong Zhang
分类: cs.AI, cs.CL
发布日期: 2026-01-22
备注: Preprint
💡 一句话要点
PhysProver：首个物理领域自动定理证明框架，提升物理及数学推理能力。
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动定理证明 物理推理 强化学习 形式化验证 数据集构建
📋 核心要点
- 现有工作较少关注形式化物理推理，而物理推理同样依赖于问题解决和定理证明框架。
- PhysProver利用可验证奖励的强化学习，训练模型在物理定理证明任务上表现更优。
- 实验表明，PhysProver在物理子领域和数学基准测试中均有提升，展现了泛化能力。
📝 摘要（中文）
本文提出了首个增强物理领域形式化定理证明的方法PhysProver。为了实现这一目标，作者构建了一个专门的数据集PhysLeanData，该数据集由PhysLean中的定理以及基于猜想的形式化数据生成流程产生的数据组成。在训练流程中，作者利用DeepSeek-Prover-V2-7B这一强大的开源数学定理证明器，并应用基于可验证奖励的强化学习（RLVR）来训练模型PhysProver。综合实验表明，仅使用约5K的训练样本，PhysProver在多个子领域实现了2.4%的总体改进。此外，经过形式化物理训练后，在MiniF2F-Test基准测试中观察到1.3%的提升，这表明该方法具有超越物理领域的泛化能力，并增强了形式化数学能力。研究结果突出了该方法的有效性和效率，为将形式化证明器扩展到数学领域之外提供了一个范例。为了促进进一步的研究，作者将向社区发布数据集和模型。
🔬 方法详解
问题定义：现有的大语言模型和可验证语言在数学和计算机科学领域取得了显著进展，但在形式化物理推理方面关注较少。物理学同样依赖于严谨的定理证明框架，因此需要专门的方法来解决物理领域的自动定理证明问题。现有方法缺乏针对物理领域的训练数据和优化策略，难以有效进行物理定理的证明。
核心思路：本文的核心思路是利用强化学习，结合可验证的奖励信号，训练一个专门针对物理定理证明的模型。通过构建物理领域的数据集，并利用已有的数学定理证明器作为基础，可以有效地提升模型在物理领域的推理能力。这种方法借鉴了数学领域的成功经验，并将其扩展到物理领域。
技术框架：PhysProver的整体框架包括数据生成、模型训练和评估三个主要阶段。首先，构建PhysLeanData数据集，包含从PhysLean中采样的定理和通过猜想生成的数据。然后，利用DeepSeek-Prover-V2-7B作为基础模型，并使用基于可验证奖励的强化学习（RLVR）进行训练。最后，在多个物理子领域和MiniF2F-Test基准上评估模型的性能。
关键创新：该论文的关键创新在于首次将形式化定理证明方法应用于物理领域，并提出了一个专门针对物理定理证明的数据集和训练流程。通过强化学习和可验证奖励，有效地提升了模型在物理领域的推理能力。此外，该方法还展现了在数学领域的泛化能力，表明其具有一定的通用性。
关键设计：在数据生成方面，采用了基于猜想的形式化数据生成流程，以扩充数据集的多样性。在训练方面，使用了DeepSeek-Prover-V2-7B作为基础模型，并利用RLVR进行微调。奖励函数的设计至关重要，需要能够准确地评估证明的正确性。具体的参数设置和网络结构细节在论文中未详细说明，属于未知信息。
🖼️ 关键图片
📊 实验亮点
PhysProver在多个物理子领域实现了2.4%的总体改进，证明了其在物理定理证明方面的有效性。更重要的是，经过物理训练后，在MiniF2F-Test基准测试中观察到1.3%的提升，表明该方法不仅提升了物理推理能力，还增强了形式化数学能力。这些结果表明，PhysProver具有良好的泛化能力，可以应用于更广泛的领域。
🎯 应用场景
PhysProver的应用场景包括物理学研究、教育和工程领域。它可以辅助物理学家进行理论推导和验证，帮助学生理解物理概念，并应用于工程设计中的物理建模和仿真。该研究的潜在价值在于提高物理研究的效率和准确性，并促进物理学与其他学科的交叉融合。未来，可以将PhysProver扩展到其他科学领域，例如化学和生物学。
📄 摘要（原文）
The combination of verifiable languages and LLMs has significantly influenced both the mathematical and computer science communities because it provides a rigorous foundation for theorem proving. Recent advancements in the field provide foundation models and sophisticated agentic systems pushing the boundaries of formal mathematical reasoning to approach the natural language capability of LLMs. However, little attention has been given to the formal physics reasoning, which also heavily relies on similar problem-solving and theorem-proving frameworks. To solve this problem, this paper presents, to the best of our knowledge, the first approach to enhance formal theorem proving in the physics domain. We compose a dedicated dataset PhysLeanData for the task. It is composed of theorems sampled from PhysLean and data generated by a conjecture-based formal data generation pipeline. In the training pipeline, we leverage DeepSeek-Prover-V2-7B, a strong open-source mathematical theorem prover, and apply Reinforcement Learning with Verifiable Rewards (RLVR) to train our model PhysProver. Comprehensive experiments demonstrate that, using only $\sim$5K training samples, PhysProver achieves an overall 2.4\% improvement in multiple sub-domains. Furthermore, after formal physics training, we observe 1.3\% gains on the MiniF2F-Test benchmark, which indicates non-trivial generalization beyond physics domains and enhancement for formal math capability as well. The results highlight the effectiveness and efficiency of our approach, which provides a paradigm for extending formal provers outside mathematical domains. To foster further research, we will release both our dataset and model to the community.