A Theory for Worst-Case vs. Average-Case Guarantees for LLMs

We thank the reviewer for their constructive feedback and thoughtful suggestions. We address each point below:

Regarding Remark 2.5: Thank you. Indeed, the remark can also be formally proven in the way you are suggesting (by decomposing into the two disjoint events, rather than the union bound). We will update the wording in the remark.

Regarding verifier instantiation and empirical demonstration: We appreciate the reviewer's suggestion to demonstrate our approach in a simplified, arithmetic setting. We have added comprehensive experiments using GCD computation as our constrained problem space, with a verifier based on Bézout's theorem: for claimed GCD $g$ of integers $x_1$ and $x_2$, the model provides coefficients $a,b$ such that $ax_1 + bx_2 = g$; the verifier then checks that $g$ divides both $x_1$ and $x_2$, and that $g=ax_1 + bx_2$ (this confirms that $g$ is the GCD, with certainty). This arithmetic setting provides the "simplified setting" the reviewer suggested while demonstrating practical instantiation of our framework. Next are the full experimental details below, which we will include in the camera-ready version.

Experiment details: We have conducted experiments demonstrating that our framework can be practically instantiated. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations on pairs of integers up to $10^4$, following Charton's [1] setup.

Key results:

• Transcript Learning (TL): Achieved 60.3% verifiability (correctly proving answers) after training for 100k steps.
• RLVF: Improved a base model with 40% verifiability to 79.3%, albeit in significantly more (4M) iterations; while this is not an experimental paper, we will continue to explore a practical speedup by searching the hyperparameter space.
• TL + Annotations: Reached 96% verifiability by training on proofs annotated with intermediate Euclidean algorithm steps (similar to chain-of-thought); importantly, evaluation uses only the final proof.

Our proof system relies on Bézout's theorem. Given inputs $x_1$ and $x_2$, to claim that $g = GCD(x_1,x_2)$, the model must output coefficients $a,b$. The verifier then checks that $g$ divides both $x_1$ and $x_2$, and that $g = a x_1 + b x_2$.

Ablations show that (1) more annotation steps improve verifiability monotonically, (2) even when trained with annotations, the model generalizes beyond the amount of annotations (i.e., it is not just memorizing the chain-of-thought, but exhibits length generalization), and (3) bases with more prime factors improve both correctness and verifiability—in line with Charton's findings.

[1] Francois Charton. Learning the greatest common divisor: explaining transformer predictions. ICLR 2024.

Thank you for your thoughtful review and for recognizing our framework as interesting and theoretically sound. We appreciate your acknowledgment of our well-presented theorems, thorough motivation, and novel ideas. Your questions about practical applicability and foundational limits are insightful and help clarify important aspects of our work.

Regarding concerns

Whilst theoretically solid, the practical implications of this work I feel would be limited. For example, considering the related area of models that prove general formal theorems. This is notoriously hard, and it seems unlikely that one could train a model with practical confidence parameters in any non-trivially applicable scenario.”

We share your view that general theorem proving is notoriously difficult. However, our framework applies to a much broader class of problems than just "trivial" mathematics. Many computational tasks admit efficient interactive proofs while remaining tractable—from arithmetic operations to graph properties to optimization problems. To demonstrate practical instantiation, we have conducted experiments on GCD computation with Bézout coefficient proofs. Our 6.3M parameter transformers achieved 60.3% verifiability with basic Transcript Learning, 79.3% with RLVF, and 96% with annotated training. While GCD is admittedly simpler than general theorem proving, it demonstrates that self-proving models can be trained effectively for non-trivial mathematical tasks. This provides a foundation for exploring more complex applications in future work. We will include analysis (with figures) in the camera-ready version and release the model and code publicly. We note that the code is generic, so that larger transformers can be trained for more involved proof systems by those who have the computational resources.

Regarding questions

Gödel's incompleteness: Not at all naive, this question is an important one to ask in the context of any Proof system! Informally speaking, you are right to say that there is no single Interactive Proof system that is complete with respect to “all True statements.” Instead, one should think about specific problems (i.e., specific notions of True statements) for which there is an IP system. Then, our theory studies whether it is possible to learn an approximately-honest Prover. Indeed, there are problems for which an IP system cannot exist; but on the other hand, there is an extremely rich family of problems (anything solvable in polynomial space) for which an IP system does exist (as shown by Shamir 1992).

"Honest" terminology: Thank you for pointing out this potential confusion. We've clarified the definition to make it clearer that we're defining what "honest" means. We now write: "If there exists a prover P* such that [conditions]... Such a prover is called an honest prover." This should make it evident that "honest" is the term being defined, not a redundant qualifier.

Experiment details: We have conducted experiments demonstrating that our framework can be practically instantiated. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations on pairs of integers up to 10^4, following Charton's [1] setup.

Key results:

• Transcript Learning (TL): Achieved 60.3% verifiability (correctly proving answers) after training for 100k steps.
• RLVF: Improved a base model with 40% verifiability to 79.3%, albeit in significantly more (4M) iterations; while this is not an experimental paper, we will continue to explore a practical speedup by searching the hyperparameter space.
• TL + Annotations: Reached 96% verifiability by training on proofs annotated with intermediate Euclidean algorithm steps (similar to chain-of-thought); importantly, evaluation uses only the final proof.

Our proof system uses Bézout's theorem: the model must output coefficients a,b such that $a x_1 + b x_2 = GCD(x_1, x_2)$, which the verifier can use to easily check (with certainty) that the model's output is indeed the GCD.

More nuanced results show (1) more annotation steps improve verifiability monotonically, (2) even when trained with annotations, the model generalizes beyond the amount of annotations (i.e., it is not just memorizing the chain-of-thought, but exhibits length generalization), and (3) bases with more prime factors improve both correctness and verifiability—in line with Charton's findings.

While GCD is simpler than general theorem proving, it provides a concrete proof-of-concept that self-proving models can be trained in practice. We are happy to provide full experimental details and will include them in the camera-ready version.

[1] Francois Charton. Learning the greatest common divisor: explaining transformer predictions. ICLR 2024.

The GCD is the only common divisor of $x_1$ and $x_2$ that satisfies Bezout's identity. So, for inputs $x_1$ and $x_2$, the prover sends $a, b, c$ as you correctly said. The verifier then checks that $c$ divides both $x_1$ and $x_2$, and that Bezout's identity is satisfied.

Thank you for requesting this clarification; this important detail will be made clear in the full write-up.

Thank you for your review and for acknowledging that our paper addresses an interesting challenge regarding worst-case guarantees of probabilistic models. We appreciate your detailed feedback and address each of your concerns below.

Regarding abstraction and PSPACE-completeness: As the reviewer notes, IPs can be used to prove PSPACE-complete problems. However, this does not preclude designing very efficient IPs for tractable computational problems or classes of computations. Moreover, even if a problem is intractable in the worst case, this does not preclude constructing efficient honest provers that perform well on real-world inputs (i.e. convince the verifier on average-case inputs). In terms of theoretical insights, the literature on IPs has produced a treasure trove of such insights (e.g. the literature on ZK proofs and doubly-efficient proof systems), even though the same objection (that IPs include PSPACE complete problems) could be raised there. This is the case even though the focus there is on worst-case guarantees (for the honest prover), let alone in the ML setting where we focus on average-case guarantees (for the honest prover).

Regarding empirical evaluation: We have conducted comprehensive experiments demonstrating practical instantiation. We trained 6.3M parameter transformers to compute and prove GCD correctness using Bézout certificates. Results: Transcript Learning achieved 60.3% verifiability, RLVF improved models from 40% to 79.3%, and Annotated TL reached 96% verifiability. Crucially, models generalize beyond their training—proving GCDs that require more steps than seen during training. These experiments validate that our algorithms produce non-trivial learning behavior in practice. We provide additional experimental details following the rebuttal.

Theorem 4.1 relies on strong and arguably unrealistic assumptions.

While autoregressive neural networks have non-convex loss landscapes, analyzing convex settings remains valuable in ML theory. Convex analysis provides clean mathematical tools for building intuition and establishing foundational results—a standard approach in theoretical ML. Proving convergence without convexity is the subject of cutting-edge research. Following common practice, we prove results under simplifying assumptions and complement them with experiments showing convergence even when these assumptions don't hold. We note that the same algorithm for transcript learning is used in the experiments as in the theorem. Our experiments confirm practical convergence of transcript learning on non-convex transformer architectures.

The technical novelty is limited. Key aspects of the convergence proof rely heavily on prior results by Shalev-Shwartz and Ben-David [2014], with little original contribution.

The technical novelty of this paper is in contributing a formal model for verifying correctness on every instance connecting a rich body of literature on interactive proofs to the area of generative models (as well as in the proofs of the convergence theorems on the use of transcript learning). Many impactful theoretical works have been first introduced in “definitional” papers; with a robust definition at hand, follow up works can yield general theorems. A case in point is the original work on “Zero Knowledge Interactive Proofs” where the first paper introduced the model and one example of zero-knowledge proof for one specific problem (distinguishing quadratic residues from non-residues) and shortly after in follow up work it was shown how to get zero-knowledge proofs for all of NP. Furthermore, using theoretical notions such as debate systems has improved the accuracy of generative models significantly; similarly, our self proving models could potentially lead to improved accuracy guarantees as well.

Experiment details We have conducted experiments demonstrating that our framework can be practically instantiated. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations on pairs of integers up to 10^4, following Charton's [1] setup.

Key results:

• Transcript Learning (TL): Achieved 60.3% verifiability (correctly proving answers) after training for 100k steps.
• RLVF: Improved a base model with 40% verifiability to 79.3%, albeit in significantly more (4M) iterations; while this is not an experimental paper, we will continue to explore a practical speedup by searching the hyperparameter space.
• TL + Annotations: Reached 96% verifiability by training on proofs annotated with intermediate Euclidean algorithm steps (similar to chain-of-thought); importantly, evaluation uses only the final proof.

Our proof system uses Bézout's theorem: the model must output coefficients a,b such that $a x_1 + b x_2 = GCD(x_1, x_2)$, which the verifier can use to easily check (with certainty) that the model's output is indeed the GCD.

More nuanced results show (1) more annotation steps improve verifiability monotonically, (2) even when trained with annotations, the model generalizes beyond the amount of annotations (i.e., it is not just memorizing the chain-of-thought, but exhibits length generalization), and (3) bases with more prime factors improve both correctness and verifiability—in line with Charton's findings.

While GCD is simpler than general theorem proving, it provides a concrete proof-of-concept that self-proving models can be trained in practice. We are happy to provide full experimental details and will include them in the camera-ready version.

[1] Francois Charton. Learning the greatest common divisor: explaining transformer predictions. ICLR 2024.

We sincerely thank you for your positive and constructive review. We appreciate your recognition of our careful definitions of correctness and soundness, our treatment of both worst-case and average-case scenarios, and our convergence analysis for transcript learning. Your feedback has helped us significantly improve the paper.

Regarding concerns

Empirical results: We will add experiments demonstrating the practical viability of our framework. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations. Key results include: Transcript Learning achieving 60.3% verifiability, RLVF improving a model from 40% to 79.3% verifiability, and Annotated TL reaching 96% verifiability. Our ablation studies reveal that models generalize beyond their training annotations and that representation choices significantly impact performance. Appended to this rebuttal are additional details. We will include analysis (with figures) in the camera-ready version and release the model and code publicly.

Paper organization: We will move the related works into the body of the paper. We follow the conventions of theory papers wherein theorems are formally stated in the body; proof overviews are given in the body, and the full details are deferred to the appendix.

Regarding questions

ZKP extension: That is an extremely interesting direction for future research. We note that already the current setup (IPs) has a secure system even when the LLM-prover is untrusted (this is the soundness property). ZK would guarantee that, an LLM-prover would not leak anything (e.g. sensitive training data) to the verifier. Thank you for encouraging this direction.

RLVF convergence: Unlike supervised learning, there is no "standard" set of assumptions for RL convergence theorems. Rather than arbitrarily choosing specific assumptions, we prove a Gradient Approximation Lemma from which convergence guarantees can be derived in particular settings. This mirrors the approach for, e.g., Policy Gradient methods, where the Policy Gradient Theorem (which is a gradient estimation lemma) provides the foundation from which specific algorithms derive their guarantees. See, for example, Chapter 3 of Reinforcement Learning: Theory and Algorithms by Agarwal, Jiang, Kakade and Sun (2022).

Experiment details: We have conducted experiments demonstrating that our framework can be practically instantiated. We trained 6.3M parameter transformers to compute and prove the correctness of GCD computations on pairs of integers up to 10^4, following Charton's [1] setup.

Key results:

• Transcript Learning (TL): Achieved 60.3% verifiability (correctly proving answers) after training for 100k steps.
• RLVF: Improved a base model with 40% verifiability to 79.3%, albeit in significantly more (4M) iterations; while this is not an experimental paper, we will continue to explore a practical speedup by searching the hyperparameter space.
• TL + Annotations: Reached 96% verifiability by training on proofs annotated with intermediate Euclidean algorithm steps (similar to chain-of-thought); importantly, evaluation uses only the final proof.

Our proof system uses Bézout's theorem: the model must output coefficients a,b such that $a x_1 + b x_2 = GCD(x_1, x_2)$, which the verifier can use to easily check (with certainty) that the model's output is indeed the GCD.

More nuanced results show (1) more annotation steps improve verifiability monotonically, (2) even when trained with annotations, the model generalizes beyond the amount of annotations (i.e., it is not just memorizing the chain-of-thought, but exhibits length generalization), and (3) bases with more prime factors improve both correctness and verifiability—in line with Charton's findings.

While GCD is simpler than general theorem proving, it provides a concrete proof-of-concept that self-proving models can be trained in practice. We are happy to provide full experimental details and will include them in the camera-ready version.

[1] Francois Charton. Learning the greatest common divisor: explaining transformer predictions. ICLR 2024.