PhysProver: Advancing Automatic Theorem Proving for Physics

TL;DR

This work presents PhysProver, the first systematic effort to push formal theorem proving into physics. By building PhysLeanData, generating conjectures via Claude-based synthesis, and applying Reinforcement Learning with Verifiable Rewards using GRPO, the authors achieve consistent improvements across physics subdomains with a modest training set (~5K samples) and observe positive transfer to mathematical proof tasks (MiniF2F). The results demonstrate that physics-focused formal data and self-evolving training can extend provers beyond math domains, offering a practical path toward domain-specific formal reasoning. The study further shows that RL-based approaches outperform supervised fine-tuning in this setting and plans to release the dataset and models to catalyze future research in physics-oriented formal reasoning.

Abstract

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.

Figures (8)

• Figure 1: Physics Prover Framework: (a) Data Generation Stage: the training set comprises 5,541 physics statements from both PhysLean tooby2025heplean and synthetic lemmas from Claude-4.5-Sonnet, where the latter are further filtered by Lean syntax and proof existence checks. (b) Self-Evolving Stage: after obtaining the training set, GRPO shao2024deepseekmathgrpo is adopted to train the base prover models, with reward signals of proof correctness provided by Lean.
• Figure 2: Successful examples from the PhysProver and failed proofs from the base model for the same statements. PhysProver demonstrates better in-context learning ability to make good usage of lemmas.
• Figure 3: An example of the PhysLeanData. The black lines denote the header, the blue lines denote the lemma statement, and the red lines denote the proof.
• Figure 4: Prompt template for DeepSeek Prover with a concrete example
• Figure 5: Prompt template for Kimina Prover and Goedel Prover with a concrete example. They are the same as the Deepseek Prover except for the special tokens, such as the BOS token.