Vibe Coding an LLM-powered Theorem Prover
作者: Zhe Hou
分类: cs.AI, cs.LO
发布日期: 2026-01-08
🔗 代码/项目: GITHUB
💡 一句话要点
Isabellm：一种基于LLM的Isabelle/HOL定理证明器，实现全自动证明合成
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 定理证明 大型语言模型 形式化验证 Isabelle/HOL 自动化推理
📋 核心要点
- 现有的定理证明自动化工具在复杂定理的证明上存在局限性，难以充分利用大规模知识。
- Isabellm利用LLM的强大推理和代码生成能力，结合逐步证明和高层规划，实现更有效的定理证明。
- 实验表明，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）的强大代码生成和推理能力，引导定理证明过程。通过LLM生成候选证明步骤，并由Isabelle/HOL验证其正确性，从而在保证正确性的前提下，加速证明搜索过程。同时，引入高层证明规划器，生成结构化的证明纲要，进一步提高证明效率。
技术框架：Isabellm的整体架构包含两个主要模块：逐步证明器和高层证明规划器。逐步证明器利用LLM生成证明命令，并由Isabelle验证。高层证明规划器生成Isar证明纲要，并尝试填充和修复剩余的空白。此外，框架还包括光束搜索、策略重排序模型、前提选择模型和反例引导的证明修复机制。
关键创新：最重要的技术创新点在于将LLM与传统的定理证明器相结合，利用LLM的生成能力和Isabelle的验证能力，实现了一种新型的定理证明方法。与现有方法相比，Isabellm能够更有效地搜索证明空间，并具有更强的适应性和灵活性。
关键设计：框架使用了多种技术细节来提升性能。例如，使用光束搜索来探索不同的证明策略；使用机器学习和强化学习模型来对策略进行重排序；使用小型Transformer模型进行前提选择，以减少搜索空间；使用微型RAG技术来检索相关的Isar证明；使用反例引导的证明修复机制来纠正证明中的错误。具体LLM的选择包括GPT系列、Gemini和Claude等，并根据实际效果进行调整。
📊 实验亮点
Isabellm成功证明了某些传统自动化工具（包括Sledgehammer）无法解决的Isabelle/HOL引理，展示了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