让 LLM 证明解释器与语义一致

Ship Your Interpreter

随着 LLM 在发现软件漏洞方面能力日益增强，构建可验证软件变得至关重要。我们尝试让 LLM 为小型语言 WHILE 编写形式语义，并利用 Lean 证明该语义与编译后的解释器二进制文件行为完全一致。实验发现，即使语义通过了所有常规测试，仍可能因实现细节（如缓冲区限制）而存在偏差。通过‘发布你的解释器’这一思路，我们将解释器本身作为验证基准，确保生成的数学规则能精准描述程序运行行为，为大规模软件验证提供了新路径。