Depth, dependency, and the cost of binary grading

What the kernel doesn't tell you

A reinforcement learning algorithm against a proof kernel is a good idea because the reward is not a proxy. A unit test will be satisfied by code that satisfies the test and nothing more; a proof kernel will not be satisfied by anything that is not a valid proof. That is the case for verifier-reward RL as a way around reward hacking.

What is left unsaid is the task itself, how difficult it is, and whether the number the verifier returns is the number to be optimized. A kernel is a function mapping (statement, candidate) to accept/reject. Building an environment on top of it means answering all three.

The corpus

The corpus is built around a 784-line, sorry-free type soundness theorem for the Volpano–Smith–Irvine information-flow security system, extended with function calls and proven to still satisfy noninterference, in Lean 4, whose only non-constructive dependencies, per #print axioms, are propext and Quot.sound. Around it, 12 information-flow-control theories are generated automatically over a small parameter space, from public agreement up to the soundness theorem, plus a synthetic noninterference control family used to check that extraction and calibration aren't an artifact of the one proof done by hand. In total: 14 theories, 158 lemmas, 2,607 distinct task instances, 158 shapes, where a shape is a (target, withheld set) pair.

A lemma's depth is the length of the longest dependency chain ending at it: 1 if it depends on nothing else in the theory, otherwise one more than the deepest lemma it needs. Reward is kernel acceptance plus an axiom audit, which is not redundant with compilation: a lemma can fail to compile for one reason while still being declared, with every citation of it still compiling, if the failure is captured by sorryAx or an accidental axiom, so no proof is accepted whose axiom set exceeds the family's allowed set.

Dependencies, measured by necessity

In Lean 4.32 a theorem's proof term is elaborated asynchronously, and the environment does not retain it once the declaration is checked. Every way of reconstructing the dependency graph via ConstantInfo.value? applied to compiled theorems yields none, and an extractor built on it would claim every theorem is dependency-free.

The graph is reconstructed with necessity instead: there is an edge T → A if removing A from the file breaks T's proof term compilation. This is strictly more powerful than parsing proof terms even where that is possible, since a name can appear in a proof term without being load-bearing to it. Handling rungs in source order lets a full transitive cone of each ancestor be deleted at once, and a subsequent transitive reduction removes edges implied by other edges.

Binary grading distorts a compositional difficulty curve

All-or-nothing grading of a multi-lemma problem is the obvious choice when using a kernel, but a bad one for assessing the difficulty of composition. If a policy proves each required lemma of a depth-d task independently with fixed probability q, and the number of required lemmas k grows with d, then binary pass rate is q^k, decaying geometrically even when per-lemma competence does not decay with depth at all. Per-target score, the fraction of required lemmas individually accepted, has expectation q, invariant to k. The kernel had this information the whole time; the binary reward discarded it.

The compositional claim at scale

If per-target credit really corresponds to policy competence, then supplying the dependency cone for a task should help, since the lemmas no longer need to be recomputed. For each task between depths 2 and 4, two arms were run: supplied, where the ancestors of the lemma being proved are provided along with their correct proofs, and withheld, where they are not. Across depths 2 to 4: 23 of 35 successes for supplied, 9 of 34 for withheld. Fisher's exact test gives p = 1.6×10⁻³ with duplicate removal, and p = 5.2×10⁻⁴ without, so the choice of analysis no longer changes the conclusion at this sample size.

Why the first training run stalls

The initial GRPO run on the kernel raised pass@1 from 0.005 to 0.021 within roughly four hours, then stopped. GRPO's advantage is calculated from the variance of the reward inside one set of rollouts from the same prompt; at a 0.5% success rate, the probability of getting both successes and failures in an 8-rollout set is low enough that 96% of such sets give exactly the same reward value, so the advantage is always zero. The model was getting a gradient update for only 4% of its samples, and nothing shows up in the loss chart, since a flat advantage produces a well-defined, differentiable, and entirely uninformative loss.

Five interventions, all aimed at the same quantity, the probability that a sampled group contains two different outcomes, move a run off this floor:

• Expert-iteration cold start.Sample/grade/mine/fine-tune iterations on the kernel before GRPO starts, limited to depths 1–2: a cold policy that can't reach depth-4 problems produces nothing, at the same grading cost as if it could solve them.
• Per-target credit assignment. One advantage per graded item in a compositional task rather than one scalar per rollout. At group 8, depth 3, this is 24 advantages per group instead of 8.
• A dynamic, difficulty-ledger-driven sampler.Prompts are tracked as informative, trivial, or hopeless from their observed reward history, with a fixed share reserved for prompts the ledger hasn't seen yet.
• Between-stage distillation. Every kernel-verified proof produced during a stage is banked and used for a short supervised pass before the next stage begins, free to collect since the rollouts are already graded.
• Automatic stall detection with expert-iteration rescue.When a stage's groups go stale, one expert-iteration round runs at that stage's depths and the stage retries, up to a fixed retry budget.

Results

A domain-specialized 7B prover (DeepSeek-Prover-V2-7B), carried through the full curriculum (depths (1,2) → (2,3) → (3,4) → all, each stage measured by held-out evaluation before the next begins) reaches, on the same vsi held-out split:

Binary pass@1 is exactly zero at every depth past 1: a curve indistinguishable, on its face, from a model that has proven nothing past the easiest tier of the corpus. Per-target score decays smoothly instead, a policy visibly and gradually running out of ability rather than falling off a cliff at depth 2.

Depth-(2,3) trains cleanly once given adequate memory headroom, and the checkpoint after it already improves on every metric over the depth-(1,2)-only checkpoint before it. The curriculum keeps improving through depth-(3,4) before a small, within-confidence-interval dip at the final all-depths stage, read as a plateau: the 95% confidence intervals on the pooled score overlap between the two final stages, and 48 tasks per depth at group 8 still isn't enough to tell a true plateau from measurement noise at this resolution.

Summary

An environment for information-flow security verification in Lean 4, where the difficulty control is a dependency cone obtained via necessity and not an assumption, where the reward is kernel acceptance plus an axiom audit, and where the primary formalization is machine-verified without sorry constructs. First with a hand-curated dataset, then pooling across 134 examples, binary assessment of a compositional task skews the difficulty curve it supposedly measures, in a way per-target regrading of the same responses fixes. The first attempt to train on this reward fails because rollout groups get stuck at a success rate where policy-gradient advantage is zero by construction; five interventions fix that, and the full curriculum result on a specialized 7B prover follows: pass@1 zero beyond depth 1, per-target score a smooth curve through depth 4.

RL environment and training code: lean-proof-environments. Source type system: type-system-for-noninterference.