# Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 36 references that are in the map.
- First posted on arXiv 30 Oct 2024.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Lost in the Middle: How Language Models Use Long Contexts](https://mlsanity.com/paper/2307.03172/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The Reversal Curse: LLMs trained on "A is B" fail to learn "B is A"](https://mlsanity.com/paper/2309.12288/) (2023)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Solving Challenging Math Word Problems Using GPT-4 Code Interpreter with Code-based Self-Verification](https://mlsanity.com/paper/2308.07921/) (2023)
- [The pitfalls of next-token prediction](https://mlsanity.com/paper/2403.06963/) (2024)
- [OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text](https://mlsanity.com/paper/2310.06786/) (2023)
- [Goat: Fine-tuned LLaMA Outperforms GPT-4 on Arithmetic Tasks](https://mlsanity.com/paper/2305.14201/) (2023)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Auto-Regressive Next-Token Predictors are Universal Learners](https://mlsanity.com/paper/2309.06979/) (2023)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Reverse Training to Nurse the Reversal Curse](https://mlsanity.com/paper/2403.13799/) (2024)
- [Sub-Task Decomposition Enables Learning in Sequence to Sequence Tasks](https://mlsanity.com/paper/2204.02892/) (2022)
- [An Independent Evaluation of ChatGPT on Mathematical Word Problems (MWP)](https://mlsanity.com/paper/2302.13814/) (2023)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [Unraveling the Mystery of Scaling Laws: Part I](https://mlsanity.com/paper/2403.06563/) (2024)
- [Benchmarking the Capabilities of Large Language Models in Transportation System Engineering: Accuracy, Consistency, and Reasoning Behaviors](https://mlsanity.com/paper/2408.08302/) (2024)
- [Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving](https://mlsanity.com/paper/2404.07382/) (2024)

## Built on by (most cited first, 2 of 2)

- [QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems](https://mlsanity.com/paper/2604.24021/) (2026)
- [Language Models, Graph Searching, and Supervision Adulteration: When More Supervision is Less and How to Make More More](https://mlsanity.com/paper/2503.10542/) (2025)

## Abstract (arXiv)

In the field of large language model (LLM)-based proof generation, despite extensive training on large datasets such as ArXiv, LLMs still exhibit only modest performance on proving tasks of moderate difficulty. We believe that this is partly due to the widespread presence of suboptimal ordering within the data for each proof used in training. For example, published proofs often follow a purely logical order, where each step logically proceeds from the previous steps based on the deductive rules. This order is designed to facilitate the verification of the proof's soundness, rather than to help people and models learn the discovery process of the proof. In proof generation, we argue that the optimal order for one training data sample occurs when the relevant intermediate supervision for a particular proof step in the proof is always positioned to the left of that proof step. We call such order the intuitively sequential order. We validate our claims using two tasks: intuitionistic propositional logic theorem-proving and digit multiplication. Our experiments verify the order effect and provide support for our explanations. We demonstrate that training is most effective when the proof is in the intuitively sequential order. Moreover, the order effect and the performance gap between models trained on different data orders can be substantial -- with an 11 percent improvement in proof success rate observed in the propositional logic theorem-proving task, between models trained on the optimal order compared to the worst order. Lastly, we define a common type of order issue in advanced math proofs and find that 17.3 percent of theorems with nontrivial proofs in the first two chapters of a widely used graduate-level mathematics textbook suffer from this issue. A detailed list of those proofs is provided in the appendix.