Learning to Plan by Looking Back: Hindsight Hierarchies for Training Reasoning Models

1 Introduction

• Reverse-engineering an idea from a known solution is generally easier than solving from scratch, so even a problem beyond current solving ability may yield a useful idea when its solution is supplied.The reconstructed idea can supervise learning to develop an idea from the problem alone.Source: §1 · p. 1
• Each iteration reconstructs ideas from problems and known solutions, then jointly trains the foresight, hindsight, and solver components on the resulting data.The foresight component predicts ideas from problems, hindsight reconstructs them from problems and solutions, and the solver uses ideas to construct solutions.Source: §1 · p. 1
• Ideas form a hierarchy from overarching strategies to detailed plans: hindsight moves from solutions toward coarser ideas, while foresight predicts a coarse idea and progressively refines it.At inference, the solver uses the foresight-predicted hierarchy to construct a solution candidate.Source: §1 · p. 1
• The hindsight ideas are intended to guide solutions from the problem alone rather than merely describe the supplied solution or reflect hindsight bias.The Lean instantiation seeks to mitigate hindsight bias through prompt-template instructions.Source: §1 · pp. 1–2
• The hindsight component is trained on its own outputs, a possible weakness that the paper optionally addresses by selecting hierarchies through repeated solver attempts in verifiable domains.Selection scores hierarchies by solver success and optionally domain-specific quantities, retaining the highest-scoring one if it meets a threshold.Source: §1 · p. 2
• The paper formally specifies the general method and an optional verifier-based refinement, and instantiates it for Lean theorem proving, where natural-language ideas guide tactic generation.The manuscript reports no empirical evaluation and leaves it for future work.Source: §1 · p. 2

2 Related work

• Prior work includes language-model-guided theorem proving, premise retrieval, automated prover integration, and synthetic proof data and proof-feedback reinforcement learning.The Lean instantiation conditions tactic generation on learned hierarchies of proof ideas.Source: §2 · p. 2
• Planning research uses intermediate steps, subproblems, and tree search, while theorem-proving approaches use proof skeletons, lemmas, and subgoals.The paper’s hierarchies are intended to describe solution ideas at different levels of granularity.Source: §2 · p. 2
• Related self-training includes expert iteration, learning from selected generated solutions, proof-search training, self-play, and correctness-estimator-guided selection.These methods provide context for the paper’s verifier-guided assessment of reverse-engineered hierarchies.Source: §2 · pp. 2–3
• Retrospective rationale work includes STaR, on-policy self-distillation, Lean-STaR, and DeepInsight.These systems respectively use answer-hinted rationales, reference-conditioned distillation, retrospective proof-state thoughts, or externally extracted techniques and proof sketches.Source: §2 · p. 3
• Unlike prior retrospective-rationale approaches, the method explicitly trains hierarchy generation and repeatedly uses the same backbone to generate, predict, and apply those hierarchies.The paper contrasts this with Lean-STaR’s forward generation of thoughts and tactics and DeepInsight’s retrospective generation using a teacher model.Source: §2 · p. 3
• In verifiable domains, separate solving attempts assess reverse-engineered hierarchies without the reference solution, and the assessment guides training-triple selection in the spirit of expert iteration.The reference solution is withheld during those attempts.Source: §2 · p. 3

3 Problem setting

• The general problem is to find a candidate solution y for an instance x such that (x, y) belongs to the validity relation R.Training uses supplied reference pairs, ideally valid, although imperfect references can be used without a verifier and their quality then depends on the data source.Source: §3 · p. 3

3.1 Verifiable problem domains

• A verifiable domain provides a deterministic procedure that terminates on considered inputs and returns 1 exactly for valid problem–solution pairs.This permits repeated verification queries during the algorithm.Source: §3.1 · p. 3
• For interactive theorem proving, tactics transition between proof states; a tactic sequence succeeds when it reaches the no-open-goals state, while errors lead to failure.The tactic set excludes tactics that admit unproved obligations or introduce disallowed axioms, including sorry and admit in Lean.Source: §3.1 · pp. 3–4

4.1 Hierarchies

• Hierarchies range from detailed solution sketches to coarse overarching ideas, with how levels are chosen and encouraged depending on the problem domain.Hindsight reconstructs from fine to coarse, while foresight predicts from coarse to fine.Source: §4.1 · p. 4, §4.2 · p. 4

4.2 System components

• The solver uses a foresight-predicted hierarchy to produce a solution candidate; hindsight reconstructs hierarchies from problems and known solutions, while foresight predicts them from problems alone.All three components share a backbone, and their predictions are conditioned on the problem.Source: §4.2 · pp. 4–5

4.3 Ingredients for training the system

• Training uses seed triples, additional problem-solution pairs, a procedure for constructing triples in hindsight, and a training operator that supervises all three components.The training objective encourages the solver to predict solutions and the foresight and hindsight components to predict hierarchies.Source: §4.3 · pp. 5–6

4.4 The full training loop

• After initial seed-data training, each iteration constructs triples from a batch, combines new and replayed data, and updates the parameters.Parameters remain fixed while triples are constructed for the batch.Source: §4.4 · p. 6

4.5 ConstructTriple in the general problem setting: direct augmentation with hindsight hierarchies

• In the general setting, direct augmentation adds a hierarchy sampled by the current hindsight component to a supplied problem-solution pair.This option can also be used in verifiable domains when verifier-guided selection is not desired.Source: §4.5 · p. 7

4.6 ConstructTriple in verifiable problem domains: verifier-guided selection of hindsight hierarchies

• For verifiable problems, the method samples candidate hindsight hierarchies, scores them using estimated usefulness and a granularity penalty, and selects the highest-scoring candidate if it meets a threshold.The assessment can retain a valid solution found by the solver; if none is found, it retains the supplied reference solution.Source: §4.6 · pp. 7–8

5.1 Lean instantiation: hierarchies and data

• The Lean hierarchy uses strings at successive granularities; the prompts use a detailed plan and coarse proof idea, neither of which must be executable Lean commands.A teacher language model generates seed hierarchies from verified problem-solution pairs, but is not used in the subsequent training loop; additional verified pairs may come from external data or synthetic generation.Source: §5.1 · p. 9

5.2 Lean instantiation: system components

• The shared language model implements foresight and hindsight through iterative hierarchy refinement or compression, while the solver uses best-first proof search with the model as a tactic oracle.The hierarchy and initial proof state remain fixed and are included in prompts throughout the search; the solver may depart from guidance when it does not fit.Source: §5.2 · pp. 9–10
• Inference predicts a hierarchy from the initial proof state, then runs the solver with that hierarchy; failed attempts may be followed by arms using newly sampled hierarchies and fresh search graphs.Inference stops at the first valid solution or signals failure after all arms are exhausted.Source: §5.2 · p. 10

5.3 Lean instantiation: ConstructTriple

• For each candidate hindsight hierarchy, the joint procedure runs the solver repeatedly, estimates usefulness from the success ratio and average proof length, and retains the shortest discovered proof.If all runs fail, usefulness is zero and the reference solution is the fallback; the positive acceptance threshold prevents that candidate from producing a returned triple.Source: §5.3 · pp. 10–11
• A verifier-guided procedure retains a training triple only when its hierarchy meets a positive score threshold, so every returned triple has a solver-discovered valid solution.The score combines usefulness with a penalty encouraging compression between hierarchy levels; compression alone does not ensure semantic meaning.Source: §5.3 · p. 11

5.4 Lean instantiation: training operator Train

• Each verified training triple supplies prompt-response pairs for foresight, hindsight, and solver tasks, including predictions at each hierarchy level and tactic generation from proof states.The pair counts are n + 1 for each of foresight and hindsight, and k for the solver when the solution has k tactics.Source: §5.4 · pp. 11–12
• Training uses normalized next-token loss and mini-batches with prescribed contributions from solver, foresight, and hindsight groups.The loss is normalized by response length because hierarchy descriptions can be substantially longer than individual Lean tactics.Source: §5.4 · p. 12

From hindsight to foresight

• The method hypothesizes that reverse-engineering ideas from known solutions is generally easier than discovering them from problems alone, but whether those ideas suit foresight prediction remains uncertain.Prompt instructions seek to mitigate hindsight bias, and the authors call for thorough experimental evaluation.Source: §6 · p. 12

The case of verifiable problem domains

• For verifiable domains, the procedure can score several hindsight-generated ideas by solving with them and checking proposed solutions, then retain the highest-scoring idea if it meets a threshold.A high score does not establish that the idea helped solve the problem, since the model might ignore it and solve from the problem alone.Source: §6 · p. 13

Future empirical validation

• The proposed method has no reported empirical validation; future evaluation should cover Lean and non-verifier settings, comparable-budget supervised fine-tuning, and ablations.Ablations should assess whether score-based selection of hindsight-generated ideas improves performance.Source: §6 · p. 13

Use of AI tools

• AI tools assisted with prose, literature work, figures, typesetting, and implementation and testing; the human authors retain responsibility for the manuscript’s scientific and mathematical content.The version reports no empirical evaluation.Source: Use of AI tools · p. 13

A Appendix

• The appendix supplies implementation details for the proposed method’s Lean instantiation.Source: A Appendix · p. 15

• The shared model is internlm/internlm2-math-plus-7b, with weights and tokenizer revision 2565e424cc6f83358e7a5aa19b639205fcdd173d.Source: §A.1 · p. 15
• The theorem-proving environment is Lean 4.10.0 with LeanDojo 2.1.3; inference uses bfloat16 context and an 8192-token limit.Runtime: Python 3.11.9 on x86_64 Linux; reference packages are vLLM 0.4.1, PyTorch 2.2.1, and Transformers 4.40.1.Source: §A.1 · p. 15
• All trainable parameters are shared across components, which are distinguished by their prompts.Source: §A.1 · p. 15

A.2 Data

• The extracted mathlib theorems [30] are partitioned following LeanDojo, with 2,000 theorems each reserved for validation and testing.The random split uses seed 3407; only the training partition supplies seed data and subsequent batches.Source: §A.2 · p. 15
• From the training partition, 50,523 complete tactic-proof pairs are retained after excluding proofs with missing tactics and verifying execution in Lean.The retained proofs close all goals and reproduce the dataset's recorded proof states.Source: §A.2 · p. 15
• The 50,523 training pairs are permuted with seed 20260523; the first 15,000 seed hierarchy generation and the remaining 35,523 are reserved for later batches.Both subsets are used for training, not evaluation.Source: §A.2 · p. 15
• A teacher language model receives each seed example’s initial state, complete tactic sequence, and theorem metadata, then supplies a detailed plan and coarse idea.Intermediate states are excluded, and an anti-hindsight-bias check is also requested; later training hierarchies come only from the current hindsight component.Source: §A.2 · p. 15
• The reserved pool is processed in successive batches of up to 2,048 entries, followed by at most two retry passes for failed triple construction.This policy uses neither synthetic data nor difficulty groups.Source: §A.2 · p. 15

A.3 Role-specific prompt templates

• For n = 1, the hierarchy has a DETAILED PLAN z0 and a COARSE IDEA z1, with one hierarchy level produced per shared-model foresight or hindsight call.The teacher produces both levels in one response.Source: §A.3 · p. 15
• The coarse idea must be a single, abstract, reusable sentence shorter than the detailed plan.Source: §A.3 · p. 16
• Foresight predicts a coarse idea from the initial state, then refines it into a detailed plan using the initial state and preceding idea.Both prompts request only the proof idea, without extra commentary.Source: §A.3 · p. 17
• The hindsight prompt infers a detailed idea from the initial state and verified tactics, while explicitly requiring guidance plausible from the original state.It warns against tactic-by-tactic replay and reliance on information visible only after later tactics.Source: §A.3 · pp. 16–17
• The solver receives the initial state, hierarchy, and current state, and may treat the ideas as incomplete or partly wrong while choosing a tactic for the current state.Only the current state changes during search; the initial state and hierarchy remain fixed.Source: §A.3 · p. 18
• The optional null arm omits foresight and supplies “No proof idea provided” in both hierarchy fields to the solver.Source: §A.3 · pp. 18–19

A.4 Best-first proof search configuration

• Each tactic-search attempt allows 100 node expansions, depth 100, 32 tactics per expanded state, and a nominal 600-second budget.LeanDojo tactic timeouts are 300 seconds; decoding uses deterministic beam search with 32 responses and at most 256 new tokens each.Source: §A.4 · p. 19
• New proof-graph nodes receive a priority based on the tactic path used to reach them, with each generated response’s token count and conditional log probabilities defined for scoring.The root priority is zero.Source: §A.4 · p. 19
• Search expands the highest-priority unexpanded node, executes candidate tactics in decreasing step-score order, reuses previously seen states, and returns failure when no nodes remain or the overall budget expires.A tactic timeout counts as failure; a completing tactic ends the attempt immediately.Source: §A.4 · p. 19

A.5 Inference: multiple arms

• Inference uses two hierarchy-conditioned arms, each generating a hierarchy before calling the solver with the full budget; the shared model stays fixed and stops at the first valid solution.An optional null arm skips hierarchy generation and uses the same solver budget and proof-search configuration.Source: §A.5 · p. 20

A.6 Hierarchy selection and iteration settings

• Four hindsight hierarchies per pair are each assessed with one solver run under the same limited search settings, which are smaller than inference budgets.The proposed settings are a starting point and have not been selected through empirical comparison.Source: §A.6 · p. 20
• Failed pairs are retried in order, accepted triples leave permanently, and processing stops when retries empty, a pass accepts none, or three passes finish.The initial pass uses 17 batches of 2,048 entries and one of 707; retry passes use at most 18 batches.Source: §A.6 · p. 20

A.7 Replay policy

• Each nonempty training batch combines all accepted new triples with an equal number sampled uniformly without replacement from earlier triples.The history retains at least 15,000 seed triples, while each batch has at most 2,048 new triples; an empty batch leaves parameters unchanged.Source: §A.7 · p. 20

A.8 Implementation details for Train

• Training uses bS = 8 and bF = bH = 2, AdamW, and peak learning rates of 5 · 10^-6 for seed training and 10^-6 thereafter.Prompts and responses must fit the 8,192-token context limit; no truncation is applied. The proposed training settings remain to be evaluated empirically.Source: §A.8 · p. 21