Lean Have-Skeleton OPSD

The one domain where PI genuinely matters. Structural proof decomposition (have-skeleton) as PI gives +3.3pp on MiniF2F, while bare retry HURTS (-2.4pp). This proves PI has real value when solution paths are narrow and cannot be discovered by exploration alone.

Hypothesis

In Lean theorem proving, the proof structure (which sub-goals to establish via have statements) is crucial information that the model struggles to discover through random exploration. If the teacher sees the proof skeleton (intermediate have propositions without their proofs), it should generate better-structured solutions that transfer genuine strategic knowledge to the student.

Expected: Positive if structural information is genuinely privileged in formal domains.

Actual: +3.3pp, confirming that PI has real value for Lean when it takes a structural form.

Method

OPSD with have-skeleton PI:

1. Extract skeletons: For each proof in the training set, extract the have statement structure: the intermediate propositions the proof establishes, WITHOUT the tactic proofs of each have. This gives the proof's decomposition plan.
2. Teacher generation: The model generates proofs conditioned on the skeleton: "Given these sub-goals: [have h1: ..., have h2: ...], prove the theorem."
3. KL distillation: Train the student to match the teacher's output distribution WITHOUT seeing the skeleton at input time.
4. Eval: MiniF2F pass@1 (does the generated proof type-check?).

The skeleton provides STRUCTURAL information: which sub-goals to pursue. It does not provide TACTICAL information: which specific Lean tactics to use. This parallels the "strategic > specific" finding from math.

Configuration

Results

Method	PI Form	Pass@1	Delta
OPSD have-skeleton	Proof decomposition structure	42.6%	+3.3pp
OPSD proof-completion	Partial proof + state	41.4%	+2.1pp
OPSD proof-states-k3	Raw proof states	40.2%	+0.9pp
OPSD nl-strategy	NL proof strategy	40.2%	+0.9pp
STaR retry (no PI)	None	36.9%	-2.4pp
Baseline (no training)	-	39.3%	-

Why This Works (While Retry Fails)

1. Structural PI provides STRATEGY SELECTION: The have-skeleton tells the model WHICH sub-goals to establish. This is the hard part in Lean; once you know the decomposition, filling in individual tactics is relatively easy.
2. Narrow solution paths: Unlike math (10+ valid approaches) or code (many implementations), most MiniF2F theorems have 2-3 viable proof strategies. Random retry cannot reliably hit the right one.
3. Type-checker verifiability: Lean's type-checker provides a perfect binary verifier. Combined with structural PI that guides strategy, this produces clean training signal.

The hierarchy of PI forms (skeleton +3.3 >> partial proof +2.1 >> raw states +0.9 ~ NL strategy +0.9) confirms that STRUCTURAL information (decomposition plan) is the valuable component, not raw proof traces or natural-language descriptions.

Training Curves

At: /data/ughai-sandbox/opsd_experiments/lean_have_skeleton/. Smooth convergence. Eval improves steadily through 500 steps with no overfitting (validation continues improving). The structural PI produces clean, consistent training signal.

Interpretation

This is the one result that saves PI distillation as a concept. It shows that PI is NOT universally useless; rather:

• When solution paths are diverse (math, code): Retry dominates because the model can find alternatives by exploration. PI content is irrelevant.
• When solution paths are narrow (Lean): PI provides genuine value because it selects the strategy the model cannot discover by trial-and-error. OPSD works here.

The practical boundary: PI matters when solution_path_diversity < threshold. Below this threshold, the model needs external guidance on WHICH approach to take.

Connection to Other Experiments