形式驗證

Dafny

Dafny 形式驗證 Alpha‑Beta 剪枝與 Minimax/Negamax 演算法

本研究聚焦於以Dafny形式驗證Minimax系列搜尋演算法，涵蓋Alpha‑Beta剪枝與轉置表等優化手法。研究者為深度受限的兩種變體設計見證式正確性條件，並完成全部驗證與Python參考實作。此成果為遊戲人工智慧提供可驗證的基礎，減少實作錯誤與效能不確定性。