Theorem Prover as a Judge for Synthetic Data Generation

• URL: http://arxiv.org/abs/2502.13137v1
• Date: Tue, 18 Feb 2025 18:57:09 GMT
• Title: Theorem Prover as a Judge for Synthetic Data Generation
• Authors: Joshua Ong Jun Leang, Giwon Hong, Wenda Li, Shay B. Cohen,
• Abstract summary: We present a framework that replaces human annotation with theorem prover in Reinforcement Learning from Human Feedback (RLHF)<n>Across multiple large language models (LLMs), applying TP-as-a-Judge and RF improves benchmarks with only 3,508 samples, achieving 5.56% accuracy on Mistral-7B for MultiArithm.
• Score: 22.124954482278536
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• R-PRM: Reasoning-Driven Process Reward Modeling [53.06844294668382]
  Process Reward Models (PRMs) have emerged as a promising solution by evaluating each reasoning step. Existing PRMs typically output evaluation scores directly, limiting both learning efficiency and evaluation accuracy. We propose Reasoning-Driven Process Reward Modeling (R-PRM) R-PRM generates seed data from limited annotations, effectively bootstrapping our model's reasoning capabilities.
  arXiv  Detail & Related papers  (2025-03-27T09:23:08Z)
• The First Few Tokens Are All You Need: An Efficient and Effective Unsupervised Prefix Fine-Tuning Method for Reasoning Models [69.798277882245]
  We introduce Unsupervised Prefix Fine-Tuning (UPFT) to enhance large language models' reasoning efficiency. UPFT removes the need for labeled data or exhaustive sampling. Experiments show that UPFT matches the performance of supervised methods.
  arXiv  Detail & Related papers  (2025-03-04T18:56:03Z)
• DeLTa: A Decoding Strategy based on Logit Trajectory Prediction Improves Factuality and Reasoning Ability [3.2561294196141835]
  This paper proposes a novel decoding strategy aimed at enhancing both factual accuracy and inferential reasoning. Our approach adjusts next-token probabilities by analyzing the trajectory of logits from lower to higher layers in Transformers. Experiments on TruthfulQA demonstrate that DeLTa attains up to a 4.9% improvement over the baseline.
  arXiv  Detail & Related papers  (2025-03-04T07:07:17Z)
• CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization [22.935127114462475]
  This paper introduces a Curriculum Learning-based DPO Iterative Theorem Proving (CuDIP) method. We propose a method for constructing preference data which utilizes LLMs and existing theorem proving data. We then integrate this preference data construction method with curriculum learning to iteratively fine-tune the theorem proving model.
  arXiv  Detail & Related papers  (2025-02-25T03:07:02Z)
• Exploring the Limit of Outcome Reward for Learning Mathematical Reasoning [65.2421542320293]
  Reasoning abilities are crucial components of general intelligence.<n>Recent advances by proprietary companies, such as o-series models of OpenAI, have made remarkable progress on reasoning tasks.<n>This paper proposes a new RL framework, termed OREAL, to pursue the performance limit that can be achieved through textbfOutcome textbfREwtextbfArd-based reinforcement textbfLearning for mathematical reasoning tasks.
  arXiv  Detail & Related papers  (2025-02-10T18:57:29Z)
• Bridging Internal Probability and Self-Consistency for Effective and Efficient LLM Reasoning [53.25336975467293]
  We present the first theoretical error decomposition analysis of methods such as perplexity and self-consistency.<n>Our analysis reveals a fundamental trade-off: perplexity methods suffer from substantial model error due to the absence of a proper consistency function.<n>We propose Reasoning-Pruning Perplexity Consistency (RPC), which integrates perplexity with self-consistency, and Reasoning Pruning, which eliminates low-probability reasoning paths.
  arXiv  Detail & Related papers  (2025-02-01T18:09:49Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a novel theorem proving method that enjoys superior sample efficiency.<n>Our method is validated on the miniF2F-test benchmark using the open-source deepseek-math-7b-base model and the Isabelle proof assistant.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  This paper focuses on improving LLMs' ability to write proofs in formal languages that permit automated proof verification/evaluation. We work in a more natural setup where the lemmas that are directly relevant to the theorem are not given to the theorem prover at test time. We design an RL-based training algorithm that encourages the model to decompose a theorem into lemmas, prove the lemmas, and then prove the theorem by using the lemmas.
  arXiv  Detail & Related papers  (2024-11-04T05:57:40Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation. For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• Step Guided Reasoning: Improving Mathematical Reasoning using Guidance Generation and Step Reasoning [7.965282234763401]
  Step Guidied Reasoning is more stable and generalizable than few-shot methods.<n>We demonstrate the significant effect of Step Guidied Reasoning in augmenting mathematical performance in state-of-the-art language models.
  arXiv  Detail & Related papers  (2024-10-18T01:38:24Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  We introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. We fine-tune the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs. Our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any.
  arXiv  Detail & Related papers  (2024-05-23T09:03:42Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.