Formal Verification of Minimax Algorithms
This work addresses the need for reliable and provably correct algorithms in game theory and AI, particularly for developers and researchers using minimax-based methods, though it is incremental as it applies existing verification techniques to specific algorithms.
The authors tackled the problem of ensuring correctness in minimax search algorithms by formally verifying them using the Dafny system, including variants with alpha-beta pruning and transposition tables, and introduced a witness-based correctness criterion for depth-limited search with transposition tables, with all verification artifacts made publicly available.
Using the Dafny verification system, we formally verify a range of minimax search algorithms, including variations with alpha-beta pruning and transposition tables. For depth-limited search with transposition tables, we introduce a witness-based correctness criterion and apply it to two representative algorithms. All verification artifacts, including proofs and Python implementations, are publicly available.