Un team di Google DeepMind ha creato AlphaProof Nexus, un sistema di intelligenza artificiale (IA) basato su grandi modelli di linguaggio, capace di affrontare in modo autonomo problemi matematici selezionati. La nuova tecnologia cerca dimostrazioni e utilizza processi di verifica per garantire che le soluzioni siano logicamente solide. Secondo lo studio pubblicato su Science, AlphaProof Nexus ha risolto diversi problemi precedentemente irrisolti, tra cui nove dei 353 problemi di Erdős.
Reazioni degli esperti
Pablo Haya Coll, Direttore del PLN all'IIC e ricercatore alla UAM
Questo lavoro dimostra che un'architettura aperta basata su agenti di IA ha risolto autonomamente nove problemi aperti di Erdős e 44 congetture dell'On-Line Encyclopedia of Integer Sequences. Oltre ai risultati concreti, il valore del lavoro risiede nella metodologia che permette di produrre scoperta matematiche potenti in modo sistematico.
Da inizio anno, abbiamo assistito a una serie di risultati sempre più impressionanti ottenuti dall'IA in matematica. La svolta è arrivata a settembre con l'annuncio, non privo di polemiche, della risoluzione di uno dei 'problemi del millennio' (equazioni di Navier-Stokes) tramite modelli specializzati in matematica e migliaia di agenti che lavorano collaborativamente. Ormai non ci sono più dubbi che stiamo assistendo alla nascita di una nuova forma di esplorare e fare matematica.
Le capacità matematiche dei grandi modelli di linguaggio sono migliorate in modo spettacolare. Tuttavia, come ha sottolineato Terence Tao, gli obiettivi dei laboratori di IA e quelli della comunità scientifica non sempre sono allineati. I primi vogliono risolvere il maggior numero di problemi per valorizzare la loro tecnologia, mentre la comunità scientifica vuole aumentare la comprensione delle matematiche.
Josep Curto, Direttore accademico del Master in Business Intelligence e Big Data alla UOC
Quando leggiamo titoli su sistemi di IA che 'risolvono problemi aperti di matematica che erano bloccati da decenni', è facile lasciarsi trasportare dalla narrativa del progresso inevitabile. Tuttavia, analizzando i dettagli tecnici dell'articolo su AlphaProof Nexus, pubblicato su Science, ci si imbatte in un pattern tristemente comune nell'attuale panorama dell'IA: una dimostrazione impressionante di capacità tecnica offuscata da importanti inconsistenze metodologiche e un grave problema di sovraingegnerizzazione.
L'articolo presenta AlphaProof Nexus come un framework avanzato per la ricerca di dimostrazioni formali in Lean. Gli autori hanno costruito un agente 'completo' (Agente D) che combina un loop di generazione-verifica, integrazione con il provatore AlphaProof tramite apprendimento per rinforzo e un algoritmo evolutivo guidato da un sistema di votazione e rating Elo tra subagenti.
Tuttavia, l'analisi di ablazione degli autori rivela che l'Agente A, un loop base semplice tipo 'Ralph loop' che alterna la generazione del LLM con la verifica del compilatore di Lean, ha replicato gli stessi nove problemi di Erdős risolti dall'Agente D. Questo suggerisce che la complessità del framework non è ciò che spinge la scoperta; piuttosto, è la capacità base del LLM combinata con il feedback diretto e inflessibile del compilatore formale.
Dal punto di vista della gestione dei dati e delle risorse, la valutazione finanziaria dello studio è, al minimo, opaca. Le metriche di costo di inferenza mostrano che gli agenti semplificati sono più redditizi nella maggior parte dei problemi, mentre l'Agente D giustifica il suo costo solo in casi puntuali come Erdős #125. L'articolo omette dettagli rilevanti, come il fatto che i calcoli contabilizzano solo l'inferenza nelle esecuzioni riuscite e che i costi riportati per gli agenti B e D escludono il costo di inferenza di AlphaProof.
Esiste la falsa percezione che, utilizzando un linguaggio formale come Lean, l'allucinazione sia eliminata. Lean garantisce che la dimostrazione è logicamente valida per l'enunciato scritto in Lean, ma non garantisce che tale enunciato traduca fedelmente il problema matematico reale. L'articolo riconosce diversi scenari in cui gli agenti allucinano e/o incorrono in vulnerabilità di formalizzazione errata.
La vera lezione di questo lavoro è che il mercato e la ricerca dovrebbero orientarsi verso la semplicità: loop agentici puliti, potenti modelli di linguaggio e ambienti di feedback rigorosi (compilatori, esecuzioni di codice, test unitari e supervisione umana esperta). Tutto il resto, per ora, sono fuochi d'artificio evolutivi che aggiungono più complessità architettonica che risultati tangibili.
Javier Aramayona, Direttore dell'Istituto di Scienze Matematiche (ICMAT)
L'incorporazione dell'IA nella ricerca matematica ha un grande potenziale, che aumenterà man mano che queste nuove tecnologie si perfezioneranno. Tuttavia, solleva anche domande importanti sui processi associati alla ricerca, inclusa la valutazione dei risultati scientifici, l'uso dei dati inseriti nei LLM e la formazione dei giovani ricercatori nell'era dell'IA.
Soprattutto, c'è una questione di fondo molto importante sulla comprensione dei risultati di ricerca prodotti. L'obiettivo principale è garantire che i risultati siano comprensibili e utili per la comunità scientifica, oltre che per la tecnologia stessa.