La notizia pubblicata oggi da Scientific American secondo cui un'intelligenza artificiale potrebbe aver contribuito alla soluzione del problema delle equazioni di Navier–Stokes - uno dei Millennium Prize Problems del Clay Mathematics Institute (1) - potrebbe rappresentare il momento in cui per la prima volta la nostra specie si trova costretta a distinguere in modo concreto tra capacità di dimostrare una verità matematica e capacità di comprenderla.
Qualche giorno fa, conclusa la lettura del saggio di Marcus du Sautoy "Il codice della creatività", avevo iniziato la scrittura di un post che verteva sul test di Lovelace, una riflessione che coinvolge tre figure fondamentali della storia dell'informatica e della logica: Ada Lovelace, Alan Turing e Kurt Gödel.
Tale test si basa su una domanda semplice da formulare: può una macchina produrre una dimostrazione matematica autenticamente nuova, corretta e non prevista dai suoi creatori, ma che gli esseri umani non sono in grado di comprendere?
Se un giorno la risposta diventasse affermativa non avremmo semplicemente costruito uno strumento matematico più potente ma introdotto nella cultura una nuova forma di produzione della conoscenza.
Nel 1843 Augusta Ada Lovelace, figlia legittima del poeta Lord Byron e della matematica Anne Isabella Milbanke, dopo aver esaminato la macchina analitica di Charles Babbage, fece una dichiarazione che sta alla base del test che porta il suo nome: "... una macchina non è dotata di una propria capacità di originare qualcosa; è invece in grado di fare soltato ciò che le viene ordinato ...".
Questa intuizione sarebbe stata ripresa più di un secolo dopo da Selmer Bringsjord, Paul Bello e David Ferrucci, che nel 2001 proposero il cosiddetto Lovelace Test come criterio per individuare una forma di creatività artificiale
Una sua formulazione (semplificata) può esser la seguente:
"ad una macchina viene assegnato un compito creativo; si stabiliscono vincoli abbastanza precisi, la macchina produce un risultato e
il progettista non riesce a spiegare come quel risultato sia stato ottenuto semplicemente a partire dalle regole e dagli obiettivi che aveva fornito".
Se il risultato è realmente sorprendente e non è riconducibile ad una procedura esplicitamente prevista dal programmatore, la macchina ha superato il test.
Il fatto è che l'affermazione della Lovelace "la macchina non origina nulla, ma esegue ciò che sappiamo comandarle" col passar del tempo e l'evoluzione delle AI è diventata sempre più difficile da difendere.
Con i moderni sistemi di AI non è più necessario programmare esplicitamente ogni passaggio per ottenere un risultato: si costruisce un sistema, gli si fornisce o dati, gli obiettivi e le procedure di addestramento, e si lascia che emerga spontaneamente una soluzione.
Una AI supera il test di Lovelace quando produce un risultato che il suo progettista non è in grado di spiegare come conseguenza diretta delle istruzioni impartite.
In questo contesto la matematica rappresenta probabilmente il banco di prova più severo; un'immagine generata da una macchina può essere sorprendente ma possiamo sempre discutere se sia davvero “creativa” mentre una dimostrazione matematica può essere corretta oppure scorretta, mentre la proposizione che dimostra è vera oppure falsa.
Ecco che se l'AI producesse una dimostrazione nuova e corretta di un teorema profondo non sarebbe più possibile liquidare il risultato come semplice imitazione statistica: la macchina avrebbe infatti individuato una struttura matematica valida.
La vicenda Navier–Stokes sembra indicare questa possibilità.
Le equazioni di Navier–Stokes sono fra gli strumenti fondamentali della matematica applicata e della fisica matematica: descrivono il comportamento dei fluidi e sono alla base della nostra comprensione matematica di fenomeni come vortici e turbolenza.
Il problema del Clay Institute - che ha messo in palio per la soluzione un premio di un milione di dollari - chiede di dimostrare che le soluzioni tridimensionali rimangano sempre regolari oppure di mostrare che possa verificarsi una singolarità in tempo finito. (2)
La vicenda raccontata da Scientific American è interessante in quanto coinvolge matematici umani, modelli linguistici e sistemi di verifica formale.
Ma attenzione! La questione non è ancora chiusa definitivamente: la dimostrazione dovrà essere verificata dalla comunità matematica e sottoposta alle procedure del Clay Institute (cosa che richiede tempi lunghi).
Supponiamo per un momento che il risultato venga confermato: una macchina risulterebbe allora aver contribuito a trovare una dimostrazione che nessuno dei matematici coinvolti aveva inizialmente previsto.
A quel punto la domanda non sarebbe più "l'AI sa fare matematica?" ma "chi sta facendo matematica?".
E qui entra in scena Kurt Gödel.
I teoremi di incompletezza del 1931 distrussero l'idea che un sistema formale sufficientemente potente potesse essere contemporaneamente completo e capace di garantire, dall'interno, la propria coerenza.
In sostanza Gödel afferma che esistono proposizioni matematiche impossibili da dimostrare all'interno di determinati sistemi formali qualora questi ultimi siano coerenti e sufficientemente espressivi.
Una macchina che lavora attraverso un sistema formale potrebbe, almeno in linea di principio, essere estremamente potente nella ricerca di dimostrazioni, ma la lezione gödeliana ci ricorda però che nessun singolo sistema formale sufficientemente potente può esaurire tutte le verità matematiche esprimibili al suo interno.
La matematica non è infatti semplicemente un enorme database di dimostrazioni ma un territorio nel quale continuamente emergono nuovi assiomi, nuovi linguaggi, nuovi sistemi formali e nuove domande.
E questo conduce a un'apparente contraddizione: se l'AI produce una dimostrazione che l'uomo non comprende abbiamo ottenuto una conoscenza matematica?
La risposta è "formalmente sì ma epistemologicamente forse non ancora".
Questo perché una dimostrazione non è soltanto una sequenza di simboli corretti ma, per un matematico, è anche una spiegazione.
Non è un caso che lo stesso Clay Institute sottolinei che una dimostrazione non fornisce soltanto certezza, ma anche comprensione.
Alan Turing porta poi il problema su un altro terreno.
Nel 1950, nel suo famoso articolo Computing Machinery and Intelligence, propose di sostituire la domanda “le macchine possono pensare?” con una domanda operativa: "possono comportarsi in modo indistinguibile da un essere umano in determinate condizioni?"
Turing aveva già intuito qualcosa di ancora più interessante: le macchine possono produrre risultati che non sono facilmente prevedibili dai loro programmatori.
Il comportamento di un programma può infatti dipendere da una complessità computazionale tale che prevedere in anticipo ciò che farà diventa impraticabile, e questo introduce una distinzione fondamentale: determinismo non significa prevedibilità.
Un sistema può infatti essere completamente deterministico e tuttavia produrre risultati che nessun essere umano è in grado di anticipare.
È esattamente ciò che potrebbe accadere con l'AI matematica: i parametri di una rete neurale possono essere determinati dall'addestramento, l'algoritmo può essere conosciuto e il processo può essere, almeno in linea di principio, computabile, e tuttavia nessun essere umano potrebbe essere in grado di prevedere quale nuova dimostrazione emergerà.
Non c'è bisogno di introdurre una misteriosa “creatività” metafisica, è sufficiente la complessità.
Il fatto è che "dimostrazione non significa comprensione".
Immaginiamo che un sistema di AI produca una dimostrazione di 200.000 passaggi; un verificatore formale (come Lean) potrebbe controllare che ogni passaggio sia valido e la dimostrazione risulterebbe quindi matematicamente certificata, ma immaginiamo anche che nessun essere umano riesca a capire la strategia complessiva.
Abbiamo allora due possibilità:
È matematica: se è formalmente corretta è sufficiente
È una dimostrazione ma non è ancora una spiegazione
La differenza tra le due posizioni è enorme.
Per secoli la matematica ha funzionato attraverso una straordinaria economia concettuale: una buona dimostrazione non serve soltanto a convincerci che un'affermazione è vera ma ci mostra perché lo è.
Euclide non ci consegna semplicemente una lista di operazioni corrette, ci mostra una struttura.
Una dimostrazione di Eulero, Gauss o Riemann è importante anche perché comprime una quantità enorme di informazione in un'intuizione che una mente umana può assimilare.
L'AI potrebbe spezzare questo equilibrio producendo dimostrazioni corrette ma cognitivamente intrattabili.
Potremmo quindi riformulare il Test di Lovelace in una versione molto più radicale sostituendo la richiesta "la macchina ha prodotto qualcosa che il programmatore non aveva previsto?" con "la macchina ha prodotto una struttura matematica che nessun essere umano aveva previsto e che, pur essendo verificabile, nessun essere umano riesce inizialmente a comprendere?"
Se accadesse, avremmo qualcosa di qualitativamente diverso dall'AI come semplice assistente: non sarebbe più soltanto uno strumento per accelerare la matematica umana ma diventerebbe una macchina di esplorazione matematica.
E potrebbe accadere qualcosa di ancora più spaventoso: gli esseri umani potrebbero essere costretti a sviluppare nuovi concetti per comprendere ciò che l'AI ha scoperto.
In questo scenario l'AI non sarebbe soltanto un matematico artificiale ma un generatore di nuovi territori matematici.
Altra questione, che sorgerebbe qualora il Clay confermasse la correttezza della soluzione, è riassumibile nella domanda: chi avrebbe risolto il problema?
Se Buckmaster e Alpoge hanno avuto l'idea iniziale, se altri matematici hanno sviluppato la teoria, se un LLM ha suggerito passaggi, se un altro sistema ha prodotto una dimostrazione e Lean ne ha verificato formalmente la correttezza, a chi appartiene il risultato?
Non è una domanda puramente accademica: la matematica è tradizionalmente associata all'autore della dimostrazione ma in un sistema ibrido uomo–AI l'autorialità potrebbe diventare distribuita:
intuizione umana → esplorazione AI → selezione umana → dimostrazione AI → verifica formale → interpretazione umana.
Non esiste più necessariamente un singolo autore cognitivo e ci troveremmo in na situazione completamente nuova nella storia della matematica.
Cosa comporterebbe poi il caso in cui l'AI scoprisse una matematica che noi non capiamo?
Per millenni la matematica è stata una disciplina costruita attorno alle capacità cognitive umane.
Anche quando utilizziamo computer siamo ancora noi a decidere quali domande porre, quali strutture cercare e quali risultati siano interessanti.
Un'AI molto più potente potrebbe invece esplorare uno spazio matematico enormemente più vasto, scoprire connessioni che richiederebbero migliaia di anni di ricerca umana, e a quel punto potrebbe verificarsi una situazione paradossale: sapremmo che un teorema è vero senza sapere perché lo sia.
Potremmo persino sapere che una certa congettura è dimostrabile senza possedere una rappresentazione mentale della dimostrazione.
La situazione inizierebbe allora, almeno metaforicamente, ad assomigliare alla fisica sperimentale: potremmo avere accesso a fatti la cui spiegazione concettuale ci sfugge.
Ma la matematica possiede una caratteristica particolare:mentre in fisica possiamo accettare che un fenomeno sia osservato prima di essere spiegato, in matematica la spiegazione è parte stessa dell'oggetto matematico.
Per questa ragione una dimostrazione incomprensibile potrebbe rappresentare contemporaneamente un trionfo e una crisi.
Turing aveva trasformato la domanda sull'intelligenza in una domanda sul comportamento; Gödel aveva mostrato i limiti dei sistemi formali; la Lovelace aveva sollevato il problema dell'originalità delle macchine: l'AI contemporanea sta mettendo queste tre intuizioni in collisione.
La domanda non è più soltanto se una macchina possa superare il Test di Turing, ma potremmo trovarci davanti ad un nuovo problema: "può una macchina produrre conoscenza che la mente umana può verificare ma non comprendere?" o ancora più radicalmente: "se possiamo verificare che una macchina ha ragione senza capire perché, possiamo dire che quella conoscenza appartiene ancora alla scienza umana?".
La possibile soluzione delle Navier–Stokes rappresenta un laboratorio perfetto per questa domanda.
Una nuova domanda che potrebbe proporre il Clay Institute potrebbe essere: "quanto lontano può arrivare la matematica prima di diventare cognitivamente estranea alla mente che l'ha inventata?"
Forse stiamo entrando in un'epoca nella quale l'umanità non sarà più necessariamente il limite superiore della capacità matematica e il paradosso è straordinario: sinora abbiamo costruito macchine per aiutarci a comprendere la matematica, potremmo aver costruito invece macchine capaci di produrre matematica che noi dovremo ancora imparare a comprendere.
Il possibile episodio delle Navier–Stokes potrebbe essere ricordato in futuro non come il giorno in cui l'AI ha risolto un problema da un milione di dollari ma come il giorno in cui il Test di Lovelace è entrato nella matematica.
Allora la domanda finale non sarà più "l'AI può fare matematica?" ma "siamo ancora noi il pubblico a cui la matematica deve essere spiegata?"
Note:
(1) Nell'anno 2000 il Clay Mathematics Institute stanziò un fondo complessivo di 7 milioni di dollari suddiviso in un milione per ciascuno dei sette problemi:
Ipotesi di Riemann
P versus NP
Congettura di Hodge
Equazioni di Navier–Stokes
Yang–Mills e mass gap
Congettura di Birch e Swinnerton-Dyer
Congettura di Poincaré
Ad oggi soltanto uno di questi 7 è stato risolto: la congettura di Poincaré la cui soluzione è stata proposta nel 2002-2003 dall'eccentrico matematico russo Grigorij Perelman. (che come è noto rifiutò sia la Medaglia Fields sia il premio di un milione di dollari del Clay Institute)
Il Clay Institute l'ha riconosciuta come valida soltanto nel 2010.
Quindi se il risultato descritto oggi da Scientific American venisse confermato dal Clay Institute sarebbe soltanto la seconda volta nella storia che uno dei sette Millennium Problems viene risolto.
(2) Il problema è quello delle equazioni di Navier–Stokes, in termini molto semplificati, chiede di stabilire se, partendo da condizioni iniziali ragionevoli, le equazioni tridimensionali della fluidodinamica producano sempre soluzioni regolari e lisce, oppure se possa verificarsi un blow-up, una situazione nella quale alcune grandezze diventano matematicamente infinite in un tempo finito.
È una questione fondamentale perché le Navier–Stokes descrivono il moto dei fluidi: acqua, aria, turbolenza, atmosfera ecc.
La storia raccontata da Scientific American vede i protagonisti - il matematico Tristan Buckmaster e Levent Alpoge, matematico e dipendente di Anthropic - lavorare ad un'idea sviluppata originariamente da Diego Córdoba e Luis Martínez-Zoroa.
L'idea riguarda un termine delle equazioni che normalmente viene considerato trascurabile nel modo in cui viene formulato il problema di Clay: il cosiddetto forcing, cioè un termine di forzamento.
Buckmaster e Alpoge, aiutandosi con modelli linguistici di Anthropic, avrebbero prima ottenuto un risultato importante sulle equazioni di Eulero (una versione più semplice delle Navier–Stokes) mostrando che possono sviluppare un blow-up.
Il risultato sarebbe stato formalmente verificato con Lean, un sistema di verifica formale delle dimostrazioni.
Poi sarebbe accaduto qualcosa di straordinario: secondo il racconto di Buckmaster informazioni sul loro lavoro sarebbero arrivate ad OpenAI che aveva già un gruppo impegnato sul problema.
Il team avrebbe utilizzato un modello interno per estendere rapidamente l'idea al caso completo delle Navier–Stokes.
Qui nasce la parte più controversa.
È davvero una soluzione del problema da un milione di dollari? Ancora non possiamo ancora dirlo.
Il problema ufficiale del Clay Institute è formulato in un certo modo mentre il metodo di forcing sfrutta proprio quel termine che molti matematici normalmente considerano non essenziale e che spesso viene omesso nella formulazione intuitiva del problema.
Perciò si presenta una situazione paradossale: matematicamente potrebbe essere stata trovata una dimostrazione che soddisfa la formulazione letterale del problema ma non necessariamente quella che la comunità matematica considerava essere la vera domanda fisico-matematica sulle Navier–Stokes.
Scientific American sottolinea questa ambiguità: alcuni matematici potrebbero sostenere che la soluzione abbia sfruttato una sorta di “loophole”, una lacuna nella formulazione.
E il Clay Institute, naturalmente, deve ancora esaminare la questione secondo le proprie regole.
Nessun commento:
Posta un commento