AWS 用 Lean 4 数学证明 Aurora Grover 数据修复协议的鲁棒性

Amazon Science·2026-11-02 23:45· 1 小时前AI 评分51

在 Lean4 中证明 AWS Aurora 数据分发协议的鲁棒性

AI 导读

Amazon 自动推理团队用 Lean 4 形式化并证明了 AWS Aurora 分布式协议 Grover 的核心数据修复与迁移协议，证明其满足默认六副本容忍任意两节点同时故障的承诺，且证明不限定副本数。团队让 LLM 迭代提出规范并尝试证明或反例，过程中发现并记录了文档中的隐性假设与歧义，若照文档实现可能导致数据丢失；两种风格的协议形式也被证明等价，便于专家审阅。

正文 · 原文

我们的许多数字数据——家庭照片、小说草稿、病历——都以电信号模式存在于金属盒子中，而这些盒子可能遭遇电网停电以及自然和人为灾害。任何一个盒子都有高得令人难以接受的故障概率，因此我们会把数据复制到位于不同地理区域的多个金属盒子中。冗余保护数据。但如果我们想修改数据——编辑那部小说，或向病历中添加一项新的血液检测——该怎么办？我们把期望的修改发送给所有盒子，但不能假定通信可靠：某些盒子收到的修改可能有缺失；某些盒子可能错过其他盒子的更新；不同盒子可能在不同时间得知某项修改。保持冗余数据同步且最新，需要一场精细的分布式更新之舞。AWS Aurora 的分布式协议 Grover 为数据库存储编排了这场舞蹈。例如，Grover 的默认设置具有六重冗余，并承诺能承受六个盒子中任意两个同时发生故障。在 Amazon 的 Automated Reasoning 团队中，我们已用数学方法证明，Grover 的核心数据修复与迁移协议兑现了这一承诺。该证明就像数独解答一样，可以在不信任发现过程（在我们的案例中，是由大语言模型生成的）的情况下进行检查。为了实现自动证明检查，我们用 Lean 4 表达我们的断言及其证明；Lean 4 是一种用于以数学严谨性表达和证明断言的语言与工具包。第 1 步：在 Lean 4 中初步规范 Grover 协议 我们的第一个挑战是在 Lean 4 中精确定义 Grover 协议。我们手写了一个 Lean 4 模板，该模板足够通用，适用于任何分布式协议，然后让 LLM 根据现有的自然语言文档为 Grover 填充该模板。在此过程中，我们在 Grover 文档中发现了许多歧义和笔误；如果按字面理解，这些内容描述的协议可能会丢失数据。一个例子是一个隐藏假设，当 Grover 扩展到高于默认冗余度时，违反该假设有时会导致数据丢失。文档作者知道 Grover 做出了该假设，但忘记记录它。我们的工作揭示了此类安全要求，并将其记录下来，供未来维护和修改 Grover 的人员使用。因此，形式化不仅产生了一个经过验证的参考算法，可作为未来实现的基础，还帮助改进了现有文档。第 2 步：协同演化证明与规范 使用 Grover 协议的 Lean 4 版本，我们证明了：一旦某条数据被安全存储，它就会在之后每一轮修复和重新洗牌中保持安全存储。该证明不假定盒子的特定数量，因此涵盖了 Grover 运行时的任何冗余设置，而不仅是默认的六重。我们使用 LLM 迭代提出协议的 Lean 4 规范，并使用同一个 LLM 为每个提案尝试证明或反例。搜索通常会产生反例，在这种情况下，我们对规范做出最小且最忠实于文档的修改以排除该反例，然后重复该过程。我们最终收敛到一个形式化协议及其正确性证明，二者均在 Lean 4 中。为了检查每一处对文档的偏离确实必要，我们自动构造反例，表明省略任何单处修改都会破坏相关定理。最后，我们将形式化协议从显式风格——自动推理最容易处理的风格，完整列出每一次转换——简化为人类可读的风格，一种我们为分布式协议设计的紧凑记法，整个协议可放入一个专家能阅读的文件中。我们形式化证明了两个版本等价。这使 Grover 团队的人类专家能够作为 ongoing work 检查所证明的协议确实就是预期协议。我们的概念验证展示了一种新的工作方法，可能加速 Amazon 在分布式协议方面更广泛的工作，并强化最终结果。借助自动正确性检查器，开发者可以积极优化并针对复杂的客户用途进行定制，而不必担心新的复杂性会引入缺陷。如果我们成功将自动推理方法应用于通用协议，那么开发者增强分布式协议的速度将取决于他们的增强意愿，而不是他们的风险承受意愿。致谢：Alexey Gotsman、Mark Tuttle

来源：Amazon Science · amazon.science