用形式化验证确保博弈搜索算法正确性，发现并证明了实际代码中的错误。
Formal Verification of Minimax Algorithms
- 通过见证机制定义返回值正确性的判定标准
- 一个变种算法获完全证明，另一个发现具体反例
- 适合研究博弈算法可靠性或形式化验证的开发者
基于极小极大搜索的算法（含剪枝和置换表）是经典博弈引擎的核心，虽广泛应用却因高度优化而难以推理，仅靠测试难发现隐蔽错误。本文使用Dafny验证系统，对多种极小极大搜索算法进行形式化验证，包括带剪枝和置换表的变体。针对深度受限搜索与置换表，提出一种基于见证的正确性标准，用于判断返回值是否可由显式博弈树展开解释。将该标准应用于两个实际的深度受限负极大值剪枝加置换表算法变体：一个获得完整机械化证明，另一个构造出具体反例，证明其违反正确性定义。所有验证代码、Dafny证明及可运行的Python实现均已公开。
原文摘要 · Abstract (English)
Minimax-based search algorithms with alpha-beta pruning and transposition tables are a central component of classical game-playing engines and remain widely used in practice. Despite their widespread use, these algorithms are subtle, highly optimized, and notoriously difficult to reason about, making non-obvious errors hard to detect by testing alone. Using the Dafny verification system, we formally verify a range of minimax search algorithms, including variants with alpha-beta pruning and transposition tables. For depth-limited search with transposition tables, we introduce a witness-based correctness criterion that captures when returned values can be justified by an explicit game-tree expansion. We apply this criterion to two practical variants of depth-limited negamax with alpha-beta pruning and transposition tables: for one variant, we obtain a fully mechanized correctness proof, while for the other we construct a concrete counterexample demonstrating a violation of the proposed correctness notion. All verification artifacts, including Dafny proofs and executable Python implementations, are publicly available.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。