伊莎贝尔漂流开发项目的合同意识救援：双罐案例研究

大语言模型 可以为交互式定理证明者提出证明，但成功的构建并不表明保留了周围的验证任务。我们在 Isabelle 开发的采样数据双罐控制器中研究了这个问题。这项工作从 9 个理论和 10 个未完成的任务开始，发展到 16 个理论构建，没有抱歉，哎呀，添加公理化或预言机使用，并积累了 23 个稳定的证明状态和 36 个损坏的证明状态。一项回顾性审计发现，100 份原始声明中有 16 份发生了重大变化，其中包括在结论中假设了四项要求中的三项的端到端保证定理被削弱。我们使用 CAPRI（一种合同感知的证明修复工具），通过将 Isabelle 接受与根据机器可读编辑合同对存储库更改进行独立检查相结合来管理重建。重建履行了原始九理论结构中的所有十项范围义务。合著者的二次重播重现了 R10 构建、合同检查、控制测试和主要审计结果；独立复制仍然是未来的工作。操作性端到端验证仍然不完整：我们仍然需要将操作执行连接到重建的定量追踪合约，这是一项需要扩展合约的任务。