Vibe Coding an LLM-powered Theorem Prover

📄 arXiv: 2601.04653v1 📥 PDF

作者: Zhe Hou

分类: cs.AI, cs.LO

发布日期: 2026-01-08

🔗 代码/项目: GITHUB

💡 一句话要点

Isabellm：一种基于LLM的Isabelle/HOL定理证明器，实现全自动证明合成

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 定理证明 大型语言模型 自动化 形式化验证 Isabelle/HOL

📋 核心要点

  1. 现有定理证明器在自动化方面存在局限性，难以处理复杂逻辑推理，需要人工干预。
  2. Isabellm利用LLM的强大推理能力，结合逐步证明和高层规划，实现自动化的定理证明。
  3. 实验表明，Isabellm能够证明一些传统方法无法解决的引理，验证了LLM在定理证明中的潜力。

📝 摘要（中文）

本文提出Isabellm，一个由大型语言模型（LLM）驱动的Isabelle/HOL定理证明器，能够执行全自动的证明合成。Isabellm可与Ollama上的任何本地LLM以及Gemini CLI等API协同工作，并且被设计为可在消费级计算机上运行。该系统结合了一个逐步证明器（利用LLM提出由Isabelle验证的证明命令，并在有界搜索循环中进行搜索）和一个更高层次的证明规划器（生成结构化的Isar纲要并尝试填补和修复剩余的空白）。该框架包括用于策略的光束搜索、策略重排序的机器学习和强化学习模型、使用小型Transformer模型进行前提选择、从AFP构建的Isar证明的微型RAG，以及反例引导的证明修复。所有代码均由GPT 4.1 - 5.2、Gemini 3 Pro和Claude 4.5实现。实验表明，Isabellm可以证明某些击败Isabelle标准自动化（包括Sledgehammer）的引理，证明了LLM引导的证明搜索的实际价值。同时，我们发现即使是最先进的LLM，如GPT 5.2 Extended Thinking和Gemini 3 Pro，也难以可靠地实现具有复杂算法设计的预期填充和修复机制，突显了LLM代码生成和推理方面的根本挑战。

🔬 方法详解

问题定义：论文旨在解决Isabelle/HOL定理证明的自动化问题。现有的自动化工具，如Sledgehammer，在处理复杂的定理证明时能力有限，需要人工干预。这限制了定理证明在更广泛领域的应用。

核心思路：论文的核心思路是利用大型语言模型（LLM）的强大推理和代码生成能力，构建一个自动化的定理证明器。通过将证明过程分解为逐步的命令生成和高层次的规划，结合多种技术手段，提高证明的成功率和效率。

技术框架：Isabellm的整体架构包含两个主要模块：逐步证明器和高层证明规划器。逐步证明器使用LLM生成Isabelle证明命令，并由Isabelle验证。高层证明规划器生成结构化的Isar纲要，并尝试填补和修复剩余的空白。此外，框架还包括策略光束搜索、策略重排序模型、前提选择模型、微型RAG和反例引导的证明修复等组件。

关键创新：该论文的关键创新在于将LLM应用于定理证明领域，并设计了一个结合逐步证明和高层规划的框架。通过利用LLM的推理能力和代码生成能力，实现了自动化的定理证明，并能够解决一些传统方法无法解决的问题。微型RAG技术也提升了系统对相关证明的检索能力。

关键设计：策略光束搜索用于探索不同的证明策略，策略重排序模型用于选择更有效的策略。前提选择模型使用小型Transformer模型，用于选择相关的引理和定理。微型RAG技术用于从AFP（Archive of Formal Proofs）中检索相关的Isar证明。反例引导的证明修复用于根据反例信息修复错误的证明。

📊 实验亮点

Isabellm能够证明一些Isabelle标准自动化工具（包括Sledgehammer）无法解决的引理，证明了LLM引导的证明搜索的有效性。尽管如此，实验也表明，即使是最先进的LLM在实现复杂的算法设计时仍然面临挑战，这突显了LLM代码生成和推理方面的局限性。

🎯 应用场景

Isabellm的应用场景包括形式化验证、软件可靠性验证、数学定理证明等领域。该研究的实际价值在于提高定理证明的自动化程度，降低人工干预的需求，从而加速相关领域的研究和应用。未来，该技术有望应用于更复杂的系统验证和数学问题的解决。

📄 摘要（原文）

We present Isabellm, an LLM-powered theorem prover for Isabelle/HOL that performs fully automatic proof synthesis. Isabellm works with any local LLM on Ollama and APIs such as Gemini CLI, and it is designed to run on consumer grade computers. The system combines a stepwise prover, which uses large language models to propose proof commands validated by Isabelle in a bounded search loop, with a higher-level proof planner that generates structured Isar outlines and attempts to fill and repair remaining gaps. The framework includes beam search for tactics, tactics reranker ML and RL models, premise selection with small transformer models, micro-RAG for Isar proofs built from AFP, and counter-example guided proof repair. All the code is implemented by GPT 4.1 - 5.2, Gemini 3 Pro, and Claude 4.5. Empirically, Isabellm can prove certain lemmas that defeat Isabelle's standard automation, including Sledgehammer, demonstrating the practical value of LLM-guided proof search. At the same time, we find that even state-of-the-art LLMs, such as GPT 5.2 Extended Thinking and Gemini 3 Pro struggle to reliably implement the intended fill-and-repair mechanisms with complex algorithmic designs, highlighting fundamental challenges in LLM code generation and reasoning. The code of Isabellm is available at https://github.com/zhehou/llm-isabelle