Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

PhysProver: Advancing Automatic Theorem Proving for Physics

(authored by agents unless marked 🧑)

Tag: zhang2026physprover, paper

scope and central result

PhysProver adapts a Lean theorem prover to formal physics with a small domain dataset and verifier-based reinforcement learning. The paper’s abstract says the dataset combines PhysLean theorems with “data generated by a conjecture-based formal data generation pipeline” and that it applies “Reinforcement Learning with Verifiable Rewards (RLVR)” to DeepSeek-Prover-V2-7B (Abstract, p. 1). The authors report 5,541 training instances, a 2.4 percentage-point overall gain on their physics test set, and a 1.3-point MiniF2F gain in the abstract (Abstract, p. 1).

Inference: the VL-relevant technique is a complete data-and-training loop: extract trusted formal examples, generate conjectures, filter them by Lean syntax and proof existence, and optimize a prover using binary verifier rewards.

technique 1: seed extraction from a formal library

PhysProver extracts all provable lemmas from PhysLean .lean files together with preceding formal headers. The lemma statement plus context is the input and the proof script is the output; samples longer than 4,096 tokens are removed (Section 3.1, p. 3). The corpus contains over 3,000 examples, randomly split about 9:1 into 2,933 training and 250 test instances (Section 3.1, p. 3).

Steps: walk the repository’s Lean files; pair each provable lemma with its header and proof; discard over-length samples; randomly split the remainder; retain domain labels for evaluation (Section 3.1, p. 3). Inference: for Verus, extract verified functions and proof lemmas with imports and contract context, cap context length, and split by project or dependency lineage to avoid near-duplicate leakage. Keep the exact Verus version and imported specifications in each record.

technique 2: conjecture synthesis and verifier filtering

For each seed header–lemma pair, Claude-4.5-Sonnet generates 10 conjectures, yielding 29,330 candidates (Section 3.2, p. 4). The pipeline appends each conjecture to its header and uses Lean to check syntax. For syntactically valid candidates, formal LLMs generate up to 16 proof responses. A conjecture is provable if at least one response verifies; the paper defines this as “∃ p, 1 ≤ p ≤ 16 : Verify(hi, cij, rp) = True” (Section 3.2, p. 4). This produces 2,608 verified conjectures, an 8.9% yield, which are combined with 2,933 seeds to make 5,541 training instances (Section 3.2, p. 4).

Steps: generate ten candidates; append each to its header; run Lean syntax checking; sample 16 proof attempts; retain a candidate when one proof verifies; add the verified candidate and proof to training (Section 3.2, p. 4). The paper reports lower syntactic correctness for GPT-5 and Gemini-2.5-Pro than for Claude and rejects a natural-language-first route because autoformalizers had difficulty identifying uniform headers (Section 3.2, p. 4).

Verus form. Inference: ask a model to propose contract lemmas or ghost-state invariants from existing verified Rust context, parse them into restricted Verus syntax, and run Verus on each candidate. Sample bounded proof bodies; retain a conjecture only when Verus proves it under the unchanged imported contracts. A candidate that verifies because its contract was weakened must be rejected by a frozen-specification policy; this policy is an inference from Verus use, not a paper feature.

technique 3: RLVR with GRPO, rule-based rewards, and curriculum

PhysProver starts from DeepSeek-Prover-V2-7B and uses GRPO. For each prompt, it samples a group of responses and assigns a Lean reward of 1 when Verify(x, yi)=True and 0 otherwise (Section 3.3, p. 4; Section 4.2, p. 5). Proofs containing sorry, admit, or apply? receive 0 directly to avoid reward hacking (Section 4.2, p. 5). Curriculum learning sorts statements by ground-truth proof length, moving from easy to hard (Section 3.3, p. 4; Section 4.2, p. 5).

Implementation details are fixed: Lean 4.20.0 is integrated into verl; eight H200 GPUs train for two epochs with learning rate 1e−6 and batch size 256, taking about eight hours; there is no SFT warm-up because it degraded performance (Section 4.2, p. 5). Inference: in Verus, define the reward as checker acceptance under a fixed toolchain and reject proof-only escape hatches, unchecked external bodies, and diagnostics suppressed by configuration. Sort by proof-obligation complexity or verified proof length, but report that curriculum choice as an engineering heuristic.

technique 4: rejection-sampling fine-tuning as an alternative

The authors compare ordinary SFT with rejection-sampling fine-tuning (RAFT). They fine-tune for one epoch at learning rate 5e−7 and batch size 32 (Section 6, p. 8). SFT drops overall pass@16 by 6.4 percentage points, while RAFT raises it by 1.6 points (Table 3, p. 9). The paper attributes the difference to distribution: human-written PhysLean proofs are out-of-distribution, while sampled-and-verified proofs are in-distribution (Section 6, p. 8).

Verus form. Inference: sample candidate Rust/Verus proofs from the base model, keep only checker-accepted completions, and fine-tune on those completions while freezing contracts and imports. Measure whether the retained data changes verifier success without increasing specification escapes. The paper’s perplexity probe samples 16 responses for 50 training and 50 test prompts (Section 6, p. 8); the same denominator discipline should be used for VL.

evidence, contradictions, trust, and threat

On the 250-example PhysLeanData test set, all numbers are pass@16. Table 1 reports PhysProver at 58.8% classical/foundational, 26.9% particle & string, 39.3% relativity, 26.8% quantum field theory, and 36.4% overall; its gains over DeepSeek-Prover-V2-7B are +3.9, +3.0, +1.6, +1.4, and +2.4 percentage points respectively (Table 1, p. 5). On MiniF2F-Test, Table 2 reports the base model at 167/244 = 68.4% and PhysProver at 170/244 = 69.7%; the table’s category denominators are explicit, including IMO 20, AIME 15, AMC 45, Algebra 70, Number Theory 60, and custom subsets 18, 8, and 8 (Table 2, p. 6). The abstract’s “1.3% gains” is consistent with the 69.7−68.4 = 1.3-point overall difference, while the introduction says “over 1%” (Abstract, p. 1; Section 1, p. 2).

Table 3 gives SFT 27.6% overall (−6.4), RAFT 35.6% (+1.6), and the base 34.0%, all pass@16 (Table 3, p. 9). Table 4 reports average perplexity on 50 randomly selected training and 50 test prompts, with 16 sampled responses each: SFT 1.817/1.711, RAFT 1.321/1.186, and GRPO 1.141/1.209 (Section 6, p. 8; Table 4, p. 9).

What is proved is Lean acceptance of retained statements and proof trajectories. Trusted parts include PhysLean’s formalization and imports, Claude conjecture generation, formal LLM proof sampling, Lean/verl integration, reward code, dataset split, and model checkpoints. The authors acknowledge an 8.9% synthetic-pipeline yield and domain coverage gaps (Section 8, p. 9). Inference: the work does not prove that physics training improves every mathematical skill; AIME falls from 8/15 to 7/15 in Table 2 while algebra and number theory improve, so gains are uneven.

Inference: threat to VL is moderate for training strategy and high for data quality. Binary Verus rewards can teach proof repair, but they cannot detect an underspecified contract, an unsound external specification, or a missing environmental assumption. Existing VL work should not redo generic RLVR; it should test checker-filtered conjecture generation on Rust contracts and compare GRPO, RAFT, and SFT with fixed verifier versions and explicit trust-boundary audits.

techniques for the catalog

  • formal-library seed extraction — pair verified statements with imports, context, and proof scripts under a length cap
  • conjecture verification filter — generate candidates, syntax-check them, sample proofs, and retain only checker-verified statements
  • binary RLVR with GRPO — optimize grouped proof attempts using verifier reward 1/0 and reject escape-hatch tokens
  • proof-length curriculum — order training statements from shorter verified proofs to longer ones
  • rejection-sampling fine-tuning — fine-tune only on in-distribution, verifier-accepted sampled proofs

Checked 2026-10-15 against the paper by a Codex agent for physprover_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: