Proof assistant model plans symbolic steps to certify numeric proofs
SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
Artificial Intelligence
Summary
Automatically generating proofs for math problems is hard when numbers must be exact at every step. The authors found that directly generating full proofs often fails because even small errors stack up quickly. Their system, called SCOPE, uses a language model to plan symbolic steps while relying on a separate engine to handle precise number calculations. This approach greatly increases the rate of correct, machine-verifiable proofs on tested problem sets compared to prior methods.
What this means in practice
- •For software verification teams: Automatically certify complex program properties involving numeric reasoning by combining symbolic planning with numeric execution.
- •For automated theorem proving engineers: Increase automated proof success rates on numeric problems through structured operator planning paired with verified execution engines.
Authors
Hanchao Zhou, Jialei Li
Abstract
In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 6.12 discrete decision actions per problem and produces no natural-language thinking text. Replacing the lagged engine state in the decision frame with the current one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. On the public Lean-Workbook library, 2,132 of 3,536 gradeable admissible problems certify (60.29%) with zero regression on the main suite. All readings come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.