PhysProver：推进面向物理的自动定理证明

可验证语言与 LLM 的结合显著影响了数学与计算机科学界，因为它为定理证明提供了严格基础。该领域近期进展提供了基础模型与复杂的 agentic 系统，把形式数学推理的边界推向 LLM 的自然语言能力。然而，形式物理推理很少受到关注，尽管它同样大量依赖类似的问题求解与定理证明框架。为解决这一问题，本文据我们所知首次提出增强物理领域形式定理证明的方法。我们为该任务构建专门数据集 PhysLeanData。它由从 PhysLean 采样的定理与基于猜想的正式数据生成管线产生的数据组成。在训练管线中，我们利用强大的开源数学定理证明器 DeepSeek-Prover-V2-7B，并应用可验证奖励强化学习（RLVR）训练我们的模型 PhysProver。综合实验表明，仅用约 5K 训练样本，PhysProver 在多个子领域取得整体 2.4% 的改进。此外，经过形式物理训练后，我们观察到在 MiniF2F-Test 基准上 1.3% 的增益，表明超越物理领域的非平凡泛化以及对形式数学能力的增强。结果凸显我们方法的有效性与效率，为把形式证明器扩展到数学领域之外提供范式。为进一步研究，我们将向社区发布数据集与模型。