SolBehave: Evaluating the Behavioural Correctness of LLM-Generated Smart Contracts
作者: Giovanni Pio Delvecchio, Stefano Fantazzini, Giacomo Frisoni, Gianluca Moro, Lorenzo Bacchiani, Mario Bravetti, Thomas Troels Hildebrandt
分类: cs.SE, cs.AI
发布日期: 2026-10-13
💡 一句话要点
提出SolBehave以评估LLM生成智能合约的行为正确性
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 智能合约 行为正确性 大型语言模型 区块链安全 自动化测试 合约评估
📋 核心要点
- 现有方法主要关注生成代码的编译成功，未能有效评估智能合约的行为正确性。
- 本文提出SolBehave基准，通过差异模糊测试、历史重放和DCR引导的合成重放，全面评估合约的行为忠实性。
- 实验结果显示，编译成功率高，但在行为测试中，生成合约与原始合约的等价性普遍较低，揭示了现有生成模型的局限性。
📝 摘要（中文）
随着大型语言模型（LLM）生成的Solidity智能合约越来越多，这些合约一旦部署便无法修补，潜在的错误可能导致严重的安全隐患。然而，现有评估方法主要关注代码是否能编译。本文提出了SolBehave，一个用于大规模评估模型生成合约正确性的基准，超越了传统的单元测试。我们在250个真实的以太坊合约上应用了三种互补的行为忠实性测试：差异模糊测试、历史交易重放，以及核心贡献的动态条件响应（DCR）图引导的合成交易重放。实验结果显示，编译成功率在26.4%到92.7%之间，但在差异模糊测试下，只有31.4%的生成函数体与原始函数等价，合约级别的偏差普遍存在。
🔬 方法详解
问题定义：本文旨在解决大型语言模型生成的智能合约在行为正确性评估上的不足，现有方法仅关注编译成功，未能识别潜在的逻辑错误和安全隐患。
核心思路：提出SolBehave基准，通过三种互补的测试方法，全面评估生成合约的行为忠实性，确保合约在实际使用中的安全性和可靠性。
技术框架：整体流程包括三个主要模块：差异模糊测试、历史交易重放和DCR引导的合成交易重放。每个模块针对合约的不同方面进行评估，确保全面覆盖。
关键创新：核心创新在于引入DCR图，该图枚举合法的函数调用序列，使得合成交易重放能够更准确地模拟合约的预期使用场景，从而提高评估的有效性。
关键设计：在实验中，使用了多种开源模型进行评估，设置了不同的输入生成策略，并对比了编译成功率与行为等价性，确保了实验结果的可靠性。实验还包括对模型进行自动修复的步骤，以评估修复后的性能提升。
🖼️ 关键图片
📊 实验亮点
实验结果表明，编译成功率在26.4%到92.7%之间，但在差异模糊测试中，只有31.4%的生成函数体与原始函数等价。合约级别的偏差普遍存在，六个模型中有13%到31%的合约在历史重放中表现出偏差，DCR引导重放的偏差率更高，达到13%到44%。
🎯 应用场景
该研究的潜在应用领域包括智能合约的自动生成与验证、区块链安全性评估以及智能合约开发工具的改进。通过提供更为严格的行为评估标准，SolBehave能够帮助开发者在合约部署前识别潜在的安全风险，从而提高区块链应用的整体安全性和可靠性。
📄 摘要（原文）
Large language models increasingly generate Solidity smart contracts that, once deployed, can never be patched, making a single latent fault permanent and exploitable. Yet current evaluations mostly ask only whether generated code compiles. We introduce SolBehave, a benchmark for evaluating the correctness of model-generated contracts at scale, moving beyond ad hoc unit tests. Across 250 real, reproducible Ethereum contracts, we apply three complementary tests of behavioural fidelity: differential fuzzing, historical-transaction replay, and, as our core contribution, synthetic-transaction replay guided by a Dynamic Condition Response (DCR) graph that enumerates the space of legitimate function-call sequences. Differential fuzzing compares each generated function with the original on automatically generated inputs; historical replay compares the whole contract on the transactions it actually received on-chain; DCR-guided replay compares it on sequences of calls that follow its intended usage, including orderings that never occurred on-chain. We evaluate seven state-of-the-art open-weight models after one round of automated repair. Compilation success ranges from 26.4% to 92.7%, but under differential fuzzing only 31.4% of all generated function bodies that compile, pooled over models and samples, are equivalent to the original. Divergence at the contract level is the norm rather than the exception: for six of the seven models, between 13% and 31% of the generated contracts that compile diverge from the original under historical replay, and between 13% and 44% under DCR-guided replay; only Gemma-4-31B stays below 3% on both. Compilation is therefore a necessary condition for correctness and far from a sufficient one.