HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

TL;DR

HybridProver tackles the challenge of automated formal proof by unifying two LLM-driven proving paradigms—whole-proof synthesis and tactic-based refinement—through mechanically generated proof sketches that bridge planning and detailed steps. Implemented for Isabelle/HOL, it employs a dual-model workflow and dataset optimization to train specialized LLMs, augmented by Sledgehammer to boost premise selection. On miniF2F, it sets a new state-of-the-art for Isabelle proofs, demonstrating that combining high-level proof planning with stepwise refinement yields substantial gains, supported by targeted ablations on data quality and sampling diversity. The work provides open-source datasets, code, and models, and outlines directions for stronger proof-search integration, extended pretraining, and reinforcement learning to further advance automated theorem proving.

Abstract

Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theorem provers. Recent advancements in large language models (LLMs) offer new opportunities for automated theorem proving. Two promising approaches are generating tactics step by step and generating a whole proof directly with an LLM. However, existing work makes no attempt to combine the two approaches. In this work, we introduce HybridProver, a dual-model proof synthesis framework that combines tactic-based generation and whole-proof synthesis to harness the benefits of both approaches. HybridProver generates whole proof candidates for evaluation directly, then extracts proof sketches from those candidates. It then uses a tactic-based generation model that integrates automated tools to complete the sketches via stepwise refinement. We implement HybridProver for the Isabelle theorem prover and fine-tune LLMs on our optimized Isabelle datasets. Evaluation on the miniF2F dataset illustrates HybridProver's effectiveness. We achieve a 59.4% success rate on miniF2F, where the previous SOTA is 56.1%. Our ablation studies show that this SOTA result is attributable to combining whole-proof and tactic-based generation. Additionally, we show how the dataset quality, training parameters, and sampling diversity affect the final result during automated theorem proving with LLMs. All of our code, datasets, and LLMs are open source.

Figures (1)

• Figure 1: HybridProver Framework Overview