用AI自动证明技术验证比特币共识协议，提升安全验证效率。
IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus
- 引入检索增强生成与错误追踪，提升大模型上下文理解能力
- 新版本IsabeLLM在比特币PoW验证中成功率显著提高
- 适合形式化验证、区块链安全研究者快速上手
人工智能在定理证明领域的进展使形式化验证计算机系统成为可能。传统形式化验证因需大量专业知识和精力而局限于高安全性系统，而AI可大幅自动化该过程，降低门槛。区块链系统日益普及且常遭恶意攻击，导致巨额损失，亟需加强验证以消除漏洞。共识协议是区块链核心，确保节点在对抗环境下达成一致。本文改进了Isabelle中的自动化定理证明工具IsabeLLM，引入检索增强生成框架、错误追踪及反例生成机制，增强大语言模型的上下文信息；同时兼容最新版Isabelle与Sledgehammer，提升运行效率。通过对比两个版本IsabeLLM在完成比特币工作量证明共识验证任务中的表现，验证了改进的有效性。
原文摘要 · Abstract (English)
Advances in Artificial Intelligence (AI) have led AI for Theorem Proving to become a promising means of formally verifying computer systems. Whilst formal verification is traditionally reserved for safety-critical systems due to the required amount of expertise and effort, AI can help to automate a large amount of this workload and make it far more accessible. Blockchain-based systems are becoming increasingly popular and are frequently targeted by malicious actors, often resulting in huge financial losses, highlighting the need to better verify these systems and mitigate vulnerabilities. Arguably the most important component of these systems is the consensus protocol, which allows nodes to agree on decisions in a potentially adversarial environment. In this paper, we improve upon IsabeLLM, the automated theorem proving tool in Isabelle. Namely, we implement a Retrieval-Augmented Generation framework, Error tracing and counterexample generation for improved context supplied to the Large Language Model. Compatibility with the latest version of Isabelle and Sledgehammer is also implemented for improved efficiency. We compare the performance of the two versions of IsabeLLM in their ability to complete the verification of Bitcoin's Proof of Work consensus.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。