I LLM faticano nel ragionamento SAT nonostante l'alta accuratezza

Un nuovo studio da arXiv rivela che i grandi modelli linguistici (LLM) falliscono nel ragionamento di soddisfacibilità booleana (SAT) nonostante ottengano punteggi elevati nelle metriche convenzionali. La ricerca valuta sistematicamente gli LLM su problemi 2-SAT e 3-SAT, insieme a riduzioni di Vertex Cover e 3D packing discreto. Metriche standard come accuratezza, precisione, richiamo e F1 sono fuorvianti perché i modelli sovrastimano le formule soddisfacibili e non riescono a riprodurre la classica firma facile-difficile-facile attorno alla soglia 3-SAT. Le prestazioni degradano bruscamente all'aumentare del numero di variabili. Per affrontare questo problema, gli autori introducono un protocollo a formule accoppiate che utilizza istanze soddisfacibili e insoddisfacibili minimamente diverse, insieme al Tasso di Differenziazione Accurata (ADR), che richiede ai modelli di distinguerle. I risultati evidenziano limitazioni fondamentali nelle capacità di ragionamento degli LLM.