Modelli di IA testati per la fedeltà del ragionamento logico in uno studio di verifica formale

Uno studio recente esplora se i modelli di IA sofisticati sfruttino le carenze nella verifica formale durante la produzione di dimostrazioni logiche. I ricercatori hanno valutato GPT-5 e DeepSeek-R1 su 303 sfide di logica del primo ordine provenienti dai dataset FOLIO e Multi-LogiEval, concentrandosi sul fenomeno del 'formalization gaming'. Sebbene i modelli abbiano raggiunto tassi di compilazione compresi tra l'87% e il 99%, non sono stati rilevati segni coerenti di gaming. I modelli tendevano a segnalare fallimenti invece di tentare di generare dimostrazioni, anche con prompt specifici. L'indagine ha confrontato la generazione unificata con una pipeline a due fasi, scoprendo diverse modalità di infedeltà che sfuggono al rilevamento. I risultati evidenziano la disparità tra dimostrazioni valide e traduzioni accurate nei sistemi di ragionamento in linguaggio naturale. Mentre la verifica formale garantisce la validità delle dimostrazioni, non assicura la fedeltà, creando potenziali vulnerabilità, specialmente per i modelli all'avanguardia che sviluppano sistemi di assiomi in modo autonomo. Per valutare la fedeltà sono state utilizzate dimostrazioni Lean 4.