Lean4Physics：在Lean4中的大学物理综合推理框架

于红博

摘要: 我们提出了**Lean4PHYS**，这是一个为大学级物理问题提供全面推理框架的Lean4。**Lean4PHYS**包括*LeanPhysBench*，一个用于Lean4中形式化物理推理的大学级基准，其中包含了从大学教科书和物理竞赛问题中提取的200个手工制作和同行评审的陈述。为了建立物理形式推理的坚实基础，我们还引入了*PhysLib*，这是一个由社区驱动的仓库，包含了对于形式物理推理至关重要的基本单位系统和定理。基于我们在**Lean4PHYS**中组成的基准和Lean4仓库，我们使用主要的专家数学Lean4证明器和最先进的闭源模型报告了基线结果，其中DeepSeek-Prover-V2-7B的最佳性能仅达到16%，而Claude-Sonnet-4的性能达到35%。我们还进行了详细分析，显示我们的*PhysLib*可以在模型性能上实现平均提高11.75%。这证明了我们的*LeanPhysBench*的挑战性质以及*PhysLib*的有效性。据我们所知，这是第一项提供Lean4物理基准的研究。

更新时间: 2025-10-30 03:09:40

领域: cs.AI,cs.LG

下载: http://arxiv.org/abs/2510.26094v1