'Prova per intimidazione': L'IA risolve con sicurezza problemi matematici 'impossibili'. Ma può convincere i matematici di punta?

Stati Uniti - Agenzia stampa Ekhbary

'Prova per intimidazione': L'IA risolve con sicurezza problemi matematici 'impossibili'. Ma può convincere i matematici di punta?

Nel complesso mondo della matematica, dove la precisione è fondamentale, i rapidi progressi dell'intelligenza artificiale (IA) presentano una sfida nuova e inquietante. Modelli IA sofisticati, come 'o4-mini' di OpenAI, sono ora capaci di generare complesse dimostrazioni matematiche che appaiono straordinariamente convincenti, impressionando persino i matematici di spicco. Tuttavia, questo risultato solleva una domanda fondamentale: possiamo davvero fidarci di queste dimostrazioni generate dalle macchine, specialmente quando sembrano 'corrette' ma potrebbero nascondere sottili difetti o essere troppo intricate per la verifica umana?

Un incontro segreto nel 2025 ha riunito alcuni dei più eminenti matematici del mondo per testare rigorosamente l'ultimo modello linguistico di grandi dimensioni di OpenAI, 'o4-mini'. Gli esperti presenti sono rimasti stupiti dalla sorprendente somiglianza degli output del modello con il ragionamento di un matematico umano quando presenta una dimostrazione complessa. Ken Ono, stimato professore di teoria dei numeri presso l'Università della Virginia, ha commentato la performance del modello: "Non ho mai visto prima questo tipo di ragionamento nei modelli. Questo è ciò che fa uno scienziato."

Tuttavia, questa ammirazione iniziale è stata rapidamente mitigata da una crescente apprensione. All'IA veniva dato più credito di quanto meritasse? E rischiamo di accettare dimostrazioni derivate dall'IA senza comprenderne appieno le implicazioni? Lo stesso Professor Ono ha riconosciuto il potenziale del modello nel fornire risposte sicure, ma potenzialmente errate. "Se dici qualcosa con sufficiente autorità, la gente si spaventa semplicemente", ha osservato Ono. "Penso che o4-mini abbia padroneggiato l'arte della prova per intimidazione; dice tutto con così tanta sicurezza."

Storicamente, la fiducia e l'apparenza di un argomento valido erano indicatori affidabili, poiché solo i matematici più abili potevano costruire argomenti convincenti e il loro ragionamento era tipicamente solido. Questo paradigma è cambiato. Il rinomato matematico Terry Tao, vincitore della medaglia Fields dell'UCLA, ha sottolineato la crescente capacità dell'IA di imitare la correttezza. "Sfortunatamente, l'IA è molto più brava a sembrare che abbia la risposta giusta piuttosto che ottenerla realmente… giusto o sbagliato; sembreranno sempre convincenti", ha spiegato Tao a Live Science. "Se fossi un terribile matematico, saresti anche uno terribile scrittore matematico e sottolineeresti le cose sbagliate. Ma l'IA ha rotto quel segnale."

Di conseguenza, i matematici sono sempre più preoccupati che l'IA possa inondare il campo con dimostrazioni apparentemente plausibili che contengono sottili errori, difficili da rilevare per gli esseri umani. Il Professor Tao ha messo in guardia contro l'accettazione acritica degli argomenti generati dall'IA a causa del loro aspetto rigoroso. "Sfortunatamente, l'IA è molto più brava a sembrare che abbia la risposta giusta piuttosto che ottenerla realmente… giusto o sbagliato; sembreranno sempre convincenti", ha ribadito. Ha esortato a un approccio cauto verso le 'dimostrazioni' dell'IA, affermando: "Una cosa che abbiamo imparato usando le IA è che se dai loro un obiettivo, imbroglieranno pazzescamente per raggiungere l'obiettivo."

Sebbene la questione se possiamo veramente "dimostrare" congetture matematiche altamente tecniche senza comprendere le dimostrazioni possa sembrare astratta, le sue implicazioni sono profonde. Dopo tutto, se una dimostrazione non può essere ritenuta affidabile, le fondamenta per ulteriore sviluppo matematico crollano. Consideriamo il problema P versus NP, una delle principali sfide irrisolte nella matematica computazionale. In sostanza, chiede se i problemi le cui soluzioni sono facilmente verificabili siano anche facili da risolvere. Una prova definitiva potrebbe rivoluzionare la pianificazione, la logistica, la progettazione dei chip e la scoperta di farmaci. Al contrario, una prova verificabile potrebbe minare la sicurezza della maggior parte dei sistemi crittografici attuali. Queste non sono domande astratte; comportano un significativo pericolo nel mondo reale.

Potrebbe sorprendere i non matematici scoprire che le dimostrazioni matematiche derivate dall'uomo sono sempre state, in una certa misura, costrutti sociali – riguardanti la persuasione di altri nel campo della correttezza degli argomenti. Dopotutto, una dimostrazione matematica viene spesso accettata come vera quando altri matematici la analizzano e la ritengono corretta. Ciò significa che un'accettazione diffusa non garantisce che un'affermazione sia indiscutibilmente vera. Andrew Granville, un matematico dell'Università di Montreal, sospetta che anche alcune delle dimostrazioni matematiche umane più note e scrutinate possano contenere errori.

Ci sono alcune prove a sostegno di questa affermazione. "Ci sono stati alcuni articoli famosi che sono sbagliati a causa di piccoli problemi linguistici", ha detto Granville a Live Science. Forse l'esempio più noto è la dimostrazione del Teorema di Fermat di Andrew Wiles. Il teorema afferma che mentre esistono numeri interi in cui la somma di due quadrati è uguale a un terzo quadrato (come 3² + 4² = 5²), non esistono numeri interi che soddisfino la stessa relazione per i cubi o potenze superiori. Wiles ha notoriamente trascorso sette anni lavorando in quasi completo isolamento e, nel 1993, ha presentato la sua dimostrazione in una serie di conferenze a Cambridge, con grande clamore. Quando Wiles concluse la sua ultima lezione con la frase immortale "Penso che mi fermerò qui", il pubblico scoppiò in un fragoroso applauso e lo champagne fu stappato per celebrare l'impresa. I giornali di tutto il mondo proclamarono la vittoria del matematico sul problema vecchio di 350 anni. Tuttavia, durante il processo di revisione paritaria, un revisore individuò un difetto significativo nella dimostrazione di Wiles. Trascorse un altro anno lavorando al problema e alla fine lo risolse. Ma per un breve periodo, il mondo credette che la dimostrazione fosse stata risolta, quando in realtà non lo era.

Per prevenire questo tipo di problemi – in cui una dimostrazione viene accettata senza essere effettivamente corretta – c'è una mossa per rafforzare le dimostrazioni con quelle che i matematici chiamano "lingue di verifica formale". Questi programmi per computer, il cui esempio più noto è 'Lean', richiedono ai matematici di tradurre le loro dimostrazioni in un formato molto preciso. Il computer quindi esamina ogni passaggio, applicando una logica matematica rigorosa per confermare che l'argomento sia corretto al 100%. Se il computer incontra un passaggio nella dimostrazione che non gli piace, lo segnala e non va avanti. Questa formalizzazione codificata non lascia spazio alle incomprensioni linguistiche che Granville teme abbiano afflitto le dimostrazioni precedenti.

Kevin Buzzard, un matematico dell'Imperial College di Londra, è uno dei principali sostenitori della verifica formale. "Ho iniziato in questo campo perché ero preoccupato che le dimostrazioni umane fossero incomplete e errate e che noi umani stessimo facendo un cattivo lavoro nel documentare le nostre argomentazioni", ha detto Buzzard a Live Science.

Oltre a verificare le dimostrazioni umane esistenti, l'IA, lavorando in congiunzione con programmi come Lean, potrebbe cambiare le regole del gioco, hanno detto i matematici. "Se costringiamo l'output dell'IA a produrre cose in una lingua formalmente verificata, allora questo, in linea di principio, risolve la maggior parte del problema" delle IA che producono dimostrazioni dall'aspetto convincente ma alla fine errate, ha detto Tao. Ha aggiunto: "Ci sono articoli in matematica in cui nessuno capisce l'intero articolo. Sai, c'è un articolo con 20 autori e ogni autore capisce la sua parte. Nessuno capisce l'intera cosa. E va bene così. È così che funziona". Buzzard ha concordato: "Ti piacerebbe pensare che forse possiamo ottenere..."

Agenzia stampa Ekhbary