SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

Summary (Overview)

• Key contribution: The paper introduces SCOPE (State-Conditioned Operator Planning and Execution), an architecture that separates theorem proving into three roles: a 135M-parameter language model as policy planner, a symbolic execution engine for numeric computation, and a template compiler for proof text generation.

• Core finding: Direct generation of multi-step numeric proofs fails due to an error-product structure—if each of $k$ load-bearing integers is correct with probability $p$, the pass rate is bounded by $p^k$. The paper verifies this power-law relationship empirically across 2,617 reference proofs.

• Main result: SCOPE certifies 191/218 (87.6%) problems on the test suite, compared to 18/218 (8.3%) for DeepSeek-Prover-V1.5-RL (7B) operating at 37.5× the wall-clock time, and 0/218 for DeepSeek-Prover-V2-7B.

• Key architectural insight: A factorial experiment shows that shifting the decision-frame state from a lagged to a current engine state raises the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss lowers it—demonstrating that information visibility at decision time matters more than loss allocation.

• Efficiency: The system produces zero natural-language thinking text, averaging only 6.12 decision actions per problem, 0.53 seconds per problem, and peaking at 833 MiB of inference memory.

Introduction and Theoretical Foundation

Background and Motivation

In proof assistants like Lean, generated proofs must pass machine compilation, eliminating the need for human scoring. However, direct generation of multi-step numeric propositions fails systematically: proofs are structurally conventional but break at concrete numeric values, ending with unresolved goals (sorry in Lean). This suggests the bottleneck lies in generating numeric content one item at a time rather than in selecting proof steps.

Theoretical Basis

The paper formalizes the error-product law: for a proof containing $k$ load-bearing integers, where integer $i$ is written correctly with independent probability $p_i$:

$$\text{Pass} = \prod_{i=1}^{k} p_i$$

When all integers share accuracy $p$, this yields the power-law bound:

$$\text{Pass} \leq p^k$$

Proposition 1 (product law and power-law bound): If a proof contains $k$ content integers, integer $i$ is written correctly with independent probability $p_i$, and certification requires all integers to be correct, then the pass rate is given by the product formula, and if no integer exceeds accuracy $p$, the bound $\text{Pass} \leq p^k$ holds.

Corollary (load correction): Let $S \subseteq \{1, \ldots, k\}$ be the set of load-bearing integers determined mechanically by controlled-corruption experiments; changing integers outside $S$ does not change certification outcomes. Thus:

$$\text{Pass} \approx p^{|S|}$$

Division-of-Labor Hypothesis

The authors test whether restricting the model's role to policy planning (choosing operators and arguments) while delegating numeric computation to symbolic tools and proof text to template compilation supports long-chain, multi-step, exact reasoning—mirroring human mathematical practice where tool selection is the core competence.

Methodology

Architecture Overview

SCOPE processes propositions through four stages:

1. Discrete representation: Problems are encoded as integer-vector states; solving is modeled as operator chains within a vocabulary of 194 operators (extended to 220 for the public library).

2. Symbolic execution engine: Deterministic map $E: (s, o, a) \mapsto (s', \text{cert})$ performing exact integer/rational arithmetic with mechanically checkable certificates per step. For the sum-of-squares family, the residual update is:

$$R_{\text{out}} = R_{\text{in}} - m\ell^2$$

where $R_{\text{in}}$ and $R_{\text{out}}$ are residuals before/after the step, $m$ is the coefficient of the removed square term, and $\ell$ is the linear form.

3. Chain-planning model: SmolLM2-135M backbone with two heads—operator selection and argument prediction (352 candidate values). The decision at step $t$:

$$(o_t, a_t) = f_\theta(s, h_1, \ldots, h_{t-1})$$

with probability distributions:

$$P(o_t = o | F_t) \propto \exp(z_o(o)), \quad P(a_t = v | o_t, F_t) \propto \exp(z_a(v))$$

Training objective (cross-entropy):

$$L = L_{\text{op}}(o_t, o_t^*) + \frac{1}{24}L_{\text{val}}(a_t, a_t^*)$$

with chain-end weighting configuration:

$$L_W = L + (\lambda - 1)\mathbb{1}[t=T]L_{\text{op}}$$

4. Proof compiler: Template-based expansion of operator chains into Lean tactic sequences; all numbers come from engine computation.

State Shift

The final configuration augments the decision framing with the current engine state:

$$(o_t, a_t) = f_\theta\left(s, h_1, \ldots, h_{t-1}, R_{\text{out}}^{(t-1)}\right)$$

where $R_{\text{out}}^{(t-1)}$ is the residual after executing step $t-1$.

Experimental Configurations

Empirical Validation / Results

Direct Generation Failure (Law 1)

• Token accuracy on held-out rows: 0.9637, yet certified passes: 0/218
• Per-integer accuracy ~0.79, ~14.9 content integers per proof → predicted pass rate ~0.031
• Controlled-corruption experiment on 2,617 proofs: measured pass rate 0.558 vs. theoretical 0.530 (relative excess ~5%)
• Deviations located at non-load-bearing positions: 0/432 coefficient/exponent corruptions survive; all 1,164 nested-induction and lemma-tower corruptions rejected

Compiler-Generated Proof Text

• Pass rate rises from 1/218 (slotting baseline) to 117/218
• Compiler reproduces reference proofs byte-for-byte on all 2,399 corpus rows; certifies 218/218 with reference chains
• Key equality: $\text{Pass} = P(\text{chain correct})$

Factorial Analysis (Law 2)

Proposition 2 (final-step conditional decomposition): With $B$ the set whose first $T-1$ steps are all correct and $C$ the set whose whole chain is correct:

$$\text{Pass} = A_{T-1} \cdot q_T$$

where $A_{T-1} = P(B)$ is prefix accuracy and $q_T = P(C|B)$ is conditional final-step accuracy.

Factorial results (n = 218):

Cross-Model Comparison

Cost Expressions

Per-problem cost of SCOPE:

$$C_{\text{sc}} = T(c_{\text{fwd}} + c_{\text{exec}}) + c_{\text{compile}}$$

Direct generation cost:

$$C_{\text{dir}} = N_{\text{gen}} c_{\text{tok}}$$

Domain Extension (Lean-Workbook)

• Full library: 132,378 rows (after excluding 7,448 library-corrupt rows)
• 48,106 rows admissible under operator system; 84,267 out-of-domain
• 3,536 rows enter review; 2,132 certify (60.29%, Wilson 95% CI: 58.67–61.89)
• Model-only chains on extension families: 45.10% (281/623 renderable rows) vs. family-tree chains at 44.07%

Theoretical and Practical Implications

Design Principle

The two empirical laws merge into one design principle: restrict the model's free-generation range and make the tool state needed for the verdict available at decision time. Within this domain, restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.

Evaluation Significance

• Token-level accuracy and chain-of-thought surface correctness can badly overestimate ability on long-derivation tasks
• In settings where proof validity is a Boolean conjunction, per-integer accuracy and element count are the quantities directly tied to pass rate
• The controlled-corruption experiment provides a mechanical way to measure load-bearing status of each integer position

Tool-Augmented Methods

The results emphasize timing and content of tool-state feedback beyond tool availability. The tool is available in every configuration; only the computation timing of the state differs, and that single difference moves the pass rate by 74 problems.

Auditability

The architecture's separation of responsibilities enables full inspection: model output is restricted to symbolic decisions, computation lives in a deterministic engine, and text comes from template compilation—each independently checkable. Error localization at decision-step granularity is possible (all 101 errors localize to the final step).

Conclusion

The paper establishes two empirical laws:

1. Law 1 (error-product structure): Direct generation pass rate is bounded by a power law in per-integer accuracy; token-level accuracy diverges from pass rate (0.9637 token accuracy with 0/218 passing).

2. Law 2 (information visibility): Inside a restricted decision space, information visibility is the first-order determinant of correctness; loss allocation is not. Correcting state timing alone lifts pass rate from 53.7% to 87.6%.

The SCOPE architecture achieves 87.6% certified pass rate on the 218-problem suite with a 135M backbone, at one to three orders of magnitude lower resource cost than 7B direct-generation models. All multi-step thinking occurs in the discrete decision sequence with no natural-language thinking text.

Future directions: Systematic validation on larger backbones, transfer to more problem families, and addressing corpus-mixing sensitivity for routing domain inclusion.