用 Vibe Coding 构建 LLM 驱动的定理证明器

我们提出 Isabellm，一个面向 Isabelle/HOL 的 LLM 驱动定理证明器，可执行全自动证明合成。Isabellm 可与 Ollama 上的任何本地 LLM 以及 Gemini CLI 等 API 协作，并设计为在消费级计算机上运行。该系统将逐步证明器与更高层的证明规划器相结合：前者使用大语言模型在有界搜索循环中提出经 Isabelle 验证的证明命令，后者生成结构化的 Isar 大纲并尝试填补与修复剩余缺口。该框架包括用于战术（tactics）的束搜索、用于战术重排的 ML 与 RL 模型、使用小型 transformer 模型的前提选择、基于 AFP 构建的面向 Isar 证明的微 RAG，以及反例引导的证明修复。所有代码均由 GPT 4.1 - 5.2、Gemini 3 Pro 和 Claude 4.5 实现。实证上，Isabellm 能够证明某些击败 Isabelle 标准自动化（包括 Sledgehammer）的引理，展示了 LLM 引导证明搜索的实用价值。与此同时，我们发现即使是 GPT 5.2 Extended Thinking 和 Gemini 3 Pro 等最先进的 LLM，也难以可靠地实现具有复杂算法设计的预期填充与修复机制，凸显了 LLM 代码生成与推理方面的根本性挑战。Isabellm 的代码可在 https://github.com/zhehou/llm-isabelle 获取。