IsabeLLM：自动定理证明在共识形式化验证中的应用

# IsabeLLM：自动化定理证明应用于共识的形式化验证
来源：https://arxiv.org/html/2606.18098  
William Knottenbelt  
帝国理工学院  
伦敦，英国  

###### 摘要  

人工智能的进步使得定理证明领域的人工智能成为形式化验证计算机系统的一种有前景的手段。传统上，形式化验证因所需专业知识和工作量巨大而仅用于安全关键系统，但人工智能能够自动化大量工作，使其更加普及。基于区块链的系统正日益流行，却经常成为恶意攻击的目标，导致巨额金融损失，这凸显了更好地验证这些系统并减轻漏洞的必要性。这些系统中最重要的组成部分之一是共识协议，它使节点在潜在对抗环境中能够达成一致决策。在本文中，我们改进了IsabeLLM，这是一款用于Isabelle的自动化定理证明工具。具体而言，我们实现了检索增强生成框架、错误追踪和反例生成，以向大语言模型提供改进的上下文。我们还实现了与最新版Isabelle和Sledgehammer的兼容性，以提高效率。我们比较了两个版本的IsabeLLM在完成比特币工作量证明共识验证方面的性能。

定理证明，形式化验证，区块链，共识，人工智能

††ccs：安全与隐私 逻辑与验证

## 1. 引言

区块链使得点对点数字交易无需可信中介即可进行。这之所以可能，完全是因为其共识协议，该协议允许系统中的节点即使在存在对手的情况下也能就区块链状态达成一致。因此，共识的设计和实现必须正确无误，以防止系统进入可能被对手利用的不可取状态。最著名的例子是比特币的工作量证明共识协议及其对51%攻击的敏感性——对手控制系统中大部分算力，从而有可能进行双重支付。此类攻击的臭名昭著的例子包括以太经典（CoinDesk, 2021 (https://arxiv.org/html/2606.18098#bib.bib4)）、比特币黄金（CoinDesk, 2020 (https://arxiv.org/html/2606.18098#bib.bib5)）和Vertcoin（CoinDesk, 2019 (https://arxiv.org/html/2606.18098#bib.bib6)），总损失超过3000万美元。

现代区块链系统的其他关键组件包括用于跨链数据传输的桥接协议和用于自动执行合约的智能合约。这些组件同样不乏漏洞，著名的例子包括Poly Network（路透社, 2021 (https://arxiv.org/html/2606.18098#bib.bib7)）、Wormhole Bridge（Investopedia, 2022 (https://arxiv.org/html/2606.18098#bib.bib8)）、币安智能链（Decrypt, 2024 (https://arxiv.org/html/2606.18098#bib.bib9)）和Qubit Finance（Chainalysis, 2023 (https://arxiv.org/html/2606.18098#bib.bib10)），总损失超过15亿美元。这些失败进一步强调了确保整个领域正确性的必要性。

形式化验证是将系统形式化并数学证明其正确性的过程。然而，由于需要大量精力和专业知识，它在软件开发过程中往往未被充分利用。尽管像以太坊基金会这样的组织积极资助该领域的形式化验证工作，但如前所述，巨额金融损失仍在继续。此外，区块链系统不能依赖传统的“测试与修补”模型来处理其共识协议，因为修补需要进行硬分叉，例如以太坊/以太经典分叉（CoinBase, 2016 (https://arxiv.org/html/2606.18098#bib.bib11)）。硬分叉具有破坏性和争议性，因为它们挑战了区块链的不可篡改性核心原则。此外，智能合约一旦部署在区块链上，通常无法修补，因为它们是不可变的（Investopedia, 2024 (https://arxiv.org/html/2606.18098#bib.bib12)），但也有少数例外（Alchemy, 2024 (https://arxiv.org/html/2606.18098#bib.bib13)）。这说明了形式化验证的必要性，因为它可用于“正确性自构造”（Bordis等人, 2023 (https://arxiv.org/html/2606.18098#bib.bib14)），并最大限度地减少昂贵的部署后修复需求。

近年来，人工智能领域取得了令人难以置信的进步，尤其是在大型语言模型方面，如OpenAI的ChatGPT和高飞的DeepSeek。这一进展为包括形式化验证在内的所有领域开辟了新的机遇。特别是，人工智能在定理证明方面已获得关注，并开始应用于纯数学陈述之外的程序验证。例如FVEL（Lin等人, 2024 (https://arxiv.org/html/2606.18098#bib.bib15)），它用于协助在Isabelle证明助手中自动验证C/C++程序。这降低了此类程序形式化验证的门槛，使其更易用且更省时。

在我们的原始论文中，我们提出了IsabeLLM（Jones和Knottenbelt, 2025 (https://arxiv.org/html/2606.18098#bib.bib59)），这是一个将Isabelle证明助手与大型语言模型相结合以协助和自动化证明的工具。我们通过使用它来证明比特币工作量证明共识协议的新模型的正确性，展示了IsabeLLM的有效性。

我们在原始论文的基础上，引入了IsabeLLM-RAG，这是IsabeLLM的改进版本。具体而言，我们进行了以下改进：

1. (1) 实现了一个基于(Jones和Marmsoler, 2024 (https://arxiv.org/html/2606.18098#bib.bib16))中二叉树模型证明的检索增强生成数据库，以提供改进的领域特定上下文。
2. (2) 实现了Nitpick反例生成器(Blanchette和Nipkow, 2010 (https://arxiv.org/html/2606.18098#bib.bib60))，以识别逻辑上错误的证明步骤。
3. (3) 实现了一个错误追踪，捕获LLM调用之间的所有修改，提供变更历史作为上下文，并突出显示哪些证明步骤已纠正且应保留。
4. (4) 与Isabelle 2025兼容，并进行了一般性效率改进。
5. (5) 将LLM从DeepSeek R1更换为DeepSeek R1T2 Chimera，以提高效率。

我们将在第5.3节 (https://arxiv.org/html/2606.18098#S5.SS3) 更详细地讨论这些变化。

## 2. 背景

### 2.1. 区块链

区块链是一种去中心化账本，允许多方无需可信中介即可进行交易，从而消除了信任需求。这只有通过区块链的共识协议才能实现，该协议允许所有方就区块链的当前状态及其上记录的交易达成一致。最流行的共识协议是比特币区块链使用的工作量证明，该区块链已记录约12亿笔交易(Blockchain.com, 2025 (https://arxiv.org/html/2606.18098#bib.bib19))，比特币市值约1.8万亿美元(CoinMarketCap, 2025 (https://arxiv.org/html/2606.18098#bib.bib18))。PoW的核心思想是最长的区块链是正确的，因为它假设系统中大多数计算能力是诚实的，因此应该能够比对手更快地解决哈希并添加区块(Nakamoto, 2008 (https://arxiv.org/html/2606.18098#bib.bib2))。

### 2.2. Isabelle

Isabelle是一个用Scala和ML编写的证明助手，使用高阶逻辑。它用于编写和验证形式化证明，由于这些证明的机械化，具有高保证性(Nipkow等人, 2002 (https://arxiv.org/html/2606.18098#bib.bib3))。Isabelle的Isar证明语言使得这些证明比传统的反复应用战术的定理证明方法更具可读性。Isabelle还利用像Sledgehammer这样的自动化工具，它使用外部自动定理证明器来帮助你完成证明。在证明助手之外，Scala库Scala-Isabelle提供了在Scala应用程序内与Isabelle进程交互的功能(Unruh, 2022 (https://arxiv.org/html/2606.18098#bib.bib20))。

### 2.3. 检索增强生成

检索增强生成是使用外部数据来提高LLM性能的技术。尽管LLM是非常优秀的通用工具，但它们常常在数据稀少的特定领域遇到困难，导致LLM产生幻觉并给出错误答案。RAG旨在通过提供领域特定数据的数据库来对抗这一问题，以帮助LLM获得更多上下文并理解问题。

RAG框架由检索机制和生成式LLM组成。数据首先被映射到一个向量空间，使得数据点越接近，它们就越相似。检索器在该向量空间中搜索，以找到与给定查询最相关的信息，然后将其包含在提供给LLM的提示中(Lewis等人, 2020 (https://arxiv.org/html/2606.18098#bib.bib56))。

在AI定理证明的背景下，RAG用于识别与当前试图证明的陈述相似的陈述。通过查看类似陈述过去是如何被证明的，它帮助LLM理解如何证明新陈述。基于RAG的技术已在Lean(Thakur等人, 2023 (https://arxiv.org/html/2606.18098#bib.bib57))和Isabelle(First等人, 2023 (https://arxiv.org/html/2606.18098#bib.bib58))中用于纯数学证明，但尚未在形式化验证的背景下使用。

## 3. 相关工作

在过去20年中，Isabelle被广泛用于进行众多验证。一些最著名的验证包括seL4微内核(Klein等人, 2010 (https://arxiv.org/html/2606.18098#bib.bib21))、ML编译器(Hupel和Nipkow, 2018 (https://arxiv.org/html/2606.18098#bib.bib22))，以及众多协议和程序验证(Gomes等人, 2017 (https://arxiv.org/html/2606.18098#bib.bib23); Foster等人, 2021 (https://arxiv.org/html/2606.18098#bib.bib24); Marić, 2010 (https://arxiv.org/html/2606.18098#bib.bib26))。在验证之外，Isabelle已被用于形式化大量在形式化证明档案库中可以找到的数学内容(Isabelle/HOL, 2004 (https://arxiv.org/html/2606.18098#bib.bib27))。AFP中最著名的形式化工作包括哥德尔不完备定理(Paulson, 2015 (https://arxiv.org/html/2606.18098#bib.bib28))、乔丹曲线定理(Thiemann和Yamada, 2016 (https://arxiv.org/html/2606.18098#bib.bib29))和拉姆齐定理(Paulson, 2004 (https://arxiv.org/html/2606.18098#bib.bib30))。近年来，Isabelle已被用于区块链系统的验证和形式化，包括以太坊虚拟机(Amani等人, 2018 (https://arxiv.org/html/2606.18098#bib.bib31))和验证Solidity智能合约的框架(Marmsoler和Brucker, 2021 (https://arxiv.org/html/2606.18098#bib.bib32))。

在Isabelle之外，各种其他定理证明器也被用于区块链领域的验证。举几个例子，Agda(Setzer, 2018 (https://arxiv.org/html/2606.18098#bib.bib35); Alhabardi等人, 2022 (https://arxiv.org/html/2606.18098#bib.bib33); Alhabardi和Setzer, 2023 (https://arxiv.org/html/2606.18098#bib.bib34))、Coq(Sun和Yu, 2020 (https://arxiv.org/html/2606.18098#bib.bib37); Yang等人, 2020 (https://arxiv.org/html/2606.18098#bib.bib36); Alturki等人, 2019 (https://arxiv.org/html/2606.18098#bib.bib38))和Lean(Nethermind, 2024 (https://arxiv.org/html/2606.18098#bib.bib40); Pusceddu和Bartoletti, 2024 (https://arxiv.org/html/2606.18098#bib.bib39))已被用于区块链的形式化。该领域也开始出现去中心化金融组件的形式化工作(Bartoletti等人, 2021 (https://arxiv.org/html/2606.18098#bib.bib43), 2022 (https://arxiv.org/html/2606.18098#bib.bib42); Bartoletti和Zunino, 2023 (https://arxiv.org/html/2606.18098#bib.bib41))，但尚未机械化。该领域的其他主要工作包括在K框架中形式化以太坊虚拟机(Hildenbrandt等人, 2018 (https://arxiv.org/html/2606.18098#bib.bib44))、用于半自动智能合约验证的Certora Prover(Certora, 2024 (https://arxiv.org/html/2606.18098#bib.bib45))，以及模糊测试工具Echidna(Grieco等人, 2020 (https://arxiv.org/html/2606.18098#bib.bib65))。最近，PropertyGPT(Liu等人, 2024 (https://arxiv.org/html/2606.18098#bib.bib66))使用在Certora审计报告上训练的LLM来形式化验证智能合约。在区块链系统中广泛使用的零知识证明电路也引起了形式分析的更大兴趣(Wen等人, 2024 (https://arxiv.org/html/2606.18098#bib.bib71))。

近年来，AI定理证明领域见证了证明助手重大数据集的发展，包括用于Isabelle的IsarStep和PISA(Li等人, 2020 (https://arxiv.org/html/2606.18098#bib.bib47); Jiang等人, 2021 (https://arxiv.org/html/2606.18098#bib.bib48))、用于Lean的LeanDojo(Yang等人, 2023 (https://arxiv.org/html/2606.18098#bib.bib49))，以及用于Coq的GamePad和CoqGym(Yang和Deng, 2019 (https://arxiv.org/html/2606.18098#bib.bib51))。利用这些数据集，开发了各种定理证明模型，包括LEGO-Prover(Wang等人, 2023 (https://arxiv.org/html/2606.18098#bib.bib52))、LISA(Jiang等人, 2021 (https://arxiv.org/html/2606.18098#bib.bib48))和DeepSeek-Prover(Xin等人, 2024 (https://arxiv.org/html/2606.18098#bib.bib53))。形式化验证领域的人工智能应用有限，前述FVEL(Lin等人, 2024 (https://arxiv.org/html/2606.18098#bib.bib15))是该领域的主要工作。至于区块链形式化验证中的人工智能，文献很少，仅有研究从自然语言提取智能合约规范(Leite等人, 2024 (https://arxiv.org/html/2606.18098#bib.bib54))。

## 4. 模型

我们的共识模型建立在先前工作(Jones和Marmsoler, 2024 (https://arxiv.org/html/2606.18098#bib.bib16))的基础上，将区块链结构从二叉树推广到n叉树。这一扩展使得模型能够考虑任意数量的分叉，反映了区块链更现实的视图。我们证明了在多数诚实网络中，使用比特币主干协议中概述的公共前缀和链质量属性(Garay等人, 2015 (https://arxiv.org/html/2606.18098#bib.bib1))可以维持共识，这些属性中有更详细的讨论。我们假设网络中的多数节点是诚实的且同步，意味着网络中大多数计算能力是诚实的，并且每个人都共享相同的区块链视图。此外，我们假设区块难度保持不变，将比特币的最重链规则简化为最长链规则。我们做出这些假设是为了降低模型的复杂性，并避免切换到计算模型。尽管此类模型提供了更现实的验证，但本研究的目标是评估LLM在验证中的有效性。该模型为未来更复杂的验证提供了足够的基础。