极小化极大算法的形式化验证
人工智能
2026-04-23 v2
摘要
具有 alpha-beta 剪枝和转换表的极小化极大搜索算法是经典游戏引擎的核心组成部分，至今仍在实践中广泛使用。尽管这些算法被广泛使用，但它们精细且高度优化且臭名昭著地难以推理，仅靠测试难以发现非明显的错误。使用 Dafny 验证系统，我们对一系列极小化极大搜索算法进行了形式化验证，包括带有 alpha-beta 剪枝和转换表的变体。对于带转换表的深度受限搜索，我们引入了一种基于见证的正确性准则，用于刻画返回值何时可由显式的博弈树展开来证明。我们将该准则应用于深度受限 negamax 的两种实际变体（均带 alpha-beta 剪枝和转换表）：对于其中一种变体，我们获得了完全机械化的正确性证明，而对于另一种变体，我们构造了一个具体的反例，证明了所提出的正确性概念被违反。所有验证产物，包括 Dafny 证明和可执行的 Python 实现，均公开可用。
引用
@article{arxiv.2509.20138,
title = {Formal Verification of Minimax Algorithms},
author = {Wieger Wesselink and Kees Huizing and Huub van de Wetering},
journal= {arXiv preprint arXiv:2509.20138},
year = {2026}
}
备注
18 pages. Revised and extended version submitted to CAV 2026