Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving

• URL: http://arxiv.org/abs/2503.09730v1
• Date: Wed, 12 Mar 2025 18:20:47 GMT
• Title: Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
• Authors: Sara Rajaee, Kumar Pratik, Gabriele Cesa, Arash Behboodi,
• Abstract summary: We propose a novel verifier-in-the-loop design for Automatic Theorem Proving task.<n>We empirically show that the step-by-step local verification produces a global improvement in the model's reasoning accuracy and efficiency.
• Score: 17.289776394847063
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The most promising recent methods for AI reasoning require applying variants of reinforcement learning (RL) either on rolled out trajectories from the model, even for the step-wise rewards, or large quantities of human annotated trajectory data. The reliance on the rolled-out trajectory renders the compute cost and time prohibitively high. In particular, the correctness of a reasoning trajectory can typically only be judged at its completion, leading to sparse rewards in RL or requiring expensive synthetic data generation in expert iteration-like methods. In this work, we focus on the Automatic Theorem Proving (ATP) task and propose a novel verifier-in-the-loop design, which unlike existing approaches that leverage feedback on the entire reasoning trajectory, employs an automated verifier to give intermediate feedback at each step of the reasoning process. Using Lean as the verifier, we empirically show that the step-by-step local verification produces a global improvement in the model's reasoning accuracy and efficiency.

Related papers

• CAPO: Towards Enhancing LLM Reasoning through Verifiable Generative Credit Assignment [39.965170904699974]
  Reinforcement Learning with Verifiable Rewards (RLVR) has improved the reasoning abilities of Large Language Models (LLMs) by using rule-based binary feedback.<n>Current RLVR methods treat whole responses as single actions, assigning the same reward to every token.<n>This coarse-grained feedback hampers precise credit assignment, making it hard for models to identify which reasoning steps lead to success or failure.
  arXiv  Detail & Related papers  (2025-08-04T11:06:08Z)
• Revisiting LLM Reasoning via Information Bottleneck [57.519119962528166]
  Large language models (LLMs) have recently demonstrated remarkable progress in reasoning capabilities through reinforcement learning with verifiable rewards (RLVR)<n>We present a theoretical characterization of LLM reasoning grounded in information bottleneck (IB) principle.<n>We propose IB-aware reasoning optimization (IBRO), a framework that encourages reasoning trajectories to be both informative about the final correct answer and generalizable.
  arXiv  Detail & Related papers  (2025-07-24T13:14:25Z)
• AALC: Large Language Model Efficient Reasoning via Adaptive Accuracy-Length Control [18.273777938294327]
  Large reasoning models (LRMs) achieve impressive reasoning capabilities by generating lengthy chain-of-thoughts.<n>We introduce AALC, a lightweight, accuracy-aware length reward integrated into reinforcement learning.<n>We show that our approach reduces response length by over 50% while maintaining or even improving the original accuracy.
  arXiv  Detail & Related papers  (2025-06-25T06:29:18Z)
• Reinforcing General Reasoning without Verifiers [47.72684162518086]
  We propose a verifier-free method (VeriFree) that bypasses answer verification and instead uses RL to directly maximize the probability of generating the reference answer.<n>VeriFree matches and even surpasses verifier-based methods on extensive evaluations across MMLU-Pro, GPQA, SuperGPQA, and math-related benchmarks.
  arXiv  Detail & Related papers  (2025-05-27T17:56:27Z)
• 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.<n>UPFT removes the need for labeled data or exhaustive sampling.<n> Experiments show that UPFT matches the performance of supervised methods.
  arXiv  Detail & Related papers  (2025-03-04T18:56:03Z)
• Optimizing Diffusion Models for Joint Trajectory Prediction and Controllable Generation [49.49868273653921]
  Diffusion models are promising for joint trajectory prediction and controllable generation in autonomous driving. We introduce Optimal Gaussian Diffusion (OGD) and Estimated Clean Manifold (ECM) Guidance. Our methodology streamlines the generative process, enabling practical applications with reduced computational overhead.
  arXiv  Detail & Related papers  (2024-08-01T17:59:59Z)
• Adaptive $Q$-Network: On-the-fly Target Selection for Deep Reinforcement Learning [18.579378919155864]
  We propose Adaptive $Q$Network (AdaQN) to take into account the non-stationarity of the optimization procedure without requiring additional samples. AdaQN is theoretically sound and empirically validate it in MuJoCo control problems and Atari $2600 games.
  arXiv  Detail & Related papers  (2024-05-25T11:57:43Z)
• REBEL: Reward Regularization-Based Approach for Robotic Reinforcement Learning from Human Feedback [61.54791065013767]
  A misalignment between the reward function and human preferences can lead to catastrophic outcomes in the real world.<n>Recent methods aim to mitigate misalignment by learning reward functions from human preferences.<n>We propose a novel concept of reward regularization within the robotic RLHF framework.
  arXiv  Detail & Related papers  (2023-12-22T04:56:37Z)
• Let's reward step by step: Step-Level reward model as the Navigators for Reasoning [64.27898739929734]
  Process-Supervised Reward Model (PRM) furnishes LLMs with step-by-step feedback during the training phase. We propose a greedy search algorithm that employs the step-level feedback from PRM to optimize the reasoning pathways explored by LLMs. To explore the versatility of our approach, we develop a novel method to automatically generate step-level reward dataset for coding tasks and observed similar improved performance in the code generation tasks.
  arXiv  Detail & Related papers  (2023-10-16T05:21:50Z)
• Provable Reward-Agnostic Preference-Based Reinforcement Learning [61.39541986848391]
  Preference-based Reinforcement Learning (PbRL) is a paradigm in which an RL agent learns to optimize a task using pair-wise preference-based feedback over trajectories. We propose a theoretical reward-agnostic PbRL framework where exploratory trajectories that enable accurate learning of hidden reward functions are acquired.
  arXiv  Detail & Related papers  (2023-05-29T15:00:09Z)
• End-to-End Meta-Bayesian Optimisation with Transformer Neural Processes [52.818579746354665]
  This paper proposes the first end-to-end differentiable meta-BO framework that generalises neural processes to learn acquisition functions via transformer architectures. We enable this end-to-end framework with reinforcement learning (RL) to tackle the lack of labelled acquisition data.
  arXiv  Detail & Related papers  (2023-05-25T10:58:46Z)
• Self-Evaluation Guided Beam Search for Reasoning [61.523627290397556]
  We introduce a stepwise self-evaluation mechanism to guide and calibrate the reasoning process of Large Language Model (LLM) We propose a decoding algorithm integrating the self-evaluation guidance via beam search. Our approach surpasses the corresponding Codex-backboned baselines in few-shot accuracy by $6.34%$, $9.56%$, and $5.46%$ on the GSM8K, AQuA, and StrategyQA.
  arXiv  Detail & Related papers  (2023-05-01T02:37:59Z)
• Efficient Learning of Accurate Surrogates for Simulations of Complex Systems [0.0]
  We introduce an online learning method empowered by sampling-driven sampling. It ensures that all turning points on the model response surface are included in the training data. We apply our method to simulations of nuclear matter to demonstrate that highly accurate surrogates can be reliably auto-generated.
  arXiv  Detail & Related papers  (2022-07-11T20:51:11Z)
• Leveraging Unlabeled Data to Predict Out-of-Distribution Performance [63.740181251997306]
  Real-world machine learning deployments are characterized by mismatches between the source (training) and target (test) distributions. In this work, we investigate methods for predicting the target domain accuracy using only labeled source data and unlabeled target data. We propose Average Thresholded Confidence (ATC), a practical method that learns a threshold on the model's confidence, predicting accuracy as the fraction of unlabeled examples.
  arXiv  Detail & Related papers  (2022-01-11T23:01:12Z)
• Ordering-Based Causal Discovery with Reinforcement Learning [31.358145789333825]
  We propose a novel RL-based approach for causal discovery, by incorporating RL into the ordering-based paradigm. We analyze the consistency and computational complexity of the proposed method, and empirically show that a pretrained model can be exploited to accelerate training.
  arXiv  Detail & Related papers  (2021-05-14T03:49:59Z)
• Pre-training Is (Almost) All You Need: An Application to Commonsense Reasoning [61.32992639292889]
  Fine-tuning of pre-trained transformer models has become the standard approach for solving common NLP tasks. We introduce a new scoring method that casts a plausibility ranking task in a full-text format. We show that our method provides a much more stable training phase across random restarts.
  arXiv  Detail & Related papers  (2020-04-29T10:54:40Z)

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.