SolBehave：评估 LLM 生成的智能合约的行为正确性

大型语言模型日益生成 Solidity 智能合约，而这类合约一旦部署便永远无法修补，使单个潜在缺陷永久存在并可被利用。然而，当前的评估大多只考察生成的代码能否编译。我们提出 SolBehave，这是一项用于大规模评估模型生成合约正确性的基准测试，超越了临时性单元测试。针对 250 个真实且可复现的 Ethereum 合约，我们采用三种互补的行为保真度测试：差分模糊测试、历史交易重放，以及作为核心贡献的、由动态条件响应（DCR）图引导的合成交易重放；该图枚举了合法函数调用序列的空间。差分模糊测试将每个生成函数与原始函数在自动生成的输入上进行比较；历史重放则根据合约实际上在链上接收过的交易，对整个合约进行比较；DCR 引导的重放则依据符合其预期用法的调用序列进行比较，其中包括从未在链上发生过的调用顺序。我们在进行一轮自动修复后，评估了七个最先进的开放权重模型。编译成功率介于 26.4% 和 92.7% 之间，但在差分模糊测试中，汇总各模型和样本后，所有能够编译的生成函数体中只有 31.4% 与原始函数等价。在合约层面，出现偏离是常态而非例外：对于七个模型中的六个，在历史重放下，能够编译的生成合约中有 13% 至 31% 与原始合约发生偏离；在 DCR 引导的重放下，这一比例为 13% 至 44%；只有 Gemma-4-31B 在两种测试下的偏离率均低于 3%。因此，编译成功是正确性的必要条件，但远非充分条件。