跳转至

HybridProver：通过大模型驱动的证明合成与精炼增强定理证明

文章背景与核心概要

形式化方法通过严格的数学验证确保关键系统的可靠性，但其广泛应用一直受限于人工构建证明时的高昂劳动成本。虽然大语言模型（LLM）通过逐步的策略生成和完整证明合成，为自动定理证明开辟了有前景的途径，但现有方法通常将这两种范式孤立开来。

为了弥合这一差距，本文推出了 HybridProver，这是一个统一框架，它以“证明草图（proof sketches）”作为中间表示，将完整证明合成与策略生成结合起来。HybridProver 在 Isabelle/HOL 中实现，并结合了经过后训练的 7B 规模大语言模型，在 miniF2F Isabelle 基准测试中取得了 73.8% 的最先进（SOTA）成功率，证明了轻量级模型无需依赖庞大的 LLM 架构也能高效生成复杂证明。

执行摘要 (Executive Summary)

Formal methods are essential for guaranteeing the reliability of critical systems through rigorous mathematical verification; however, their practical adoption remains bottlenecked by the labor-intensive nature of manual proof construction. While Large Language Models (LLMs) have introduced promising paths toward automated theorem proving via stepwise tactic-based generation and whole-proof synthesis, existing approaches usually isolate these two paradigms.

HybridProver bridges this gap by introducing a unified framework that combines whole-proof synthesis and tactic-based generation using proof sketches as an intermediate representation. Implemented in Isabelle/HOL alongside post-trained 7B-scale LLMs, HybridProver achieves a state-of-the-art 73.8% success rate on the miniF2F Isabelle benchmark, proving that lightweight models can effectively generate complex proofs without relying on massive LLM architectures.

论文元数据 (Paper Metadata)

Field Details
Title HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
Authors Jilin Hu, Jianyu Zhang, Yongwang Zhao, Talia Ringer
Subjects Formal Languages and Automata Theory (cs.FL); Artificial Intelligence (cs.AI); Software Engineering (cs.SE)
Primary Venue / Status Accepted to EMNLP Findings 2026
Identifiers arXiv:2505.15740 [cs.FL]
DOI: 10.48550/arXiv.2505.15740
Submission History v1: May 21, 2025
v2: August 27, 2026

摘要 (Abstract)

Formal methods play a crucial role in ensuring the reliability of critical systems through rigorous mathematical verification. However, their adoption remains limited due to the labor-intensive nature of manual proof construction. Recent advances in large language models (LLMs) have opened new opportunities for automated theorem proving. Two main paradigms have emerged: stepwise tactic-based generation and whole-proof synthesis. While both approaches have complementary strengths, existing work largely treats them in isolation.

In this work, we propose HybridProver, a unified framework that integrates whole-proof synthesis and tactic-based generation through proof sketches as an intermediate representation. This design enables the reuse of partially correct proof structures while effectively combining high-level planning with fine-grained reasoning. We implement HybridProver in Isabelle/HOL and post-train two 7B-scale LLMs on our optimized Isabelle datasets. Experiments on the miniF2F Isabelle benchmark achieved a 73.8% success rate and improved upon the previous state of the art (61.9%), demonstrating that lightweight models, when combined with our approach, can effectively generate Isabelle/HOL proofs without relying on very large LLMs. Ablation studies further analyze the impact of dataset quality, training configurations, and sampling strategies on proof generation.

核心贡献与架构 (Key Contributions & Architecture)

  • Unified Framework: Successfully merges high-level proof planning (whole-proof synthesis) with low-level execution (tactic-based generation).
  • Proof Sketches: Employs proof sketches as an intermediate representation to seamlessly reuse partially correct structural logic.
  • Lightweight Efficiency: Demonstrates that 7B-parameter models can outperform prior benchmarks by achieving a 73.8% success rate on miniF2F Isabelle (surpassing the previous SOTA of 61.9%).
  • Rigorous Analysis: Conducts extensive ablation studies covering dataset quality, training setups, and sampling strategies.

访问与资源 (Access & Resources)