Learned Interventions in Lean 4 grind

Evan Wang; Simon Chess; Sophie Szeto; Theodore Meek

REVIEW 4 major objections 4 minor 20 references

This paper argues that learned guidance inside a non-monotone symbolic tactic like Lean's grind is safest and most effective when deployed as a failure-triggered cascade — run the stock tactic first, intervene only on failures — and shows t

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 03:58 UTC pith:VT3IYLSM

load-bearing objection A genuinely useful safety pattern and a convincing negative result, but the headline +5 is from a hindsight-selected set and the deployed split policy isn't learned. the 4 major comments →

arxiv 2607.22972 v2 pith:VT3IYLSM submitted 2026-07-25 cs.LG

Learned Interventions in Lean 4 grind

Evan Wang , Simon Chess , Sophie Szeto , Theodore Meek This is my paper

classification cs.LG

keywords learned interventionstheorem provingLean 4grind tacticnon-monotone searche-matchingcase splittinglookahead

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper claims that learning inside a non-monotone theorem-proving tactic is safest and most effective when deployed only after the stock tactic has failed. It demonstrates this with Lean 4's grind: a cost-aware e-match filter and a lookahead split policy are inserted as failure-triggered cascades, so they cannot regress proofs grind already solves. On the evaluated trace, the cascade rescues all five stock-grind timeouts among 44 theorems, while an always-on version breaks two previously solved goals. The paper also reports that static feature-based models cannot predict which case split explodes, supporting the design choice: dynamic execution, not static prediction, is the lever.

Core claim

grind's search is non-monotone, so a learned heuristic that helps one proof can break another; always-on replacements net out near zero. The paper's central discovery is that invoking a learned intervention only after stock grind fails — a failure-triggered cascade — makes capability gains additive by construction: the base solver's solved set is untouched, and rescues add on top. A bounded lookahead that force-runs candidate splits on discarded goal copies recovers 90% of rescuable failures under a 15-second cap, and in the live experiment the cascade solves 44/44 theorems versus 39/44 stock, a net +5 with no regressions.

What carries the argument

The failure-triggered cascade: run stock grind first; only on goals that remain open, apply the intervention. The lookahead split policy turns split selection into a small experiment — for each candidate, copy the goal, force the split, run grind on the copy for a bounded number of steps, and commit to the first candidate whose trial closes. This probes the dynamic branch-explosion behavior that static features miss.

Load-bearing premise

The claim that the cascade cannot lose a proof grind already had, and the observed +5, rests on the premise that the evaluated 44 theorems whose traces contain a rescue decision are representative of grind's real failure distribution; if rescuable failures are rare in the broader pool, the net gain does not generalize.

What would settle it

Run the failure-triggered cascade on a fresh random sample of stock-grind timeouts drawn from a larger theorem pool than the 44 trace-selected theorems; if the rescue rate per timeout is near zero, or if regressions appear on previously solved theorems outside the hold-out set, the cascade's no-regression guarantee and the +5 result do not transfer.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

A learned (or even non-learned) probe can be inserted into a non-monotone tactic without endangering existing proofs, provided it runs only after base failure.
The +2 e-match filter and +5 lookahead suggest small, targeted interventions can yield capability gains; scaling training data does not necessarily broaden the niche.
Static feature models are likely to underperform on decisions where the cost is dynamic; lookahead or rollout-based policies are the natural alternative.
The cascade principle transfers to other tactic internals, including premise augmentation, which the paper shows nets about zero always-on but can bank rescues when failure-triggered.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

One testable extension: use the lookahead trial cost itself as a feature for a meta-model that decides when to probe, instead of always probing on failure; the paper leaves this as a stated direction.
The same failure-triggered pattern might apply to other proof assistants and solvers with non-monotone search, where a port could measure whether rescues generalize beyond the benchmark used here.
An editor's inference: the paper's own data suggest a possible ceiling — if most failures are 'idea gaps' rather than wrong split choices, the rescue pool is bounded, so the +5 may not scale to arbitrary new problem distributions.
A minimal non-learning probe with random candidate ordering already captures most of the benefit, which suggests that the value of learning in this regime lies in gating and ordering, not in identifying the correct split from static features.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

A genuinely useful safety pattern and a convincing negative result, but the headline +5 is from a hindsight-selected set and the deployed split policy isn't learned.

read the letter

Punchline: the failure-triggered cascade is the real contribution, and the negative result about static split prediction is the strongest evidence. The +5 solve claim is real but comes from 44 theorems chosen because their traces already contain rescue decisions, so it doesn't tell you how often such rescues exist in general. Don't let the title oversell it: the deployed split policy is a non-learned bounded probe.

What's new and good. The cascade pattern—run stock grind first, intervene only on failures—is clean and safe by construction; it gives a principled answer to the non-monotonicity problem. The negative result is more than a null: four static models with decent aggregate AUC all fail to beat random on the rescuable failures, which is a nice demonstration that branch explosion is dynamic. The e-match filter work is honest: +2 solves on 855, ~5% faster, scaling plateaus, synthetic sweep inert. The appendix tables and the discussion of what lookahead can and cannot do show the authors know the limits.

Soft spots. The 44/44 live evaluation is the big one. The set is selected by hindsight—theorems whose traces contain a rescue decision—so the 5 rescues are not an independent measure on a general benchmark. There's also an apparent internal inconsistency: if a rescue decision is defined as one where grind's default split leads to timeout, then any theorem with such a decision should be a stock timeout, yet only 5 of 44 time out. Either the definition is used differently in live evaluation or the paper's wording is wrong; either way, it needs auditing. Only 7 per-theorem cases are listed, not the full 44. Second, the deployed lookahead is not learned; it's a first-closing candidate probe, and Table 3 credits a random-order probe with ~96% rescue. The learned gating/ordering is proposed as future work, so the abstract's last sentence is a suggestion, not a demonstrated result. Third, code and data are referenced but not linked with a commit hash; for an empirical paper on a specific tactic version, that's important.

Who it's for: someone working on learned ITP or solver heuristics will get value from the cascade pattern and the negative result; the specific NUMINA numbers matter less. It deserves a serious referee, but it needs revision: clarify the 44-theorem definition, release code and per-theorem data, and ideally add a broader benchmark that doesn't preselect rescuable failures.

Referee Report

4 major / 4 minor

Summary. The paper proposes a failure-triggered cascade for learned interventions inside Lean 4's grind tactic: run stock grind first and apply a modified heuristic only to goals that stock fails to solve, so that the intervention cannot regress existing solves. It reports three components: a learned e-match instance filter (small solve gain, ~5% faster) on 855 held-out theorems; a bounded lookahead split policy that, in a cascade, solves 44/44 on a selected 44-theorem subset versus 39/44 for stock, rescuing five stock timeouts with no regressions; and a negative result that four static split-prediction policies do not beat random on 97 'rescuable failures.' The paper also reports honest scaling plateaus and an added-premise oracle study.

Significance. If the empirical claims hold, the paper makes a useful methodological point: for non-monotone tactics, learning should be deployed as a fallback that runs bounded experiments rather than as an always-on replacement, and static features may not capture branch explosion. The paper is commendably transparent: it includes per-theorem detail, negative results, a scaling plateau, an explicit statement that the deployed lookahead is non-learned, and a code repository. However, the headline +5 comes from a hindsight-selected set, and the successful split intervention is not itself learned; the general significance depends on clarifying the set-construction rule and the resource accounting.

major comments (4)

[Section 5, Table 4] The term 'rescue decision' is used inconsistently. Earlier in Section 5 a rescuable failure is defined as a decision where grind's chosen split leads to a timeout and another available split closes the goal. A theorem containing such a decision should be a stock timeout, yet the live set reports 39/44 stock solves. If the live set instead uses a weaker notion—any decision where the lookahead probe finds a closing trial—that must be stated explicitly. The paper does not specify how the 44 theorems were selected, from what pool, or with what hindsight. Table 4 lists only the 7 decisive cases, not the full 44. As written, the 44/44 and '+5' headline results are not auditable and risk being an artifact of set construction.
[Section 5/6, '400K-heartbeat budget'] The resource accounting for the cascade is unclear. The paper gives stock grind a deterministic 400K-heartbeat budget, then runs lookahead only if stock fails. It does not state whether the lookahead phase is charged to the same budget or receives a fresh heartbeat allocation. Reporting 'fewer total splits' (1059 vs 1271) does not resolve this, since heartbeats and wall time are the constrained resources. If the cascade is allowed additional search after a stock timeout, the 39/44 vs 44/44 comparison is not like-for-like and the +5 could partly be a budget effect. Please report total heartbeats or wall-clock time for stock, always-on, and cascade on the same 44 theorems, and specify the budget semantics for the fallback phase.
[Title/Abstract and Section 6] The paper's central capability gain is produced by a non-learned mechanism. Section 6 states that the deployed split policy is a greedy first-closing probe, and Table 3 shows a random-order bounded probe recovers ~96% of rescuable failures. The four learned static policies are at or below random. Thus the '+5' result is not evidence for a learned intervention; the only learned component with a positive problem-level result is the e-match filter, whose +2 is described in Section B as three near-duplicate recurrences minus one loss. The proposed learned gating/ordering model is not implemented or evaluated. The title and abstract overstate the role of learning and should be scoped to match what was actually built and measured.
[Table 1, Section C] The negative result that static policies 'do not beat random' lacks uncertainty quantification. The rescuable-failure set has n=97 decisions; the point estimates 46–53% for the learned policies are within a few standard errors of the 57% random baseline (standard error about 5 percentage points). Report confidence intervals or bootstrap intervals for each row, the number of random seeds/trials for the 57% estimate, and a per-decision paired test. Without this, the strong claim that static prediction is no better than random is not established beyond this sample, and the comparison may be underpowered.

minor comments (4)

[Section 5] The phrase 'without new lemmas or extra search' is confusing, because the alternative split is itself an executed search. Rephrase to say 'without additional premises and within the same forced-run continuation.'
[Section D, Table 5] The failure-triggered premise retry is not implemented; Table 5 is an oracle study. Please label it as an oracle/thought experiment rather than implying it is part of the implemented cascade.
[Abstract/Contributions] Please specify in the abstract and contribution list that the lookahead split policy is non-learned and that the learned role (gating and ordering) is proposed but not evaluated.
[Table 4] Only 7 anonymized IDs are given for the decisive cases. Please provide the full per-theorem table for all 44 theorems (IDs, stock/lookahead/cascade outcomes, rescue depth) in an appendix to make the live result auditable.

Circularity Check

1 steps flagged

Live lookahead evaluation is selected on the outcome it reports: the 44-theorem set is defined by containing rescue decisions, so the +5 gain is partly a restatement of the selection criterion.

specific steps

self definitional [Section 5, 'Proving theorems stock grind misses' (and oracle definition preceding it)]
"In 675 decisions, grind’s chosen split leads to a timeout. In 97 of those decisions (14%), at least one other split available at the same point closes the goal without new lemmas or extra search. We call these the rescuable failures: ... On the 44 theorems whose traces contain a rescue decision, stock grind solves 39 and times out on 5 ... On this set, the cascade solves 44/44 theorems instead of 39/44, a net gain of 5 with no regressions."

A 'rescue decision' is defined, in the oracle study, as a decision where an alternative available split closes the goal. The live evaluation set is then defined as the theorems whose traces contain such a decision. The five stock timeouts in that set are therefore already certified by the oracle as having a rescuing split, so reporting the cascade's +5 as a gain is largely a restatement of the set-construction criterion rather than an independent estimate of how often the intervention helps on a general benchmark. The zero-regression part is similarly definitional, since the cascade runs stock first and invokes lookahead only on stock failures, which the paper itself labels 'by construction.'

full rationale

Most of the paper is not circular. The 855-theorem suite and active-split benchmark are programmatically excluded from training (Section A), so the e-match filter's +2 solves and speed gain are genuine held-out measurements. The negative split-prediction result is evaluated on by-decision held-out forced-choice labels from an oracle, not on the learned models' own outputs, so that negative result is also independent. The cascade safety claim ('cannot lose a proof grind already had') is explicitly a construction, not an empirical discovery. The one load-bearing step with a definitional flavor is the live lookahead evaluation: the 44 theorems are selected because their traces contain a rescue decision, and a rescue decision is earlier defined as a decision where an alternative split closes the goal. The five stock timeouts in that set are already oracle-certified as rescuable, so the reported +5 is a verification that the implemented probe recovers oracle-known rescues under its budget, not an estimate of general usefulness. The paper is transparent about the scoping ('On this set') and about the deployed probe being non-learned, which keeps the circularity partial rather than total.

Axiom & Free-Parameter Ledger

4 free parameters · 4 axioms · 0 invented entities

The central results rest on a handful of domain assumptions about grind's search behavior and on hand-tuned thresholds; no new entities are introduced. The three main analyses are empirical, with held-out evaluation, so they are not circular in the fitted-value sense, but the selected 44-theorem evaluation limits generalization.

free parameters (4)

e-match filter threshold τ and per-round drop ratio = not given; swept over five settings
Controls which instantiations are dropped; the reported 833/855 depends on this calibration (Appendix A, threshold tuning).
Lookahead trial time cap C = 15 s (deployment); swept 5, 10, 20 s
Defines the bounded probe; 90% rescue rate at C=15, 0% at C=5 (Table 2).
E-match filter MLP hyperparameters (135→64→32→1, dropout 0.1)
Architecture chosen by hand; the paper argues capacity is not the limit but the choice is not optimized systematically.
Static-model features and training distributions
The four static policies are trained on different data mixes; the negative result depends on these feature sets (Appendix C).

axioms (4)

domain assumption grind's search is non-monotone
Asserted in Section 1 as 'the main complication'; the cascade's safety argument and the positive result depend on this property, but it is not formally proven.
domain assumption Proof-relevance labels from the closing proof term are a faithful supervision signal.
Appendix A defines the label; if the closing term's instance set is an artifact of grind's search order, the filter learns to replicate that order rather than to improve it.
domain assumption The forced-run oracle gives valid counterfactuals.
Section 5 and Appendix A re-run grind with each candidate forced 'with the rest of the proof fixed'; this assumes the cost of a split can be measured independently of other decisions.
ad hoc to paper The 44-theorem trace subset is representative of the general benefit.
The live cascade is evaluated only on theorems whose traces already contain a rescue decision (Section 5), so the 44/44 result is conditional on this selection.

pith-pipeline@v1.3.0-alltime-deepseek · 8497 in / 11738 out tokens · 105381 ms · 2026-08-01T03:58:52.730394+00:00 · methodology

0 comments

read the original abstract

Lean 4's grind tactic combines congruence closure, E-matching, and case-splitting into a single automated solver, and like any such solver, it relies on hand-tuned heuristics to decide what to instantiate and where to case-split. These heuristics are tempting targets for learning, but there is a catch: because grind's search is non-monotone, a learned heuristic that helps one proof can break another, and an always-on replacement usually nets out near zero. We avoid this by invoking a learned intervention only after stock grind has already failed: a failure-triggered cascade that, by construction, cannot lose a proof grind already had. We apply it to two of grind's internal decisions. A cost-aware E-matching filter solves slightly more problems and runs about 5% faster. A lookahead step proves five theorems it otherwise times out on. We also report the negative result that motivated the design: across four feature-based models, statically predicting the correct case split is no better than random, because whether a split explodes is a runtime property that the features do not capture. Our results suggest that learning within theorem-proving tactics is most effective as a mechanism for deciding when and how to spend bounded search, backed by a reliable symbolic fallback.

discussion (0)

Reference graph

Works this paper leans on

20 extracted references · 3 linked inside Pith

[1]

2024 , howpublished =

The. 2024 , howpublished =

2024
[2]

Automated Deduction (CADE-28) , series =

Moura, Leonardo, Leonardo and Ullrich, Sebastian , title =. Automated Deduction (CADE-28) , series =. 2021 , publisher =

2021
[3]

Efficient E-Matching for SMT Solvers , year =

Moura, Leonardo and Bj. Efficient E-Matching for SMT Solvers , year =. doi:10.1007/978-3-540-73595-3_13 , booktitle =

doi:10.1007/978-3-540-73595-3_13
[4]

Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , series =

Moura, Leonardo and Bj. Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , series =. 2008 , publisher =

2008
[5]

, title =

Nelson, Greg and Oppen, Derek C. , title =. Journal of the ACM , volume =
[6]

Science , volume =

Silver, David and Hubert, Thomas and Schrittwieser, Julian and Antonoglou, Ioannis and Lai, Matthew and Guez, Arthur and Lanctot, Marc and Sifre, Laurent and Kumaran, Dharshan and Graepel, Thore and Lillicrap, Timothy and Simonyan, Karen and Hassabis, Demis , title =. Science , volume =
[7]

arXiv preprint arXiv:2009.03393 , year =

Polu, Stanislas and Sutskever, Ilya , title =. arXiv preprint arXiv:2009.03393 , year =

Pith/arXiv arXiv 2009
[8]

Advances in Neural Information Processing Systems (NeurIPS) , year =

Lample, Guillaume and Lacroix, Timoth. Advances in Neural Information Processing Systems (NeurIPS) , year =
[9]

and Anandkumar, Animashree , title =

Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan J. and Anandkumar, Animashree , title =. Advances in Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track , year =
[10]

Journal of Automated Reasoning , volume =

Gauthier, Thibault and Kaliszyk, Cezary and Urban, Josef and Kumar, Ramana and Norrish, Michael , title =. Journal of Automated Reasoning , volume =
[11]

and Chollet, Fran

Alemi, Alexander A. and Chollet, Fran. Advances in Neural Information Processing Systems (NeurIPS) , year =
[12]

and Urban, Josef , title =

Blanchette, Jasmin Christian and Kaliszyk, Cezary and Paulson, Lawrence C. and Urban, Josef , title =. Journal of Formalized Reasoning , volume =
[13]

Hammer for

Czajka,. Hammer for. Journal of Automated Reasoning , volume =
[14]

Gordon and J

Stephane Ross and Geoffrey J. Gordon and J. Andrew Bagnell , year=. A Reduction of. 1011.0686 , archivePrefix=

Pith/arXiv arXiv
[15]

Learning a

Selsam, Daniel and Lamm, Matthew and B. Learning a. International Conference on Learning Representations (ICLR) , year =
[16]

Advances in Neural Information Processing Systems (NeurIPS) , year =

Kurin, Vitaly and Godil, Saad and Whiteson, Shimon and Catanzaro, Bryan , title =. Advances in Neural Information Processing Systems (NeurIPS) , year =
[17]

Learning to Solve

Balunovi. Learning to Solve. Advances in Neural Information Processing Systems (NeurIPS) , year =
[18]

CoRR , volume =

Max Willsey and Yisu Remy Wang and Oliver Flatt and Chandrakana Nandi and Pavel Panchekha and Zachary Tatlock , title =. CoRR , volume =. 2020 , url =. 2004.03082 , timestamp =

Pith/arXiv arXiv 2020
[19]

and Leyton-Brown, Kevin , title =

Xu, Lin and Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin , title =. Journal of Artificial Intelligence Research (JAIR) , volume =
[20]

Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD) , pages =

Chen, Tianqi and Guestrin, Carlos , title =. Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD) , pages =

[1] [1]

2024 , howpublished =

The. 2024 , howpublished =

2024

[2] [2]

Automated Deduction (CADE-28) , series =

Moura, Leonardo, Leonardo and Ullrich, Sebastian , title =. Automated Deduction (CADE-28) , series =. 2021 , publisher =

2021

[3] [3]

Efficient E-Matching for SMT Solvers , year =

Moura, Leonardo and Bj. Efficient E-Matching for SMT Solvers , year =. doi:10.1007/978-3-540-73595-3_13 , booktitle =

doi:10.1007/978-3-540-73595-3_13

[4] [4]

Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , series =

Moura, Leonardo and Bj. Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , series =. 2008 , publisher =

2008

[5] [5]

, title =

Nelson, Greg and Oppen, Derek C. , title =. Journal of the ACM , volume =

[6] [6]

Science , volume =

Silver, David and Hubert, Thomas and Schrittwieser, Julian and Antonoglou, Ioannis and Lai, Matthew and Guez, Arthur and Lanctot, Marc and Sifre, Laurent and Kumaran, Dharshan and Graepel, Thore and Lillicrap, Timothy and Simonyan, Karen and Hassabis, Demis , title =. Science , volume =

[7] [7]

arXiv preprint arXiv:2009.03393 , year =

Polu, Stanislas and Sutskever, Ilya , title =. arXiv preprint arXiv:2009.03393 , year =

Pith/arXiv arXiv 2009

[8] [8]

Advances in Neural Information Processing Systems (NeurIPS) , year =

Lample, Guillaume and Lacroix, Timoth. Advances in Neural Information Processing Systems (NeurIPS) , year =

[9] [9]

and Anandkumar, Animashree , title =

Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan J. and Anandkumar, Animashree , title =. Advances in Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track , year =

[10] [10]

Journal of Automated Reasoning , volume =

Gauthier, Thibault and Kaliszyk, Cezary and Urban, Josef and Kumar, Ramana and Norrish, Michael , title =. Journal of Automated Reasoning , volume =

[11] [11]

and Chollet, Fran

Alemi, Alexander A. and Chollet, Fran. Advances in Neural Information Processing Systems (NeurIPS) , year =

[12] [12]

and Urban, Josef , title =

Blanchette, Jasmin Christian and Kaliszyk, Cezary and Paulson, Lawrence C. and Urban, Josef , title =. Journal of Formalized Reasoning , volume =

[13] [13]

Hammer for

Czajka,. Hammer for. Journal of Automated Reasoning , volume =

[14] [14]

Gordon and J

Stephane Ross and Geoffrey J. Gordon and J. Andrew Bagnell , year=. A Reduction of. 1011.0686 , archivePrefix=

Pith/arXiv arXiv

[15] [15]

Learning a

Selsam, Daniel and Lamm, Matthew and B. Learning a. International Conference on Learning Representations (ICLR) , year =

[16] [16]

Advances in Neural Information Processing Systems (NeurIPS) , year =

Kurin, Vitaly and Godil, Saad and Whiteson, Shimon and Catanzaro, Bryan , title =. Advances in Neural Information Processing Systems (NeurIPS) , year =

[17] [17]

Learning to Solve

Balunovi. Learning to Solve. Advances in Neural Information Processing Systems (NeurIPS) , year =

[18] [18]

CoRR , volume =

Max Willsey and Yisu Remy Wang and Oliver Flatt and Chandrakana Nandi and Pavel Panchekha and Zachary Tatlock , title =. CoRR , volume =. 2020 , url =. 2004.03082 , timestamp =

Pith/arXiv arXiv 2020

[19] [19]

and Leyton-Brown, Kevin , title =

Xu, Lin and Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin , title =. Journal of Artificial Intelligence Research (JAIR) , volume =

[20] [20]

Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD) , pages =

Chen, Tianqi and Guestrin, Carlos , title =. Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD) , pages =