可访问的智能合约验证：利用驯服的大语言模型合成形式化模型
Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs
AI总结：
本文提出一种利用大语言模型自动合成形式化模型的方法，通过转译、填空和迭代修复三阶段流程，显著降低智能合约形式化验证所需的时间和专业知识门槛。
摘要：
当区块链系统被称为无需信任时，这实际上意味着所有信任都被置于软件之中。因此，有强烈的动机确保区块链软件的正确性——这里的漏洞会造成数百万美元的损失并破坏业务。建立软件正确性最强大的方法之一是使用形式化方法。然而，基于形式化方法的方法在成功运用所需的时间和专业知识方面带来了显著的负担。我们的工作通过自动化创建形式化模型——软件系统的数学抽象——来解决这一关键缺点，这通常是采用形式化方法时的核心任务。我们分三个阶段执行模型合成：首先将代码转译成模型存根；然后使用大语言模型（LLM）“填空”；最后，在语法和语义层面迭代修复生成的模型。通过这种方式，我们显著减少了创建形式化模型所需的时间，并提高了依赖这些模型的宝贵软件验证方法的可访问性。我们工作的实际背景是减少使用形式化模型对智能合约进行正确性审计的时间价值。
英文摘要：
When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software is correct -- vulnerabilities here cost millions and break businesses. One of the most powerful ways of establishing software correctness is by using formal methods. Approaches based on formal methods, however, induce a significant overhead in terms of time and expertise required to successfully employ them. Our work addresses this critical disadvantage by automating the creation of a formal model -- a mathematical abstraction of the software system -- which is often a core task when employing formal methods. We perform model synthesis in three phases: we first transpile the code into model stubs; then we "fill in the blanks" using a large language model (LLM); finally, we iteratively repair the generated model, on both syntactical and semantical level. In this way, we significantly reduce the amount of time necessary to create formal models and increase accessibility of valuable software verification methods that rely on them. The practical context of our work was reducing the time-to-value of using formal models for correctness audits of smart contracts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
