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

arXiv: https://arxiv.org/abs/2610.12168 · HTML: https://mlsanity.com/paper/2610.12168/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Prompting and chain-of-thought reasoning, one of 17 directions in LLM reasoning.
- Builds on 5 of its 30 references that are in the map.
- First posted on arXiv 8 Oct 2026.

## Placed in

- LLM reasoning / [Prompting and chain-of-thought reasoning](https://mlsanity.com/lr/prompting-and-chain-of-thought-reasoning/)

## Builds on (most cited first, 5 of 5)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Learning to Reason with Insight for Informal Theorem Proving](https://mlsanity.com/paper/2604.16278/) (2026)

## Abstract (arXiv)

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.