Learned Interventions Inside Lean 4's grind

Summary (Overview)

• Failure-triggered cascade design: The authors introduce a deployment pattern where learned interventions are invoked only after stock grind fails, guaranteeing by construction that the intervention cannot regress proofs the baseline already solves.
• Two implemented interventions: A cost-aware e-match filter (improves speed ~5% and recovers +2 solves on 855 held-out theorems) and a bounded lookahead procedure for case-splitting (rescues 5 stock grind timeouts with zero regressions).
• Key negative result: Static feature-based models for predicting the correct case split perform no better than random on the "rescuable" failures—the decisions where grind's own heuristic was wrong—because branch explosion is a dynamic property not captured by static features.
• Lookahead beats static prediction: A non-learning bounded probe that actually executes candidate splits under a time cap rescues ~90–100% of rescuable failures, demonstrating that dynamic execution is the key lever, not static scoring.
• Design principle: Learning within theorem-proving tactics is best used to decide when and how to spend bounded search, backed by a reliable symbolic fallback.

Introduction and Theoretical Foundation

Automated theorem provers increasingly rely on a small number of powerful tactics as reasoning backends, making the internal search decisions of those tactics high-leverage targets for learning. However, these decisions are difficult to learn safely: a heuristic that appears better locally may change the shape of symbolic search enough to create new blow-ups, causing regressions on goals the original tactic already solved.

The paper studies this problem within grind (Lean FRO, 2024), a tactic for the Lean 4 proof assistant (Moura & Ullrich, 2021) that integrates SMT-style automation into Lean by combining:

• Congruence closure (Nelson & Oppen, 1980)
• e-match-based lemma instantiation (Moura & Bjørner, 2007)
• Case splitting

The core complication is that grind's search is nonmonotone: e-matching can grow very quickly, so a choice that appears better short-term may make overall search worse. In experiments, always-on learned replacements solve some goals stock grind misses but also break goals stock grind already proves.

The paper's key insight is to use learning more conservatively: rather than predicting the right choice from static features, run a cheap lookahead triggered only after stock grind fails. This gives a failure-triggered cascade: stock grind is tried first, and interventions apply only to goals it leaves open.

The action loop of grind is schematically:

$$\text{solvers} \triangleright \text{instantiate} \triangleright \text{splitNext} \triangleright \text{mbtc}$$

The loop repeats until fixpoint or heartbeat exhaustion. Three insertion points for learned guidance are identified:

1. e-match instance filter — discards low-value instantiations before they enter the congruence structure
2. split-target selection (implemented by splitNext) — chooses which goal to split next
3. premise augmentation — chooses facts to assert before search begins

Methodology

Model Architecture

The e-match filter is a binary classifier scoring each candidate instantiation for proof-relevance (whether it appears in the final proof term). Features include:

• Lemma identity, head symbol, conclusion tokens, premise tokens
• Matching features of the current goal
• Numeric signals: e-matching round, lemma usefulness frequency

These form a 135-dimensional vector fed to a three-layer MLP:

$$135 \rightarrow 64 \rightarrow 32 \rightarrow 1$$

trained with binary cross-entropy. The split-study models are similarly small: MLPs and gradient-boosted trees over goal- and candidate-level features.

Oracle Experiment for Split Decisions

To study split-target selection, the authors run an oracle experiment: at each multicandidate decision, each candidate is forced in turn, grind is rerun with the rest of the proof fixed, and the outcome recorded. This yields approximately 16K forced-choice outcomes from 4,120 multicandidate decisions over the NUMINA benchmark.

Lookahead Procedure

For each split candidate, the policy:

1. Makes a throwaway copy of the goal
2. Forces that split
3. Runs grind on the copy for a bounded number of steps (time cap $C$)
4. Commits to the first candidate whose trial closes; discards other copies

Since the trial actually executes the split, it observes the dynamic behavior that static models miss.

Empirical Validation / Results

E-match Filter Results

On a held-out suite of 855 theorems:

• Runs ~5% faster
• Recovers +2 solves over stock grind
• Scaling training data by 20× does not broaden the niche, suggesting a limitation of the lemma-identity mechanism rather than data scarcity

Oracle Study of Split Decisions

• An oracle choosing the cheapest split reduces total splits by only ~4%
• In 675 decisions, grind's chosen split leads to timeout
• In 97 of those (14%), at least one other available split closes the goal without new lemmas — these are the rescuable failures

Table 1. Static-feature policies do not beat random on the rescuable split failures.

Four static policies were tried: a gradient-boosted cost model (Chen & Guestrin, 2016), a generation-ordering rule, a doom/value model, and a failure-aware success classifier with candidate AUC 0.85 on by-decision held-out data. None beats random on the rescuable decisions, despite strong aggregate metrics.

Table 2. Time-capped lookahead on the rescue decisions.

At $C = 15$ s, lookahead rescues 90% of rescuable failures at lower cost than the ~53 s grind spends on its bad choice.

Live Deployment Results

On the 44 theorems whose traces contain a rescue decision:

• Stock grind: solves 39, times out on 5 (deterministic 400K-heartbeat budget)
• Always-on lookahead: solves 42 (rescues all 5 failures, but regresses on 2 stock solves)
• Cascade (stock first, lookahead only on failures): solves 44/44 theorems (vs. 39/44 stock), a net gain of 5 with zero regressions, using fewer total splits (1059 vs. 1271)

When lookahead works: The 5 rescued theorems have shallow rescues (branch closes within ~9 further splits after the right split). The 2 regressions require deeper commitments (10–57 splits deep, sometimes across several sequential decisions).

Table 3. On rescuable decisions, dynamic execution is the lever.

A non-learning probe trying candidates in random order until one closes rescues nearly all (~96%) in ~1.6 candidate trials on average, while learned static policies fall below even the random single pick.

Theoretical and Practical Implications

1. Static prediction is insufficient for high-impact decisions: The negative result (Table 1) shows that four different learned models perform no better than random precisely where grind's heuristic fails. The cost of a branch is often visible only after taking it, making it a dynamic property.

2. Dynamic execution is the key lever: Table 3 demonstrates that a non-learning random-order bounded probe captures nearly all the benefit of perfect lookahead. The role for learning shifts to:

   • A gating policy: deciding when lookahead is worth its cost
   • A candidate-ordering policy: reducing average probe cost toward the perfect-order baseline of 1 trial

3. The cascade discipline generalizes: The same recipe extends to premise augmentation—adding premises only as a retry after grind fails preserves rescues without regressions.

4. Safety by construction: The failure-triggered cascade guarantees no proof that stock grind already solves can be lost, addressing the fundamental nonmonotonicity problem of learned heuristics in symbolic search.

Conclusion

The authors integrated learning into Lean 4's grind at several internal call sites with two problem-level improvements:

• A cost-aware e-match filter gives small success and speed gains on a held-out suite
• A bounded lookahead cascade proves five theorems stock grind cannot, with zero regressions

The results support a simple rule: preserve the symbolic solver as the default, and use learning to decide when and how to spend bounded search on the failures it leaves behind.

Two future directions are identified:

1. Gating and ordering models: A gating model deciding when lookahead is worth running, and an ordering model reducing average candidate trials per rescue toward the perfect-order baseline of 1
2. Learned premise retrieval: Extending the cascade pattern to a learned premise retriever, protecting it from regression in the same way