💻 computer science

Formal Verification of Minimax Algorithms

本文利用 Dafny 形式化验证系统，对包含 Alpha-Beta 剪枝和置换表的 Minimax 搜索算法进行了严谨的正确性验证，提出了一种基于见证的深度限制搜索正确性判据，并分别完成了对一种变体的完全机械化证明以及对另一种变体的反例构造。

原作者： Wieger Wesselink, Kees Huizing, Huub van de Wetering

发布于 2026-04-23

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Wieger Wesselink, Kees Huizing, Huub van de Wetering

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文讲述了一个关于如何确保电脑下棋程序（游戏引擎）“不耍赖”且“算得对”的故事。

想象一下，你正在和一个超级聪明的机器人下棋。机器人为了赢你，会在脑海里模拟成千上万种未来的走法。它使用的核心算法叫“极小化极大”（Minimax），就像是在一棵巨大的“决策树”上爬来爬去，寻找对自己最有利的路径。

但是，这棵树太大了，机器人记不住所有东西，也跑不完所有路。所以，它用了两个“作弊”技巧来加速：

剪枝（Alpha-Beta Pruning）：如果机器人发现某条路明显是死胡同，它就直接砍掉，不再往下走。
查表（Transposition Tables）：就像记笔记一样，如果之前算过某个局面，它就把它记在“小本本”上，下次遇到同样的局面直接查表，不用重算。

问题来了： 这些“作弊”技巧虽然快，但很容易出错。因为机器人可能会在深度不够的时候查到一个旧笔记，或者因为剪枝太快而错过了真正的最佳走法。这就好比一个学生为了赶时间，抄了作业本上的答案，结果发现那个答案是在特定条件下才对的，直接套用就错了。

这篇论文的作者们（来自荷兰埃因霍温理工大学的团队）做了一件非常硬核的事：他们不用“多跑几遍测试”来检查机器人，而是用数学证明（形式化验证）来确保机器人绝对没错。

核心比喻：侦探与“目击者”

为了证明机器人是对的，作者们发明了一个叫**“目击者”（Witness）**的概念。

传统做法：就像警察抓犯人，只看监控录像（程序运行日志）。如果录像里没看到犯罪，警察就认为没事。但录像可能有死角，或者被剪辑过。
作者的做法：他们要求机器人必须能拿出一个**“完整的目击者”**。
- 想象机器人说：“我给出的这个分数（比如这步棋价值 5 分），是因为我脑子里确实构建了一棵完整的、没有遗漏的‘决策树’，在这棵树上，5 分是无可争议的最优解。”
- 如果机器人拿不出这样一棵完整的树（比如它偷偷剪掉了一部分，或者引用了一个不匹配的旧笔记），那它给出的分数就是不可信的。

他们验证了什么？

作者们用一种叫 Dafny 的“数学语言”（一种能自动检查代码逻辑的编程工具），把两种常见的下棋算法翻译成了数学证明题：

算法 A（Wikipedia 版，NegamaxTTW）：
- 表现：完美通过！
- 比喻：这个机器人很谨慎。当它查“小本本”时，如果笔记里的信息不够确定（比如只说“这步棋至少值 3 分”，但现在的局势需要更精确的判断），它宁愿扔掉笔记，重新算一遍。虽然慢一点，但它保证每次给出的答案都有完整的“目击者”支持，绝对正确。
算法 B（Marsland 版，NegamaxTTM）：
- 表现：翻车了！ 作者发现了一个具体的“反例”。
- 比喻：这个机器人太聪明了，反而聪明反被聪明误。
  - 它之前在一个很窄的视野里（比如只看了 4 步），记下了一个笔记：“这步棋至少值 3 分”。
  - 后来，它在更宽的视野里（比如看 2 步）又遇到了同样的局面。它看到笔记说“至少 3 分”，就以为“既然至少 3 分，那肯定比现在的 2 分好”，于是直接剪掉了去探索其他可能性的路。
  - 结果：它错过了一个其实只有 1 分（对对手来说更好，对自己更差）的陷阱，或者错过了一个其实有 4 分的好机会。它给出的答案在数学上无法用任何完整的“决策树”来解释。这就好比你为了省时间，直接抄了别人的作业，结果发现那题的已知条件变了，你的答案虽然看起来像那么回事，但其实是错的。

为什么这很重要？

以前：大家觉得这些算法“差不多是对的”，因为用了这么多年，没出过大乱子。但就像论文里说的，这些算法非常微妙，微小的改动（比如怎么更新笔记、怎么判断剪枝）就会导致隐蔽的错误，靠人工测试很难发现。
现在：作者们证明了，有些流行的写法其实是“有缺陷”的。他们不仅指出了问题，还给出了一个数学上无懈可击的标准（即“目击者”标准），告诉未来的开发者：如果你想写一个既快又绝对正确的下棋程序，你的代码必须能通过这个“目击者”测试。

总结

这就好比在说：

“我们不仅造了一辆跑得飞快的赛车（下棋算法），我们还用数学方法证明了：A 款赛车虽然快，但刹车系统绝对可靠，不会在弯道失控；而 B 款赛车虽然设计更激进，但在特定弯道（特定棋局）下，它的刹车逻辑有漏洞，可能会导致它以为前面是直路而直接冲出去。以后大家造车，都得按 A 款的标准来，或者至少得知道 B 款哪里会翻车。”

这篇论文的价值在于，它把“感觉上是对的”变成了“数学上证明是对的”，为人工智能在复杂决策领域的可靠性树立了新的标杆。

论文技术总结：Minimax 算法的形式化验证

1. 研究背景与问题定义

背景：
基于 Minimax 的搜索算法（结合 Alpha-Beta 剪枝和置换表/Transposition Tables, TT）是经典游戏引擎的核心组件，广泛应用于国际象棋、围棋等游戏中。尽管这些算法在实践中被广泛使用，但它们极其微妙、高度优化，且难以推理。微小的实现差异可能导致非显而易见的错误，仅靠测试难以发现。

核心问题：
现有的形式化验证工作（如 Nipkow 等人使用 Isabelle 的工作）主要集中在无深度限制的搜索场景。然而，实际应用中普遍使用的是深度限制搜索（Depth-limited Search）。
在深度限制搜索中，置换表（TT）引入了复杂性：

上下文依赖断裂：缓存的结果是在不同的搜索深度、不同的 Alpha-Beta 窗口以及树的不同部分生成的。
语义模糊：传统的基于单一执行树的正确性定义无法解释置换表中“部分探索的子树”和“重用结果”的混合行为。
缺乏形式化基础：置换表条目的有效性（如上下界标志）通常缺乏精确的语义定义，导致难以形式化验证其正确性。

2. 方法论

作者使用 Dafny（一种基于 Floyd-Hoare 逻辑的编程语言和验证器）对 Minimax 和 Negamax 算法及其变体进行了形式化验证。

2.1 核心创新：基于“见证（Witness）”的正确性准则

为了解决深度限制搜索中置换表带来的语义复杂性，作者提出了一种基于见证的正确性准则（Witness-based Correctness Criterion）：

定义：算法返回的值必须能够被一个具体的“见证树（Witness Tree）”所证明。
见证树（ $u'$ ）：是原始游戏树 $u$ $u$ 的一个特定扩展（Expansion）。它满足以下条件：
1. 包含原始树在深度 $d$ 以内的完整截断（ $\lfloor u \rfloor_d = \lfloor u' \rfloor_d$ ）。
2. 对于树中的任何节点，要么包含其所有子节点，要么不包含任何子节点（避免无效的子集）。
3. 算法返回的值必须等于该见证树在 Alpha-Beta 窗口下的 Negamax 值。
意义：这一准则将置换表的重用行为形式化为“隐式地组装了一个更大的有效游戏树”，从而允许验证器检查返回值的合理性，而无需追踪具体的执行轨迹。

2.2 验证对象

作者验证了两种结合了深度限制、Alpha-Beta 剪枝和置换表的 Negamax 变体：

NegamaxTTW：基于维基百科（Wikipedia）描述的常见变体。
NegamaxTTM：基于 Marsland [7] 提出的变体（移除了最佳移动排序，专注于值正确性）。

3. 主要结果

3.1 NegamaxTTW 的完全验证

结果：作者成功使用 Dafny 为 NegamaxTTW 构建了完全机械化的正确性证明。
规模：验证代码约 850 行，在标准工作站上耗时约 4 秒。
过程：验证过程涉及定义复杂的循环不变量（Loop Invariants）和引理（Lemmas），特别是关于“见证树”的结构性属性（如自反性、传递性、子树包含关系）。作者通过显式调用引理而非内联推理，解决了深层嵌套量词导致的验证器超时或内存耗尽问题。
结论：NegamaxTTW 满足基于见证的正确性准则。

3.2 NegamaxTTM 的反例发现

结果：在尝试验证 NegamaxTTM 时，验证器无法建立后置条件。作者通过深入分析未证明的配置，构造了一个具体的反例（Counterexample）。
反例机制：
- 场景：在较窄的 Alpha-Beta 窗口（如 $(0, 2)$ ）下搜索节点 $v$ ，得到一个下界（Lower Bound, LB）值 3 并存入置换表。
- 冲突：随后在更宽的窗口（如 $(0, 5)$ ）下再次搜索同一节点 $v$ （深度更浅）。
- 错误：NegamaxTTM 利用表中存储的下界 3 来缩小当前搜索窗口（将 $\alpha$ 提升至 3），导致窗口变为 $(3, 5)$ 。这引发了过早的剪枝（Beta Cutoff），使得算法跳过了一个本应被探索且能提供更优值（如 1）的子树。
- 结果：算法返回了值 2，但在任何合法的见证树扩展中，都无法得到值 2（正确的 Minimax 值应为 1 或 4）。
结论：NegamaxTTM 违反了基于见证的正确性准则。其根本原因在于错误地复用了在窄窗口下计算出的下界，导致在宽窗口下进行了不正确的剪枝。

3.3 算法差异分析

通过对比 NegamaxTTW 和 NegamaxTTM 的执行轨迹，作者发现关键差异在于置换表查找（Table Lookup）阶段：

NegamaxTTW：只有当存储的值能立即保证剪枝（即满足 $t.value \ge \beta$ 或 $t.value \le \alpha$ 等严格条件）时才返回；否则忽略该条目并执行完整搜索。这种保守策略保证了见证树的存在。
NegamaxTTM：利用存储的上下界来缩小当前的 Alpha-Beta 窗口。这种策略在窗口变宽时会导致错误，因为它假设窄窗口下的界限在宽窗口下依然有效，从而破坏了正确性。

4. 关键贡献

提出了基于见证的正确性准则：首次为带有置换表的深度限制搜索形式化定义了一个灵活且直观的正确性标准，解决了“部分探索子树”和“重用结果”的语义难题。
首个深度限制 Negamax 的形式化证明：提供了 NegamaxTTW 算法的完全机械化证明，这是该领域的重要进展。
发现并证明了现有算法的缺陷：通过形式化验证，发现并构造了 Marsland 提出的 NegamaxTTM 算法的具体反例，揭示了其逻辑漏洞。
验证了多种变体：验证了超过 15 种 Minimax/Negamax 变体（从基础递归到深度限制优化），所有验证工件（Dafny 代码、Python 实现）均已开源。

5. 意义与影响

理论意义：证明了形式化方法在处理具有复杂状态（如置换表）和递归结构的 AI 搜索算法时的有效性。它表明，仅靠直觉或测试无法保证此类高度优化算法的正确性。
实践意义：
- 为游戏引擎开发者提供了经过严格验证的算法参考（NegamaxTTW）。
- 警示了直接复用旧有算法（如 NegamaxTTM）可能带来的隐蔽错误，特别是在处理置换表窗口管理时。
未来方向：该框架可扩展至其他依赖置换表状态的搜索算法（如 SSS*, MTD(f)），甚至可能应用于量子游戏树搜索的验证。

总结：这篇论文通过引入“见证树”概念，成功解决了深度限制搜索中置换表正确性验证的难题，不仅证实了一个流行算法的正确性，还通过反例推翻了另一个看似合理的算法，展示了形式化验证在 AI 算法工程中的核心价值。