可信软件项目生成：交互式定理证明器的案例研究

根据自然语言需求生成代码已成为LLM辅助软件开发的主要途径。尽管 LLM 可以成功完成小型编程任务，但生成整个复杂项目仍然不可靠，因为细微的错误可能会在编译和测试中幸存下来。经过验证的编程可以通过要求生成的实现满足机器检查的规范来降低这种风险。现有的探索主要针对面向验证的语言和工具链，例如 Dafny 和 Frama-C，但利用这些系统直接生成项目规模的验证代码仍然很困难。本文研究交互式定理证明器（ITP）是否可以支持大规模软件生成。由于 ITP 处理纯总体功能，但不处理 I/O 等效果，因此我们的代理将有效代码与纯逻辑分开：它用目标语言实现效果，证明 ITP 中的纯逻辑，并将其提取以集成到最终项目中。我们通过为非特权 RISC-V RV32I 基础的所有 47 条指令全自动开发 CPU 解释器来研究这条路线：提供需求后，无需人工干预合成、证明修复、提取或集成。以 Rocq 作为后端，代理在 30 分钟内完成了该项目，生成了 1,859 行经过验证的 Rocq 并提取了 2,848 行 C++。生成的解释器通过了涵盖 47 条指令的所有 265 个 LLM 生成的测试，并在 12 小时的 AFL++ 模糊测试期间表现出零崩溃和零挂起。在相同配置下，基于Dafny的后端无法完成验证。我们的观察是，当证明尝试失败时，Rocq 会公开具体的证明状态，为代理提供可操作的修复反馈。这些结果提供了经验证据，表明基于 ITP 的验证编程是 LLM 生成的软件项目的可行途径。