Formal Verification of Minimax Algorithms

arXiv:2509.20138v2 Announce Type: replace Abstract: 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.

Related

• Learning Evolution via Optimization Knowledge Adaptation
• Early Pruning for Public Transport Routing
• Adapting Dijkstra for Buffers and Unlimited Transfers
• Decidable By Construction: Design-Time Verification for Trustworthy AI

Source: arXiv cs.AI | 2026-04-23