Technical Summary: PhysProver

Problem Statement

While the integration of Large Language Models (LLMs) with verifiable formal languages has significantly advanced automatic theorem proving in mathematics (e.g., Lean4), the domain of formal physics reasoning remains largely underexplored. Existing state-of-the-art (SOTA) theorem provers, trained primarily on mathematical datasets, demonstrate poor performance on physics-related tasks. This gap exists because physics relies on rigorous mathematical foundations and formal derivations specific to physical theories (e.g., Quantum Field Theory, String Theory) that are not adequately represented in current mathematical theorem proving datasets. Previous works have identified this deficiency but have not proposed effective methods to bridge it.

Methodology

The authors propose PhysProver, the first systematic approach to enhance formal theorem proving specifically for the physics domain. The methodology consists of three core components:

1. Data Construction (PhysLeanData)

To address the scarcity of high-quality formal physics data, the authors constructed PhysLeanData, a specialized dataset comprising approximately 5,541 training samples. The data generation pipeline involves:

• Seed Collection: Extracting provable lemmas and their corresponding proofs from the open-source PhysLean repository, covering domains such as classical mechanics, electromagnetism, quantum mechanics, relativity, and quantum field theory.
• Synthetic Augmentation: Utilizing Claude-4.5-Sonnet to generate new conjectures based on seed lemma-header pairs.
• Verification Pipeline: A two-stage filtering process:
  1. Syntactic Verification: Using the Lean verifier to ensure generated conjectures are well-formed and all referenced definitions exist.
  2. Provability Verification: Employing multiple strong provers (DeepSeek-Prover-V2-7B, Kimina-Prover-Distill-8B, Goedel-Prover-V2-8B) to attempt proofs. Conjectures are retained only if at least one prover successfully verifies the statement.
• Result: The final dataset contains ~5,000 training samples and ~250 test samples, filtered to a maximum length of 4,096 tokens.

2. Training Framework

The authors leverage DeepSeek-Prover-V2-7B, a strong open-source mathematical theorem prover, as the base model. Instead of Supervised Fine-Tuning (SFT), which the authors found to degrade performance on this task, they employ Reinforcement Learning with Verifiable Rewards (RLVR) using the Group Relative Policy Optimization (GRPO) algorithm.

• Reward Signal: The Lean verifier provides a binary reward (1 for a correct proof, 0 otherwise). Proofs containing placeholders like sorry or admit are penalized with a reward of 0 to prevent reward hacking.
• Curriculum Learning: To facilitate learning, the training data is sorted by the length of the ground-truth proofs, enabling an "easy-to-hard" training progression.

3. Evaluation Strategy

The model is evaluated on:

• In-Distribution: The PhysLeanData test set, categorized into Classical, Particle & String, Relativity, and Quantum Field Theory.
• Out-of-Distribution (OOD): The MiniF2F-Test benchmark (mathematics) to assess generalization capabilities beyond the physics domain.

Key Results

• Performance on Physics Benchmarks: PhysProver achieves an overall 2.4% improvement over the base DeepSeek-Prover-V2-7B across all physics sub-domains. Notably, it improves performance on the challenging "Particle & String" category by 3.0%.
• Comparison with Proprietary Models: The 7B-parameter PhysProver outperforms both GPT-5 and Claude-4.5-Sonnet in overall accuracy on the physics test set, demonstrating the efficacy of small, domain-specialized expert models.
• Generalization to Mathematics: Training on physics data yields a 1.3% improvement on the MiniF2F-Test benchmark (pass@16), indicating that formal physics training enhances general formal mathematical reasoning capabilities.
• Ablation on SFT: Experiments show that standard Supervised Fine-Tuning (SFT) on the physics dataset leads to a 6.4% performance drop. In contrast, Rejection-Sampling Fine-Tuning (RAFT) and the proposed RLVR approach yield improvements, suggesting that aligning the model's output distribution with the training data (via RL or RAFT) is more effective than direct SFT for this domain.

Significance and Contributions

The paper claims three primary contributions:

1. First Domain-Specific Prover: It introduces the first methods specifically designed to train formal theorem provers for physics, addressing a critical gap in the literature where SOTA models fail on physics tasks.
2. Dataset and Pipeline: It develops and releases PhysLeanData, a compact but comprehensive dataset, along with a conjecture synthesis pipeline tailored for physical theorems, intended to benefit the research community.
3. Performance and Generalization: It demonstrates that a model trained on a small (~5K) physics dataset can outperform SOTA mathematical provers on physics tasks and simultaneously improve performance on general mathematical benchmarks.

The authors conclude that their work provides a paradigm for extending formal provers beyond mathematical domains. They emphasize that while current results are promising, the approach highlights the potential of using RLVR and high-quality, domain-specific data to overcome the limitations of general-purpose models in specialized scientific fields. The dataset and model are released to the community to foster further research.