核心发现

1. 概念理解缺陷

   • 模型无法有效推理合约所有权、重入攻击、费用分配等高级概念
   • 即使能自然语言描述重入攻击，Codex仍无法将其转化为实际分析能力
   • GPT-4对Solidity的分析能力虽有提升，但仍存在跨函数重入检测等关键缺陷

2. 工具链缺失

   • 缺乏处理不确定性的类型系统和开发库
   • 提示工程调试工具严重不足（如缺乏提示质量评估体系）
   • 现有生态中微软Infer.NET是少数支持概率编程的框架

3. 技术局限性

   • 小规模测试成功率为6/7（所有权检测），但扩展到300+行代码时出现15个误报
   • 对条件语句（==, <, >）的推理能力薄弱，易受变量命名干扰
   • 整数溢出检测在11个小样本中成功10例，但在5个真实合约中产生6个误报

定制化框架设计

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

# 示例：所有权检测提示链配置
[[questions]]
name = "can-change"
query = "能否通过调用`{{ contract.name }}`合约函数修改`{{ contract | owner_variable }}`变量？逐步思考后回答'是'/'否'/'未知'"
is_decision = true

[[questions]]
name = "who-can-call"
runtime_condition = "questions['can-change'].is_affirmative()"
query = """所有权推理步骤：
1) 详细分析函数代码
2) 逐步论证调用权限"""

性能对比数据

未来展望

• GPT-4大上下文窗口可能改善复杂任务处理能力
• LangChain等开源工具正在填补LLM集成工具链空白
• 概率编程语言的发展将关键性提升不确定性处理能力

实验表明：当Codex分析无现有工具的语言时，其"不完美但存在"的分析价值可能远超空白状态，但Solidity领域已有成熟静态分析工具作为更高基准。

完整技术细节及测试案例参见Trail of Bits官方报告。团队将持续探索LLM在自动生成审计文档等辅助场景的应用。