ミニマックスアルゴリズムの形式検証
なぜ重要か: 企業や社会への影響が見込まれ、一般メディアにも波及する可能性があります。
arXiv:2509.20138v1 発表種別：新規
概要：Dafny検証システムを用いて、アルファ・ベータ枝刈りや置換表を用いた変種を含む、様々なミニマックス探索アルゴリズムを形式的に検証した。置換表を用いた深さ限定探索に対しては、witness-based 正しさの基準を導入し、2つの代表的なアルゴリズムに適用した。全ての検証成果物（証明やPython実装を含む）は公開されている。
原文（英語）を表示
Title (EN): Formal Verification of Minimax Algorithms
arXiv:2509.20138v1 Announce Type: new
Abstract: 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.
Published: 2025-09-24 19:00 UTC