On Reasoning-Centric LLM-based Automated Theorem Proving

TL;DR

This paper introduces ReCent-Prover, a reasoning-centric proof agent that enhances automated theorem proving by enabling strategic reasoning and self-critique, leading to significant performance improvements on the CoqStoq benchmark.

Contribution

It proposes reflection-based validation and proof plan-guided retrieval techniques to improve LLM-based proof agents, addressing key limitations in current systems.

Findings

ReCent-Prover achieves a 22.58% relative improvement in proved theorems over previous state-of-the-art.

Reflection with validation helps identify and filter out potential errors in tactics.

Retrieval conditioned on proof plans improves lemma and proof selection.

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.