Le scoperte matematiche dell'IA che tutti citano sono controesempi, non prove.

      Un controesempio e una dimostrazione non sono la stessa cosa. Una dimostrazione mostra che qualcosa è sempre vero. Un controesempio mostra che qualcosa che si afferma essere sempre vero non lo è, producendo un oggetto in cui fallisce. Entrambi risolvono una questione. Chiedono cose diverse a chi li trova. Uno richiede un argomento che copra ogni caso. L'altro richiede un singolo oggetto e il permesso di continuare a indovinare fino a quando non lo si ha. Quella distinzione è l'oggetto di un post sul blog che il matematico di Cambridge Timothy Gowers ha pubblicato il 12 agosto. Gowers ha vinto la Medaglia Fields nel 1998. Ha anche letto i documenti, cosa che la maggior parte delle persone che commentano l'IA e la matematica non ha fatto. Non è sprezzante. Chiama i risultati "straordinariamente impressionanti" e dice chiaramente che i modelli possono dimostrare anche cose difficili. "I LLM non sono bravi solo a trovare controesempi: possono trovare anche dimostrazioni di affermazioni difficili", scrive.

      Cosa hanno in comune i risultati famosi

      OpenAI ha annunciato dieci problemi aperti risolti in matematica e informatica teorica. Due hanno guidato la copertura. Il primo è stata la costruzione di un gruppo non-sofico. Gowers ha assistito alle conferenze. Lo definisce "uno dei problemi irrisolti più importanti nella teoria dei gruppi". Il secondo è stato un limite inferiore che mostra che un numero di Ramsey multicolore cresce superesponenzialmente. Su questo è insolitamente sincero. Era "un grande problema aperto nella teoria di Ramsey che non mi aspettavo necessariamente di vedere risolto nella mia vita".

      Poi arriva l'osservazione che gli aggregatori hanno saltato. I risultati LLM più celebrati, nota Gowers, sono quasi tutti arrivati come controesempi piuttosto che come dimostrazioni. Conta i due sopra, più la congettura di Jacobiano e la congettura della distanza unitaria. Il suo terzo punto di sintesi è la versione attenta. I modelli dimostrano affermazioni universali molto bene. Ma le cose più forti che hanno dimostrato non corrispondono alle cose più forti che hanno smentito.

      Due risultati che riclassifica

      Un controesempio guadagna il suo nome demolendo qualcosa in cui le persone avevano buone ragioni per credere. Secondo questo standard, Gowers riclassifica due dei risultati principali, incluso uno contro la propria documentazione. Sull gruppo non-sofico, dice che diversi percorsi di costruzione esistevano già nella letteratura. Dubita anche che molti esperti credessero fermamente che tutti i gruppi fossero sofici. Quindi si legge più naturalmente come il primo esempio di un gruppo non-sofico piuttosto che come un controesempio. Nota direttamente la tensione: OpenAI ha intitolato quella sezione del suo documento "Un controesempio alla congettura di soficità".

      Il risultato di Ramsey riceve lo stesso trattamento, e qui segna i suoi compiti. Molte persone si aspettavano un limite esponenziale, quindi per loro è stato un controesempio. Gowers era neutrale. Aveva lavorato su una formulazione equivalente anni fa. I suoi sforzi all'epoca si sono rivelati nella direzione giusta. Per lui ha confermato una debole aspettativa piuttosto che rovesciare una credenza.

      Perché gli esempi si adattano alle macchine

      Gowers elenca otto modi in cui i matematici cercano un esempio. Provare esempi standard già pronti. Costruirne uno da pezzi familiari. Lasciare parti indefinite e compilarle man mano che la dimostrazione richiede. Provare a dimostrare l'opposto e vedere cosa si rompe. Indovinare, fallire, diagnosticare, indovinare di nuovo. Costruire l'oggetto passo dopo passo. Sceglierne uno a caso. Sceglierne uno generico. Quattro di questi si adattano a ciò che una macchina ha già: una vasta conoscenza e la capacità di eseguire enormi numeri di tentativi. Il controllo standard, la costruzione passo dopo passo, l'argomento probabilistico e l'esempio generico premiano tutti il volume. Tre degli altri necessitano di qualcos'altro. Lasciare parti indefinite, provare a dimostrare l'opposto e l'approssimazione successiva richiedono tutti un giudizio su se l'approccio attuale valga la pena di essere continuato.

      È lì che Gowers colloca il divario, e non è una capacità grezza. Lo chiama un "naso", intendendo il senso di quando si sta andando da qualche parte e quando abbandonare un ramo. È ciò che consente a un umano di potare un albero di ricerca che nessun computer potrebbe esaurire.

      Cinque riduzioni e nessun progresso

      La sua evidenza per il divario è in parte aneddotica, e lo dice. Lavorando con GPT-5.6 Pro su problemi aperti, spesso gli vengono presentati approcci che sembrano promettenti e poi non sopravvivono all'analisi. Descrive anche un modello di risposta riconoscibile. Il modello riporta di non aver risposto alla domanda, ma di averla ridotta a una più ristretta e precisa, "che suona molto promettente fino a quando non è successo cinque volte senza alcun progresso ovvio". Gli esperti reagiscono ai successi genuini in un modello anche, scrive: stupore inizialmente, poi uno sguardo più attento rivela un approccio che non era particolarmente nuovo e che un umano esperto avrebbe potuto trovare con un piccolo suggerimento.

      La sua spiegazione sul perché il naso potrebbe non emergere semplicemente è la cosa più interessante nel post. La matematica pubblicata nasconde la ricerca. I modelli vedono, con le sue parole, "dimostrazioni sistematizzate che nascondono i processi di pensiero dei loro scopritori".

      I vicoli ciechi non raggiungono mai la letteratura. Quindi i dati di addestramento non contengono quasi alcun record delle direzioni abbandonate, o perché. Aggiunge una seconda ragione. Un sistema abbastanza veloce da provare tutto ha pochi incentivi per imparare a potare.

      Il test che accetterà

      Gowers offre uno standard falsificabile, che è più di quanto riesca a fare la maggior parte dei commenti. Accetterà l'ostacolo superato quando un modello produce una dimostrazione sorprendente come la soluzione del cap-set del 2016, dove i vecchi limiti sono stati eclissati e il metodo era diverso da qualsiasi cosa avesse considerato di provare.

      Propone anche una soluzione. Le strutture di ricompensa attualmente valutano la risposta. Penalizzare un modello per aver esplorato troppi vicoli ciechi, o per aver sollevato il risultato dalla letteratura, potrebbe spingerlo verso una ricerca più umana.

      Niente di tutto ciò è una previsione che i modelli si fermeranno. Gowers si aspetta che continuino a migliorare rapidamente, si aspetta che l'ostacolo cada e ammette che potrebbe aggrapparsi alla speranza che gli esseri umani continuino a contribuire per un po'. La distinzione che fa riguarda ciò che è successo finora, non ciò che è possibile.

      Il che rende l'aggregazione del suo post degna di nota. Il Decoder lo ha riassunto come i migliori matematici che chiamano i LLM calcolatori forti ma poveri pensatori creativi. Gowers ha scritto che i modelli trovano dimostrazioni di affermazioni difficili, che i risultati sono straordinariamente impressionanti e che non fa alcuna affermazione su ciò che non faranno mai. Il suo post precedente ha affrontato la Dichiarazione di Leiden.

      Ora è stato ridotto a uno scettico due volte in tre settimane.

      L'affermazione sottostante è più ristretta e più difficile da respingere. Le macchine stanno vincendo dove il metodo è provare un gran numero di cose. È anche dove vengono trovati difetti crittografici e dove i test nel Regno Unito hanno mostrato che i modelli imbrogliano quando esiste un'abbreviazione.

      Il test del cap-set non ha scadenza, il che è piuttosto il punto. Qualcuno pubblicherà una dimostrazione. L'argomento sarà quindi se il metodo fosse presente nei dati di addestramento fin dall'inizio.