PaperlayerView exact revision on arXiv

Source-linked AI summary

Theorem Prover as a Judge for Synthetic Data Generation

Joshua Ong Jun Leang, Giwon Hong, Wenda Li, Shay B. Cohen

arXiv:2502.13137v2cs.AI

TL;DR

Intermediate mathematical reasoning can contain errors, while autoformalisation for theorem-prover checking can fail on complex tasks. The paper combines iterative autoformalisation, theorem-prover assessment of synthetic reasoning, and theorem-prover feedback for model training. With 3,508 samples, the approach reports results comparable to large-sample training and competitive GSM8K and AIME 2024 performance against models fine-tuned on larger datasets.

  • Problem

    Intermediate LLM reasoning can contain errors, and autoformalisation errors can cause theorem-prover execution failures on complex tasks.

    Source: §1 · p. 1

  • Method

    The paper iteratively refines formalisation using prover errors, applies theorem-prover verification to synthetic reasoning, and uses the feedback in RLTPF instead of human annotation.

    Source: §1 · p. 2

  • Results

    With 3,508 samples, TP-as-a-Judge with RLTPF achieves results comparable to large-sample training and competitive GSM8K and AIME 2024 performance against models fine-tuned on larger datasets.

    Source: §1 · p. 2, §6 · p. 9

  • Takeaways & Limitations

    The authors report that theorem-prover feedback improves training data efficiency and underscore the importance of intermediate reasoning for data quality.

    Source: §1 · p. 2

    The implementation focuses on algebra, counting, probability, and problem-solving; computational constraints particularly limit scalability above 8 billion parameters.

    Source: Limitations · p. 9

Abstract

from arXiv · show

The demand for synthetic data in mathematical reasoning has increased due to its potential to enhance the mathematical capabilities of large language models (LLMs). However, ensuring the validity of intermediate reasoning steps remains a significant challenge, affecting data quality. While formal verification via theorem provers effectively validates LLM reasoning, the autoformalisation of mathematical proofs remains error-prone. In response, we introduce iterative autoformalisation, an approach that iteratively refines theorem prover formalisation to mitigate errors, thereby increasing the execution rate on the Lean prover from 60% to 87%. Building upon that, we introduce Theorem Prover as a Judge (TP-as-a-Judge), a method that employs theorem prover formalisation to rigorously assess LLM intermediate reasoning, effectively integrating autoformalisation with synthetic data generation. Finally, we present Reinforcement Learning from Theorem Prover Feedback (RLTPF), a framework that replaces human annotation with theorem prover feedback in Reinforcement Learning from Human Feedback (RLHF). Across multiple LLMs, applying TP-as-a-Judge and RLTPF improves benchmarks with only 3,508 samples, achieving 5.56% accuracy gain on Mistral-7B for MultiArith, 6.00% on Llama-2-7B for SVAMP, and 3.55% on Llama-3.1-8B for AQUA.

1 Introduction

The paper targets errors in intermediate mathematical reasoning and the difficulty of formalising proofs for theorem-prover verification. It proposes iterative autoformalisation, TP-as-a-Judge, and RLTPF, reporting competitive GSM8K and AIME 2024 performance against models fine-tuned on larger datasets.

1 Introduction

  • LLM reasoning can contain flawed intermediate steps even when the final answer appears plausible, motivating checks of reasoning validity rather than answers alone.The introduction notes that flawed steps can occur even when the correct answer is reached.Source: §1 · p. 1, Figure 1 · p. 1
  • Theorem provers validate logical reasoning, but autoformalisation errors can cause execution failures on complex tasks.The introduction also notes that Python can struggle with Olympiad-level problems.Source: §1 · p. 1
  • Iterative autoformalisation uses formalisation errors as feedback to verify each intermediate step; discarding questions after one failed attempt risks bias toward simpler problems.Unlike Python approaches that refine execution traces, it refines proof tactics, theorems, and logical steps within the formal system.Source: §1 · p. 2
  • TP-as-a-Judge integrates theorem-prover step-by-step verification into synthetic data generation for mathematical reasoning tasks.The introduction contrasts this with LLM-as-a-Judge, which can introduce bias.Source: §1 · pp. 1–2
  • TP-as-a-Judge with RLTPF achieves competitive GSM8K and AIME 2024 performance against models fine-tuned on larger datasets, while improving training data efficiency.The authors relate this result to the importance of intermediate reasoning for data quality.Source: §1 · p. 2
  • RLTPF replaces human annotators with formalised theorem-prover feedback for reinforcement learning.The authors report that this approach achieves competitive performance on GSM8K and AIME 2024 compared with models fine-tuned on larger datasets.Source: §1 · p. 2

2 Theorem Prover as a Judge

The framework generates synthetic mathematical questions and answers, checks their formalisation with a theorem prover, and uses verification outcomes to train models. Iterative autoformalisation refines execution failures, while question and answer checks determine which examples are retained or used for preference training.

2 Theorem Prover as a Judge

  • The framework generates questions and answers, verifies them with a theorem prover, then uses verification results for SFT and DPO.The answer-generation process uses gpt-4o and chatgpt-4o-latest, with gpt-4o also used for autoformalisation.Source: §2 · p. 2, §2.2 · p. 3

2.1 LLM Data Generation

  • Synthetic question-answer generation uses Reverse Question-Answering, prompting models to generate questions aligned with example solutions from GSM8K and MATH.The setup focuses on problem solving, algebra, and counting and probability.Source: §2.1 · pp. 2–3

2.2 Theorem Prover Verification

  • Theorem-prover verification of generated questions also filters out questions that lack clarity.The question formalisation process is described as a four-phase approach.Source: §2.2.1 · p. 3

2.2.1 Question Formalisation

  • Question formalisation converts each question to a symbolic representation, formalises it, translates it back to natural language, and checks alignment with the original.Questions whose original and final representations differ are flagged as inconsistent or poorly formalised and excluded from answer formalisation.Source: §2.2.1 · p. 3

2.2.2 Answer Formalisation

  • For answer formalisation, a theorem prover validates each reasoning step; false answers may be removed or kept for RLTPF, while execution errors trigger iterative refinement.An answer is verified if all steps are validated and false if any step is refuted.Source: §2.2.2 · pp. 3–4

2.2.3 Iterative Autoformalisation

  • Iterative refinement improves Lean prover formalisation execution from 60% to 87% after up to five iterations.The model revises and reverifies individual mathematical steps using theorem-prover errors as feedback.Source: §2.2.3 · p. 4

2.3 Reinforcement Learning from Theorem Prover Feedback (RLTPF)

  • RLTPF trains sequentially with SFT on verified data followed by DPO on pairs where one model response is verified and the other is rejected.When both responses are verified, the data is allocated to SFT.Source: §2.3 · p. 4, Table 1 · p. 4

3 Experimental Setup

The experiments use a 3,508-sample synthetic dataset and evaluate multiple language models on mathematical benchmarks. The setup compares prompting and training baselines using Pass@1 accuracy, with dataset-specific answer evaluation procedures.

3 Experimental Setup

  • SIMQA contains 3,508 samples: 1,876 generated from GSM8K and 1,632 from MATH.The evaluation dataset list includes SVAMP, GSM8K, MultiArith, GSMSymbolic-p1, MATH-500, AQUA, AIME 2024, and OlympiadBench.Source: §3 · p. 5
  • The study evaluates five base models, including Llama-2-7B, Llama-3.2-3B, Llama-3.1-8B, OLMo-2-7B, and Mistral-7B, using LoRA fine-tuning.The authors describe these as general-purpose models without specific mathematical reasoning specialisation.Source: §3 · p. 5
  • Baselines are standard prompting, Chain of Thought prompting, and model training with RLTPF on the 3,508-sample synthetic dataset.The prompts for model training follow the CoT template for comparison.Source: §3 · p. 5
  • Pass@1 accuracy is the primary metric; exact matching is used where possible, with numerical parsing or gpt-4o-mini alignment scoring for specified datasets.The gpt-4o-mini procedure is used for MATH-500, AIME, and OlympiadBench.Source: §3 · p. 5

4 Experimental Results

Across mathematical benchmarks, TP-as-a-Judge and RLTPF show gains with a 3,508-sample dataset, while analyses examine verification accuracy and iterative autoformalisation. Results vary by model and benchmark, and SFT/DPO allocation affects training performance.

4.1 Main Results

  • Llama models improve over CoT with TP-as-a-Judge, including Llama-2-7B gains on MultiArith (39.44% →59.44%), SVAMP (38.00% →44.00%), and GSM8K (10.33% →16.70%).Llama-3.1-8B also improves on GSM-Symbolic (55.60% →58.20%) and AQUA (53.54% →57.09%); Llama-3.2-3B improves on GSM-Symbolic (55.80% →59.60%).Source: §4.1 · p. 5
  • With 3,508 samples, RLTPF-based TP-as-a-Judge achieves competitive benchmark performance against synthetic-data models fine-tuned on larger datasets.Llama-3.1-8B with RLTPF outperforms most models but remains slightly behind OpenMath-2 on GSM8K; Llama-3.2-3B with RLTPF achieves the highest AIME 2024 performance.Source: Table 3 · p. 6, §4.1 · p. 6
  • OLMo-2-7B improves across evaluated tasks, while Mistral-7B decreases on GSM8K by 0.84% and MATH by 1.2% but gains 3.2% on GSM-Symbolic.The results also report a substantial gap between standard prompting and CoT reasoning, and stronger reasoning performance by more advanced models on MATH-500.Source: §4.1 · pp. 5–6

4.2 Analysis

  • In an analysis of 2,000 SIMQA samples using GSM8K as the few-shot example, 30% failed question formalisation; among the remaining 70%, approximately 5% exhibited Lean prover execution errors during answer formalisation.Source: §4.2 · p. 6
  • TP-as-a-Judge scores F1 0.87 and recall 0.91, versus o1-mini's F1 0.72 and recall 0.78; the LLM judge produces twice as many false positives.The comparison is notable because o1-mini achieves 94.80% accuracy on GSM8K, yet scores lower on reasoning-step verification.Source: §4.2 · p. 7

4.3 Robustness to Iterative Autoformalisation

  • About 40% of 356 samples required iterative refinement, and most successful refinements completed by the third iteration, though some cases remained incorrect after seven attempts.Manual inspection found syntax or theorem/tactic errors commonly needed one or two more iterations; iteration count also correlated positively with sequence length.Source: §4.3 · pp. 7–8
  • Lean feedback lets iterative autoformalisation refine both syntax and theorem choice, supporting verification of intermediate steps in complex proofs.The authors attribute typical errors to an incorrect theorem or tactic, or invalid Lean syntax.Source: §4.3 · pp. 7–8

4.4 Effectiveness of RLTPF in TP-as-a-Judge

  • Among tested training strategies, RLTPF with separate preferences for verified and rejected instances achieves the highest accuracy, while combining it with SFT on all instances degrades performance.SFT on all available instances alone has the highest SFT accuracy, and SFT using only rejected instances performs worse than using only verified instances.Source: §4.4 · p. 8

5 Related Work

Prior work explores synthetic chain-of-thought data and verification, but intermediate-step errors remain difficult to detect. The related work also describes theorem provers and formal-proof methods for LLMs.

Math Data Synthesis Advancements

  • Math-reasoning datasets are often distilled from frontier models, but intermediate steps can be erroneous, and rejection sampling does not guarantee their correctness.The cited discussion notes diminishing returns from scaling CoT datasets, including OpenMathInstruct's reported 3.9% MATH improvement after an 8× dataset increase.Source: §5 · p. 8
  • STaR, Lean-STaR, and rStar-Math use multiple rollouts and trajectories for verification and synthesis [Zelikman et al., 2022; Lin et al., 2024; Guan et al., 2025].The passages also describe rejection sampling as filtering less reliable outputs without guaranteeing intermediate-step correctness.Source: §5 · p. 8

Theorem Proving and Autoformalisation

  • Draft-Sketch-Prove develops formal proving by generating informal proofs, translating them into formal sketches, and completing them with symbolic tools [Jiang et al., 2023b].The section situates this approach alongside theorem provers such as Lean, Isabelle, and Coq.Source: §5 · pp. 8–9

6 Conclusion

The conclusion presents TP-as-a-Judge as a framework for verifying intermediate reasoning in synthetic mathematical data. It combines iterative autoformalisation with Auto-Informalisation, Alignment Check, and RLTPF, reporting accuracy gains with 3,508 samples comparable to larger datasets.

6 Conclusion

  • TP-as-a-Judge combines synthetic-data generation, theorem-prover verification, and RLTPF to target correctness of intermediate reasoning steps.Iterative autoformalisation refines formalisation until execution succeeds; Auto-Informalisation and Alignment Check address question formalisation errors.Source: §6 · p. 9
  • RLTPF separates data into SFT and DPO subsets and trains sequentially, with TP-as-a-Judge improving accuracy using 3,508 samples.The authors report results comparable to those obtained with larger samples.Source: §6 · p. 9
  • The conclusion presents autoformalisation as a promising direction for improving mathematical reasoning in LLMs.It reports that Auto-Informalisation and Alignment Check reduce autoformalisation errors and improve verification consistency.Source: §6 · p. 9

Limitations

The approach is bounded by its mathematical scope, imperfect formalisation, limits on problem complexity, and computational demands.

Limitations

  • Theorem-prover verification remains challenging beyond mathematics, leaving extension of the approach to other domains an open research question.Formalisation also requires further refinement for broader applicability.Source: Limitations · p. 9
  • The implementation focuses on algebra, counting, probability, and problem-solving datasets, while the model’s problem-solving ability limits the complexity of generated questions.When generating more challenging problems, the model often fails, preventing creation of more advanced mathematical questions.Source: Limitations · p. 9
  • Computational constraints limit scalability, particularly for models exceeding 8 billion parameters, and iterative formalisation incurs high computational cost.Multiple refinement cycles are needed to ensure correct execution.Source: Limitations · p. 9

A Detailed Breakdown of Dataset

The appendix details the dataset’s sample composition, generation settings, and training procedure, including its reported overall count of 3,508 samples.

A Detailed Breakdown of Dataset

A.1 SIMQA dataset Creation Details

  • The SIMQA synthetic dataset was created using gpt-4o models, including two dated versions, or ChatGPT-4o-latest.The models were used alternatively for SIMQA dataset creation.Source: §A.1 · p. 14

A.2 Generation Parameters

  • SIMQA generation used temperature 0.0, corresponding to greedy decoding.Source: §A.2 · p. 14

A.3 Experimental Settings

  • Questions used few-shot prompts, answers used zero-shot prompts, and theorem-prover formalisation used 10, 8, or 6 shots depending on the dataset.Formalisation used 10 shots for GSM8K, 8 for MATH Algebra, and 6 for MATH Counting and Probability.Source: §A.3 · p. 14

A.4 Cost for Dataset Creation

  • Dataset creation cost approximately $50 per 300 samples, averaging $0.60 per sample, with total expense varying by iteration count.The authors report that fewer iterations may reduce costs.Source: §A.4 · p. 14

B Details on hyperparameters Tuning

  • RLTPF training used one SFT epoch followed by three DPO epochs, with an effective batch size of 64 in each phase.Both phases used a learning rate of 3 × 10−5; evaluation occurred at fixed intervals, and experiments used two 80-GB A100 GPUs.Source: B Details on hyperparameters Tuning · pp. 14–15

C Consistency Check

Three-seed checks found generally stable accuracy across runs, while variability was higher on GSM8K-Symbolic and AIME and the evaluation covered only two models.

C Consistency Check

  • GSM8K-Symbolic and AIME showed higher standard deviation across three runs, suggesting true accuracy may be higher than reported values.Average accuracy remained stable across runs overall, with relatively low standard deviation.Source: C Consistency Check · p. 15
  • Evaluation was limited by computational constraints to Llama-3.2-3B and Llama-3.1-8B, although the authors report robustness and stability across runs.Source: C Consistency Check · p. 15

D Evaluation Metrics

The evaluation section describes benchmark scoring, while the autoformalisation analysis reports how many refinement iterations successful Lean verification required.

D Evaluation Metrics

  • For MATH-500, AIME, and OlympiadBench, evaluation followed a strategy similar to Leang et al. (2024), using gpt-4o-mini to assess answer alignment.Most benchmarks used exact match; the gpt-4o-mini assessment compared the final two output sentences with ground truth.Source: D Evaluation Metrics · p. 15

E Iterative Autoformalisation

G Breakdown of Theorem Prover as a Judge

The breakdown describes a staged formalisation pipeline whose components support question formalisation and verification accuracy, and reports the resulting error categories.

G Breakdown of Theorem Prover as a Judge

  • Autoformalised questions must align with their originals, and prior approaches often use multiple LLM calls and expensive automated theorem proving (Li et al., 2024b; Poiroux et al., 2024).Source: G Breakdown of Theorem Prover as a Judge · p. 16
  • The pipeline separates question and answer formalisation, with question formalisation improving answer verification (Jiang et al., 2023b).CoMAT facilitates question formalisation, while alignment checks support verification accuracy.Source: G Breakdown of Theorem Prover as a Judge · p. 16
  • S1 CoMAT improves performance by approximately 20%, while S2 enhances answer formalisation.S3 Auto-Informalisation and S4 alignment checks assess whether question formalisation and autoformalisation were performed correctly.Source: G Breakdown of Theorem Prover as a Judge · p. 16
  • S3 Auto-Informalisation and S4 alignment checks provide verification metrics, while misalignments may lead to disposal before answer formalisation.The passage notes that no definitive metrics validate question-formalisation correctness.Source: G Breakdown of Theorem Prover as a Judge · pp. 16–17
  • 23.10% of samples had question-formalisation errors, 5.4% had answer-formalisation errors, and 71.50% were categorised as verified or false.Table 11 provides the component-level error-rate breakdown.Source: Table 11 · p. 17, G Breakdown of Theorem Prover as a Judge · p. 17

H Few-shot Examples for Synthetic Data Creation

This section documents the reverse question-answering setup, manual validation, and worked examples used for synthetic-data creation.

H Few-shot Examples for Synthetic Data Creation

  • Synthetic questions are generated by giving the model only solutions as few-shot examples, so it must reconstruct problem statements from them.Question-answer pairs from GSM8K and some MATH problems are then used as few-shot examples for Lean formalisation.Source: H Few-shot Examples for Synthetic Data… · p. 17

I Manual Annotation Details

  • 54 GSM8K-synthetic instances were randomly sampled for manual validation by a mathematics and statistics bachelor’s graduate instructed to solve the problems.The annotation checks the correctness of theorem-prover validations.Source: I Manual Annotation Details · p. 17

Few Shot Examples for GSM8K

Algebra

  • Worked algebra examples derive 2 vertical asymptotes for a rational function and n = 401 for a functional equation.Source: Algebra · pp. 21, 23

Counting and Probability

  • Counting and probability examples derive 8/63 for weighted dice, 35/128 for matching coin-head counts, and 24 triforce colorings.The coloring example treats rotations as distinct.Source: Counting and Probability · pp. 23–25

J Examples for Manual Annotation

This appendix section presents manual-annotation examples showing how theorem-prover labels accept or reject proposed solutions, alongside iterative autoformalisation and its use in preference training. One example traces corrections to a selling-price equation and verified calculations, including earlier attempts with unsolved goals.

J Examples for Manual Annotation

  • Emily’s answer of $3,625 was marked Verified, with reported revenue of $6,125 exceeding the $3,625 required amount.The answer is framed as covering costs and leaving a donation of at least $2,000.Source: J Examples for Manual Annotation · p. 26
  • The factory’s proposed answer of 320 widgets was marked False by verification.The question asks how many widgets are needed after variable costs rise 25% and the selling price rises 10%.Source: J Examples for Manual Annotation · p. 28
  • Sara’s 8-week answer was marked Verified, but the reported actual result was FALSE at 2.75 weeks.This example is labeled as a verification of solutions on a bad-clarity question.Source: J Examples for Manual Annotation · pp. 29–30
  • $414,000 was marked False, while the revised $324,468.09 selling-price answer was marked Verified.The two answers address the same property-sale question but reach different results.Source: J Examples for Manual Annotation · pp. 31–32

K Example of Iterative Autoformalisation

  • Question formalisation uses CoMAT, autoformalisation, Auto-Informalisation, and Alignment Check; answer formalisation refines Lean code over three iterations.When one formalisation is False and another is Verified, the model is trained using Direct Preference Optimisation.Source: K Example of Iterative Autoformalisation · p. 33

Question Formalisation

  • The question formalisation encodes five-year property growth as two full 25% increases plus a half-period increase, and computes selling price from profit, investment, renovations, and commission.The Lean definitions set selling price to (profit + initial investment + renovation cost) / (1 − commission rate).Source: Question Formalisation · p. 33
  • In Lean, the five-year property value is 2109375/8, total expenses are 2560000/47, and computed profit equals the target profit under the unfolded definitions.Source: Question Formalisation · p. 35
  • The corrected equation sets selling_price to (profit + initial_investment + renovation_cost) / (1 - commission_rate), and Lean verifies it as 15250000/47.The example evaluates the result as verified and approximately 324468.085106383.Source: Question Formalisation · p. 36

Error for Answer Formalisation 1

  • The first autoformalisation reports unsolved goals for value_after_4_years and total_expenses (272340427/5000), plus computed_profit, while its output also records verified.The reported rational amount is (32446809 : Rat)/100.Source: Error for Answer Formalisation 1 · p. 37

Error for Answer Formalisation 2

  • The second answer formalisation also reports unsolved goals, including the profit equation with a 3/50 commission rate.The error output then restarts the file and shows selling_price as 15250000/47.Source: Error for Answer Formalisation 2 · p. 37

Related papers

Loading 2502.13137v2…