i matematici stanno incorporando assistenti di intelligenza artificiale nel loro lavoro
Gli strumenti di intelligenza artificiale stanno aiutando i matematici a sviluppare e verificare dimostrazioni complesse
I matematici esplorano le idee proponendo congetture e dimostrando teoremi. Per secoli, hanno costruito queste dimostrazioni riga per riga con estrema attenzione, e la maggior parte dei ricercatori matematici continua a lavorare così ancora oggi. Ma l’intelligenza artificiale è sul punto di cambiare radicalmente questo processo.
L’evoluzione dell’intelligenza artificiale sta trasformando il modo in cui i matematici sviluppano e dimostrano teoremi matematici complessi, con nuovi co-piloti di intelligenza artificiale che emergono come potenti strumenti collaborativi che potrebbero potenzialmente estendere le capacità matematiche umane.
Matematica e IA
Gli assistenti di intelligenza artificiale soprannominati “co-pilot” stanno iniziando ad aiutare i matematici a sviluppare dimostrazioni, con la concreta possibilità che in futuro possano aiutare gli esseri umani a rispondere ad alcuni problemi attualmente al di là delle capacità della mente umana. Aiutando i matematici a sviluppare e verificare dimostrazioni complesse, questi “assistenti intelligenti” stanno segnando il cambiamento più significativo nei metodi di ricerca matematica dal sistema di algebra computerizzata.
Un co-pilot come assistente
Un promettente co-pilot di intelligenza artificiale è in fase di sviluppo presso il California Institute of Technology. Può proporre automaticamente i passaggi successivi in una dimostrazione e aiutare a completare obiettivi matematici intermedi, contribuendo a costruire il tessuto logico connettivo tra passaggi più ampi.
“Quando sto sviluppando una dimostrazione, questo nuovo co-pilota mi offre molteplici suggerimenti per andare avanti”, spiega Animashree Anandkumar, professoressa di scienze informatiche e matematiche al Caltech. Insieme al suo team, Anandkumar ha presentato il co-pilot di intelligenza artificiale in un recente studio pre-pubblicazione, che non è ancora stato sottoposto alla revisione peer-to-peer propria delle ricerche scientifiche. E’ piuttosto convinta che i suggerimenti offerti dal co-pilot siano “tutti corretti” e che la revisione lo confermerà.
Cos’è un co-pilot
Il co-pilot è un modello di linguaggio di grandi dimensioni (LLM – Large Language Model), lo stesso tipo di sistema di apprendimento automatico alla base di ChatGPT di OpenAI e Gemini di Google, per intenderci.
Anche se il suo addestramento è diverso, è simile alla tecnologia che alimenta AlphaProof e AlphaGeometry 2 di Google, entrambi i quali hanno generato dimostrazioni matematiche complesse a un livello di medaglia d’argento ai recenti Giochi Olimpici Internazionali di Matematica (IMO) per i migliori studenti delle scuole superiori.
E sebbene gli LLM possano anche generare quello che, in senso tecnico, è definito “spazzatura” (risultati non dettagliati), i suggerimenti errati di un co-pilot sono comunque verificati e respinti, quando non di adeguata qualità. Nel caso del co-pilot sviluppato dal Caltech, questo è possibile grazie al software in cui opera l’intelligenza artificiale, chiamato Lean, che utilizza una rigorosa logica matematica per vagliare le affermazioni valide.
“Non sbaglia mai”
Negli ultimi anni, Lean è diventato sempre più popolare e oggi vanta una base di utenti piccola ma in crescita tra gli esperti di calcolo e i matematici puri. Si tratta di un software open-source che consente ai matematici di inserire i loro calcoli e studi mediante codifica, un processo noto come “formalizzazione”.
Il vantaggio di usare Lean è che non sbaglia mai. *A differenza della matematica tradizionale dove l’errore umano è possibile, Lean verifica automaticamente l’accuratezza delle affermazioni, diversamente da quello che accade nella matematica tradizionale, cosiddetta informale, dove le revisione avviene peer-to-peer da parte di altri colleghi studiosi, che controllano minuziosamente pagine e pagine di affermazioni e studi. Un processo che, chiaramente, è soggetto a errori umani e anche alla possibilità che alcuni errori possano sfuggire. Un’eventualità che non accade con Lean o con i sistemi affini.
E’ tutto oro?
Nonostante i potenziali benefici, l’adozione diffusa degli strumenti matematici di intelligenza artificiale deve affrontare diverse difficoltà:
- Molti accademici non hanno ancora abbracciato Lean a causa dei suoi requisiti di codifica
- Convertire i concetti matematici in codice può essere time-consuming e richiede dettagli estesi
- Gli attuali sistemi di intelligenza artificiale, pur impressionanti, non hanno ancora raggiunto il livello di capacità necessario per la ricerca matematica complessa
E’ indubbio che l’integrazione dei co-pilot di intelligenza artificiale potrebbe trasformare radicalmente il modo in cui viene condotta la ricerca matematica. Gli strumenti di intelligenza artificiale potrebbero consentire a gruppi più ampi di matematici di collaborare su problemi complessi, questi sistemi potrebbero aiutare ad affrontare sfide note come i Problemi del Millennio – David Silver di Google DeepMind suggerisce che, entro tre anni, le partnership AI-umane potrebbero avvicinarsi a problemi complessi come P contro NP, ma l’integrazione piena e pienamente efficace ha ancora bisogno di molto lavoro.
Il cambiamento culturale
Soprattutto, ha bisogno di un cambiamento culturale: l’evoluzione della pratica matematica attraverso l’assistenza dell’intelligenza artificiale indica una trasformazione fondamentale nel modo in cui viene svolto il lavoro matematico. Attualmente, i giovani matematici stanno sempre più abbracciando i sistemi di intelligenza artificiale per avvantaggiarsene. Per certi versi, questa transizione sembra rispecchiare l’impatto rivoluzionario delle calcolatrici elettroniche sul calcolo matematico
Il vantaggio dei co-pilot di intelligenza artificiale è soprattutto nel fatto che potrebbero consentire un approccio più collaborativo alla ricerca matematica, sfidando l’immagine tradizionale della matematica come attività solitaria
Ad ogno modo, mentre gli attuali assistenti matematici di intelligenza artificiale mostrano promesse di futuro possibile, il loro vero potenziale risiede nell’aumentare le capacità umane piuttosto che sostituire i matematici, potenzialmente conducendo a progressi in problemi matematici precedentemente intrattabili.
fonte: Caltech I American Scientific
immagine di copertina: Elchinator via Pixabay
autore: Barbara Marcotulli
Maker Faire Rome – The European Edition, promossa dalla Camera di Commercio di Roma, si impegna fin dalla sua prima edizione a rendere l’innovazione accessibile e fruibile, offrendo contenuti e informazioni in un blog sempre aggiornato e ricco di opportunità per curiosi, maker, PMI e aziende che vogliono arricchire le proprie conoscenze ed espandere la propria attività, in Italia e all’estero.
Seguici sui nostri social (Facebook, Instagram, Twitter, LinkedIn, YouTube) e iscriviti alla nostra newsletter: ti forniremo solo le informazioni giuste per approfondire i temi di tuo interesse.
