Verifica Formale di Algoritmi di Ricerca Minimax Utilizzando Dafny

Utilizzando il sistema di verifica Dafny, i ricercatori hanno confermato con successo la correttezza degli algoritmi di ricerca basati su minimax che incorporano potatura alfa-beta e tabelle di trasposizione. Questi algoritmi svolgono un ruolo cruciale nei motori di gioco tradizionali, ma sono complessi e finemente ottimizzati, rendendo difficile identificare errori solo tramite test. La ricerca presenta un criterio di correttezza basato su testimoni per ricerche a profondità limitata che utilizzano tabelle di trasposizione, che indica quando i valori restituiti possono essere giustificati da una chiara espansione dell'albero di gioco. Questo criterio è stato testato su due adattamenti pratici di negamax a profondità limitata con potatura alfa-beta e tabelle di trasposizione: una variante ha ottenuto una prova di correttezza meccanizzata completa, mentre per l'altra è stato creato un controesempio concreto. Questo studio affronta le ben note difficoltà nel ragionare su questi algoritmi e stabilisce una base formale per la loro correttezza.