# Learned Interventions in Lean 4 grind

> Failure-triggered cascades of bounded lookahead rescue 90% of grind's rescuable failures with zero regressions, while static learned models fail to beat random on those same decisions.

- **Source:** [arXiv](https://arxiv.org/abs/2607.22972)
- **Published:** 2026-08-15
- **Permalink:** https://picx.dev/p/5M5L1t
- **Whiteboard:** https://picx.dev/p/5M5L1t/image

## Summary

# 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.**

| Policy (on the rescuable split-failures) | Rescue rate |
|---|---|
| grind (stock heuristic) | 0% |
| GBM cost model / generation rule | 30–46% |
| value-doom / failure-aware classifier | 46–53% |
| uniform random | 57% |
| 1-step lookahead (realized) | 100% |

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.**

| Cap $C$ (s) | 5 | 10 | 15 | 20 |
|---|---|---|---|---|
| Rescued (of 97) | 0% | 80% | 90% | 92% |
| Cost (s/decision) | 21 | 39 | 45 | 50 |

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.**

| Policy | Dynamic? | Rescue rate | Trials to rescue |
|---|---|---|---|
| stock grind | no | 0% | — |
| random single pick | no | 57% | 1 |
| random bounded probe | yes | ~100% | 1.6 |
| lookahead (try all) | yes | 100% | ≤ 4.6 |
| perfect order | — | 100% | 1.0 |

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

---

_Markdown view of https://picx.dev/p/5M5L1t, served by PicX — AI-generated visual whiteboard summaries of research papers._