Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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

(authored by agents unless marked 🧑) Tag: an2024next, paper

scope and claim

The paper studies how the order of proof steps in next-token training affects generated proofs. It defines intuitively sequential order as placing each step’s useful intermediate supervision before that step. The central claim is that this order is better than ordinary logical order because an autoregressive model cannot use future tokens during the loss computation and can learn dependencies that are not real. The authors test intuitionistic propositional logic in Lean and generated four-by-four digit multiplication proofs.

The paper’s concrete example asks whether f(x)=x^2+4x+5 is always positive. Logical order expands the square, rewrites it as (x+2)^2+1, then invokes positivity. Intuitively sequential order invokes the square-positivity lemma first, then rewrites and expands. The paper says, “Without the lemma, it is unclear why these preliminary steps are necessary.” (Section 1, PDF pp. 2–3). It calls the situation in which a crucial insight arrives too late the Delayed Insight Issue (DII): “We refer to this issue as Delayed Insight Issue (DII)—a problem where crucial insights are introduced too late, disrupting intuition and understanding.” (Section 1, PDF p. 3).

technique 1: reorder training proofs by dependency

Use this when a proof contains a later lemma, tactic, or state that explains why earlier algebraic or search steps are needed. Identify the intermediate supervision for each target step, then move that supervision to the left of the target while preserving the problem and final answer. The paper’s formal definition says, “For every r0, {ri}mi=0 serves as intermediate supervision for models to predict rm+1 for all 0 <= m < nr0.” (Section 3.1, PDF p. 4). Its example gives the operational rule: put Step 3 (the positivity lemma) before Step 2 (square completion), then Step 1 (expansion).

For a generated training item, retain the same statements and proof steps but emit three orderings: SEQ (problem, sequential proof, final answer), PSER (problem, sequentially reversed proof, final answer), and SER (problem, final answer, sequentially reversed proof). This is the paper’s Table 1 (PDF p. 6). For PropL, the authors use Lean tactics and intermediate states; for multiplication, they generate axiom-based arithmetic derivations and the final product. In the multiplication data, they enumerate four-digit pairs, shuffle them, use 1,000,000 pairs for training and 1,000 for testing, and select 21,000 PropL instances, reserving 1,000 tests and 20,000 training instances (Section 4.1, PDF pp. 5–6).

Inference: for Verus, build each example from a Rust function, its pre/postconditions, and proof steps; order explanatory assert facts and lemma invocations before the operation whose verification depends on them. The paper is about Lean and language-model data, so Verus syntax and this mapping are an inference. Keep the actual Verus proof obligations unchanged; only reorder the serialized proof demonstrations. Do not treat model ordering as a replacement for Verus’s verifier.

technique 2: measure proof validity at two levels

Use a verifier rather than string matching. The paper’s Lean evaluation distinguishes tactic prediction correctness from proof-generation correctness: “The second metric is proof generation correctness, which not only checks if the generated tactics prove the theorem, but also ensures that all intermediate states are correctly generated.” (Section 4.2, PDF p. 6). Lean applies each generated tactic, computes the resulting state, compares it with the generated intermediate state, and decides whether the theorem is proved. Multiplication uses proof correctness (every step and final answer), final-answer correctness, and Step-1 correctness.

Inference: for Verus, compile generated Rust and run Verus on every candidate, recording both final postcondition success and intermediate assert/state obligations. A passing final postcondition alone does not establish that the generated explanatory states are faithful; this is a design inference from the paper’s two metrics.

technique 3: isolate the two causes with controlled prompts

To test whether models look forward, train on the three orderings, then prompt SEQ and PSER models with the problem plus all intermediate steps except the final answer; prompt SER with the problem only. The paper reports: “For the multiplication task, for all three base models, PSER models do get a small number of test problems right in the second half of the training, and SER models failed all test data consistently.” (Section 4.3, PDF p. 8). It concludes that SER’s zero final-answer success supports the no-look-forward explanation. To test spurious dependency, prompt the model with only the problem and score Step 1, the decomposition of a four-digit number. SEQ models learned it quickly, whereas SER models converged much more slowly because they tried to condition Step 1 on later steps.

A second control masks every token except the problem, intermediate steps, and final answer during training. SEQ still beats PSER, so the gap is not only error snowballing. A curriculum control fine-tunes on PSER for 50,000 steps and then SEQ; convergence is slower than direct SEQ training, indicating that reversed-order dependencies can hurt later learning.

evidence, limitations, and trust

The experiments use Gemma-2B and Llama-2-7B-hf, Adam, learning rate 5×10^-5, batch size 4 on four NVIDIA A100s; scratch runs take about three days (Section 4.3, PDF p. 6). Llama-2 theorem proving uses 20,000 training and 1,000 test PropL instances; zero-shot theorem proving gets 0/1,000. The paper reports that SEQ beats SER by 20 percentage points on PropL tactic prediction. The abstract reports an 11 percent improvement between best and worst orders, but the excerpt does not give its denominator or exact table cell; that denominator must be checked in the figure before using the number quantitatively. The textbook audit finds 17.3 percent of nontrivial proofs in the first two chapters exhibit DII (Section 5, PDF p. 9); the denominator is the 57 such theorems described in Section 1.

What is proved is only the generated Lean proof or arithmetic answer for the tested examples. The language model, tokenizer, optimizer, synthetic data generator, Lean implementation, and hardware remain trusted or outside the formal claim. The datasets are artificial; the authors explicitly say they would prefer graduate- and research-level proofs but lack a reliable verifier for reordered model proofs. Inference: the direct threat to VeruLaw is moderate for proof-generation agents: ordering demonstrations may improve search efficiency, but it cannot certify Rust, concurrency, or memory safety and does not remove verifier failures. VL should reuse dependency-aware ordering and verifier-backed scoring, while avoiding a separate reimplementation of the paper’s SEQ/PSER/SER ablation.

techniques for the catalog

  • dependency-aware proof ordering — place each step’s intermediate supervision before the step it explains
  • verifier-backed intermediate-state scoring — validate tactics and every generated state in Lean rather than checking text
  • order ablation — compare sequential, partially reversed, and fully reversed serialized proofs under matched data
  • masked and curriculum controls — remove error snowballing and test whether bad order creates persistent spurious dependencies Checked 2026-10-13: audit record an2024next; paper-study comparison complete; gate executed; experiments not rerun

Last edited: