Un'IA chiude in tre giorni la congettura di Aaronson-Ambainis, aperta dal 2008

Alla fine del terzo giorno di elaborazione, il sistema di ricerca di Physical Superintelligence (PSI) aveva in mano una dimostrazione completa. Il problema era la congettura di Aaronson-Ambainis, formulata nel 2008 e rimasta aperta da allora. La società ha comunicato di aver lavorato con infrastruttura interna e con istanze di un modello Anthropic non disponibile al pubblico.

La domanda di fondo è se un computer quantistico risolva sempre un problema molto più in fretta di uno tradizionale. La risposta è no. Il caso più noto di vantaggio enorme è l'algoritmo di Peter Shor del 1994, che fattorizza grandi numeri sfruttando la periodicità, cioè gli schemi ripetitivi nascosti nel problema. Resta aperto quanto il vantaggio quantistico dipenda dalla presenza di una struttura di questo tipo.

Nel 2008 Scott Aaronson e Andris Ambainis ipotizzarono che, con input casuali e privi di regolarità, in una specifica classe di problemi il computer quantistico non possa ottenere un vantaggio esponenziale. Si pensi a una sequenza di milioni di interruttori, ciascuno su 0 o 1, da analizzare per rispondere sì o no. Il computer classico li consulta uno alla volta. Quello quantistico, grazie alla sovrapposizione degli stati, può organizzare diversamente le interrogazioni, senza però leggere gratis l'intera sequenza.

La congettura traduce la questione in una proprietà delle funzioni polinomiali. Se il risultato dipende da una funzione costruita sui singoli bit e sulle loro combinazioni, e varia in modo significativo, almeno un bit deve avere un'influenza non trascurabile, ossia deve cambiare in modo apprezzabile l'esito quando passa da 0 a 1. Non possono dunque milioni di variabili contribuire tutte in misura infinitesimale. Dimostrarlo dà a un algoritmo classico il modo di imitare quello quantistico: può concentrarsi sui bit più influenti e stimare il risultato senza esaminare tutto l'input. Per questa classe di problemi, le interrogazioni necessarie crescono al più in modo polinomiale rispetto a quelle dell'algoritmo quantistico, non in modo esponenziale.

Sul piano del metodo, l'aspetto più notevole è la verifica. La dimostrazione è stata formalizzata in Lean, un proof assistant che controlla ogni passaggio rispetto a definizioni, regole logiche e ipotesi. Non basta quindi che un'altra IA giudichi plausibile il ragionamento. Secondo la documentazione, la prova è stata controllata anche con due implementazioni indipendenti del kernel di Lean, senza passaggi lasciati in sospeso e senza assiomi aggiunti. PSI ha pubblicato su GitHub il paper e il codice della formalizzazione, così che chiunque possa riprodurre le verifiche.

Il lavoro è stato guidato da David Turturean, dello staff tecnico di PSI, che ha sviluppato il sistema, impostato il problema e supervisionato la produzione della prova. Jim Halverson ha contribuito all'audit e Phiala Shanahan ha dato osservazioni sulla formalizzazione. Secondo la società, anche Guy Blanc, Jordan Docter, Carmen Strassle e Li-Yang Tan, ricercatori di Stanford che nell'agosto 2026 avevano dimostrato un caso particolare della congettura, hanno esaminato la nuova prova e inviato commenti.

Va evitato un equivoco: non si dimostra che i computer quantistici non offrano più vantaggi significativi. La conclusione è circoscritta ai problemi considerati, in assenza di strutture particolari negli input e nel modello di interrogazione studiato. I ricercatori di Stanford stanno ora preparando una presentazione più breve del risultato per la comunità scientifica, che sarà il passaggio da osservare.