L'avanzamento dell'intelligenza artificiale nella ricerca scientifica solleva un interrogativo cruciale: come prevenire che modelli autonomi generino risultati matematici plausibili ma sbagliati? La startup Axiom Math si propone di affrontare questa sfida, puntando a stabilire fondamenta verificate per impedire che l'AI produca "slop", ovvero contenuti formalmente convincenti ma privi di affidabilità. Il suo progetto di punta è la formalizzazione matematica AI dello Stacks Project, un'ampia opera open source fondamentale per algebra, geometria e teoria dei numeri.
Axiom Math: verificare lo Stacks Project con Lean
Lo Stacks Project, avviato nel 2005 da Johan de Jong, rappresenta un riferimento esteso per la geometria algebrica. Axiom Math ha tradotto circa 7.654 pagine di quest'opera in circa 16 milioni di righe di codice Lean, un linguaggio impiegato per redigere dimostrazioni verificabili da un proof assistant. Questo approccio implica che ogni dimostrazione non è solo esaminata da un matematico, ma è anche controllata passo dopo passo dal kernel del sistema, che ne assicura la coerenza logica.
L'obiettivo non è sostituire la matematica tradizionale con il codice, bensì convertire teoremi e definizioni in elementi verificabili meccanicamente. In tal modo, la formalizzazione matematica AI si configura come un'infrastruttura essenziale: una maggiore disponibilità di risultati verificati semplifica la costruzione di nuove conoscenze, evitando di ricominciare da capo.
Questo principio ricalca la logica delle librerie software, applicata però a dimostrazioni matematiche di elevata complessità.
Agenti AI e gerarchie flessibili
Il metodo adottato da Axiom Math è altrettanto rilevante. L'azienda ha utilizzato una flotta di agenti AI, configurati per operare in parallelo con una gerarchia flessibile. La sfida cruciale non consisteva solo nel generare codice Lean funzionale, ma nel mantenere intatte le complesse relazioni tra migliaia di definizioni, lemmi e teoremi. In un sistema matematico così interconnesso, un errore terminologico o formale può infatti compromettere l'intera struttura.
La società ha sviluppato e addestrato modelli AI proprietari, specificamente orientati alla matematica, anziché dipendere da modelli generalisti.
Questo aspetto è significativo, poiché la matematica esige non solo competenze linguistiche, ma anche precisione simbolica, una profonda memoria delle dipendenze e un certo "gusto formale", ovvero la capacità di selezionare rappresentazioni efficaci e riutilizzabili. La formalizzazione matematica AI si configura così come un test fondamentale per valutare il contributo degli agenti AI in progetti scientifici complessi, cumulativi e verificabili.
Controllo umano e livelli di formalizzazione
La libreria sviluppata da Axiom Math si struttura su due livelli. Uno di questi, denominato StacksCore, è stato sottoposto a un rigoroso controllo umano e adeguato agli standard più elevati. Questo aspetto sottolinea come il controllo umano rimanga un elemento decisivo per prevenire errori semantici, garantendo l'affidabilità dei contenuti formalizzati.
