On Reasoning-Centric LLM-based Automated Theorem Proving

• URL: http://arxiv.org/abs/2604.19558v1
• Date: Tue, 21 Apr 2026 15:11:42 GMT
• Title: On Reasoning-Centric LLM-based Automated Theorem Proving
• Abstract summary: We introduce ReCent-Prover, a reasoning-centric proof agent for Rocq.<n>We show that ReCent-Prover achieves a 22.58% relative improvement in the number of proved theorems over the previous state-of-the-art.
• Score: 1.8002666661892468
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated theorem proving is fundamental to formal methods, and the recent trend is to integrate large language models (LLMs) and proof assistants to form effective proof agents. While existing proof agents show promising performance, they inadequately leverage reasoning capabilities of modern LLMs in high-level planning and self-critique. We argue that proof agents should not merely generate tactics but also reason strategically about proof plans and critically evaluate their own proposals. This paper introduces ReCent-Prover, a reasoning-centric LLM-based proof agent for Rocq that addresses two critical limitations in current systems. First, we present validation with reflection, enabling LLMs to scrutinize their generated tactics and synthesize failure summaries when reflection identifies potential errors, filtering out potentially misapplied tactics earlier. Second, we propose retrieval with planning, which conditions retrieval on LLM-generated proof plans rather than subgoal similarity, retrieving lemmas and proofs that align with the anticipated proof strategy. Both techniques increase the number of invocations of LLMs. However, when evaluated on the CoqStoq benchmark, even under the same budget of LLM invocations, ReCent-Prover achieves a 22.58% relative improvement in the number of proved theorems over the previous state-of-the-art, demonstrating that our reasoning-centric design significantly enhances automated theorem proving capabilities.

Related papers

• A Learning Method for Symbolic Systems Using Large Language Models [2.3263761713486066]
  We propose LLM2Ltac as an intelligent synthesizers to mine purely symbolic tactics from data.<n>We implement LLM2Ltac on Rocq 8.20.0 and mine tactics from 11,725 theorems in the standard library.<n>Results show that the mined tactics improve CoqHammer to prove 23.87% more theorems, and when integrating the improved CoqHammer with Claude Code, the overall proved theorems increases by 9.90%.
  arXiv  Detail & Related papers  (2026-05-09T05:05:02Z)
• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  We present PROMISE, a structure-aware framework that reframes proof generation as a stateful search over proof-state transitions.<n>We evaluate PROMISE on the seL4 benchmark across multiple LLM backends and compare it with prior systems such as Selene and Rango.
  arXiv  Detail & Related papers  (2026-04-07T03:49:12Z)
• On Multi-Step Theorem Prediction via Non-Parametric Structural Priors [50.16583672681106]
  In this work, we explore training-free theorem prediction through the lens of in-context learning (ICL)<n>We propose Theorem Precedence Graphs, which encode temporal dependencies from historical solution traces as directed graphs, and impose explicit topological constraints that effectively prune the search space during inference.<n>Experiments on the FormalGeo7k benchmark show that our method achieves 89.29% accuracy, substantially outperforming ICL baselines and matching state-of-the-art supervised models.
  arXiv  Detail & Related papers  (2026-03-05T06:08:50Z)
• A State-Transition Framework for Efficient LLM Reasoning [58.18141262230392]
  Long Chain-of-Thought (CoT) reasoning significantly improves Large Language Models (LLMs) performance on complex reasoning tasks.<n>Existing studies usually enhance the reasoning efficiency of LLMs by compressing CoT sequences.<n>We propose an efficient reasoning framework that models the reasoning process of LLMs as a state-transition process.
  arXiv  Detail & Related papers  (2026-02-01T12:40:40Z)
• Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
  We propose a lightweight alternative for step-level reasoning verification based on data-driven uncertainty scores.<n>Our findings suggest that the internal states of LLMs encode their uncertainty and can serve as reliable signals for reasoning verification.
  arXiv  Detail & Related papers  (2025-11-09T03:38:29Z)
• Reasoning with Preference Constraints: A Benchmark for Language Models in Many-to-One Matching Markets [13.111181135818184]
  Large language models (LLMs) have shown strong performance on complex mathematical tasks, including optimization.<n>Applying LLMs to matching problems, which require reasoning under preferential and structural constraints, remains underexplored.<n>We employ a novel benchmark of 369 instances of the College Admission Problem to evaluate LLMs across key dimensions: feasibility, stability, and optimality.
  arXiv  Detail & Related papers  (2025-09-16T14:48:46Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  Large Language Models (LLMs) have demonstrated strong generalization across a wide range of tasks.<n>Recent studies have shifted attention from explicit chain-of-thought prompting toward implicit reasoning.<n>This survey introduces a taxonomy centered on execution paradigms, shifting the focus from representational forms to computational strategies.
  arXiv  Detail & Related papers  (2025-09-02T14:16:02Z)
• 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)
• Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving [14.569345246475509]
  Large language models (LLMs) have shown promising first-order logic (FOL) reasoning capabilities.<n>However, their effectiveness in complex mathematical reasoning involving multi-step FOL deductions is still under-researched.<n>We propose DREAM, a self-adaptive solution that enhances the Diversity and REAsonability of LLMs' generation strategies.
  arXiv  Detail & Related papers  (2025-06-20T16:09:56Z)
• Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
  Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning.<n>We propose a neuro-symbolic approach that combines LLMs' generative strengths with structured components to overcome this challenge.
  arXiv  Detail & Related papers  (2025-05-20T15:13:32Z)
• Are LLMs Rigorous Logical Reasoners? Empowering Natural Language Proof Generation by Stepwise Decoding with Contrastive Learning [14.718645333008332]
  The recent advancement of large language models has led to significant progress in natural language proof planning.<n>We propose a stepwise decoding approach augmented by contrastive learning to address two common errors encountered during the generator's decoding process.
  arXiv  Detail & Related papers  (2023-11-12T05:12:49Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  Causal explanations of predictions of NLP systems are essential to ensure safety and establish trust. Existing methods often fall short of explaining model predictions effectively or efficiently. We propose two approaches for counterfactual (CF) approximation.
  arXiv  Detail & Related papers  (2023-10-01T07:31:04Z)

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.