Learning to Plan by Looking Back: Hindsight Hierarchies for Training Reasoning Models
Lars Simon, Holger Eble, Manuel Radons
cs.AI
Oct 8, 2026 · v1
cs.LG cs.LO
TL;DR
Proposes a self-improvement training loop for LLM provers with a concrete Lean instantiation using tactic-level proof search guided by natural-language proof-idea hierarchies.
Abstract
We introduce a self-improvement loop for reasoning models based on the following observation: Even when the difficulty of a problem exceeds the model's current solving abilities, an additionally supplied solution might enable the model to extract useful solution ideas in hindsight. We operationalize this by jointly training the same model to exhibit the following three capabilities: predicting solution ideas from problems alone, reverse-engineering ideas from problems and known solutions, and solving problems using provided ideas. The loop alternates between reverse engineering such ideas from problems with supplied solutions and using these ideas as additional supervision for joint training of all three capabilities. We give a formal specification of our method and a concrete instantiation for interactive theorem proving in the Lean theorem prover; empirical evaluation remains future work.
Problem
Reasoning models struggle to learn from problems beyond their current solving ability. Even so, a supplied solution may let a model reconstruct the underlying solution idea in hindsight.
Approach
A single shared language model is jointly trained in three roles. Foresight predicts solution ideas from a problem alone, hindsight reverse-engineers ideas from a problem plus its known solution, and the solver solves problems from the provided ideas. Training alternates between generating hindsight idea hierarchies and joint training on the resulting triples. A verifier-guided variant scores candidate hierarchies by solver utility minus a length penalty. In the Lean instantiation, proof states are the problems and tactic sequences are the solutions, and two-level natural-language hierarchies (a detailed plan and a coarse idea) condition tactic generation during proof search.
Results
The paper gives a formal specification of the method and a concrete Lean instantiation with implementation details. It reports no empirical evaluation; that is left to future work.
