Ce s-a întâmplat
Într-o realizare istorică pentru domeniul matematicii computaționale, startup-ul Axiom Math a anunțat verificarea formală a unei demonstrații extrem de dificile utilizând instrumente de inteligență artificială. Echipa a reușit să „traducă” și să valideze automat teorema 2.4.6 din lucrarea „Higher-order Fourier Analysis” de Terence Tao, Ben Green și Tamar Ziegler. Această teoremă, care tratează distribuția numerelor prime în progresii aritmetice, era considerată până acum prea densă și abstractă pentru a fi procesată integral de sistemele informatice actuale.
Context tehnologic
Procesul utilizat nu se bazează pe modele de limbaj generativ (precum ChatGPT) în sensul lor clasic, ci pe verificarea formală. Aceasta presupune scrierea matematicii într-un limbaj de programare specializat (în acest caz, Lean), pe care un computer îl poate procesa logic pas cu pas.
Spre deosebire de un AI care „ghicește” următorul cuvânt, sistemele de verificare formală funcționează ca un judecător logic infailibil. Provocarea majoră a fost „formalizarea”: transformarea limbajului uman matematic, plin de intuiții și omisiuni lăsate pe seama cititorului, într-un cod strict pe care sistemul Lean să îl poată valida fără urmă de îndoială.
De ce contează
Matematica modernă a devenit atât de complexă încât chiar și cei mai buni experți umani pot petrece ani de zile verificând o singură demonstrație, existând mereu riscul unor erori subtile.
1. Certitudine absolută: Odată ce o demonstrație este acceptată de un verificator formal, probabilitatea unei erori logice este practic zero.
2. Accelerarea cercetării: AI-ul poate prelua munca de rutină a verificării, permițând matematicienilor să se concentreze pe crearea de noi teorii.
3. Biblioteci digitale: Această reușită contribuie la crearea unei biblioteci de cunoștințe matematice verificabile, care pot fi folosite ca „piese de Lego” pentru viitoare descoperiri.
Impact
Pe termen scurt, vom asista la o colaborare mai strânsă între matematicieni și inginerii AI pentru a „codifica” marile teoreme ale secolului XX. Pe termen mediu, această tehnologie va permite dezvoltarea unor sisteme AI capabile de raționament logic pur, eliminând „halucinațiile” frecvente în modelele actuale. Acest lucru este esențial în domenii critice precum securitatea cibernetică, proiectarea hardware-ului și explorarea spațială, unde eroarea nu este o opțiune.
Ce urmează
Următorul pas este integrarea modelelor LLM (Large Language Models) cu verificatoarele formale. În loc ca oamenii să scrie manual codul Lean, AI-ul va putea să citească o lucrare PDF, să o formalizeze singur și să identifice dacă există erori logice. Ne îndreptăm către o eră a „matematicii asistate”, unde descoperirile vor fi limitate doar de creativitatea umană, nu de capacitatea noastră limitată de a verifica manual mii de pagini de calcule.
Surse
- IEEE Spectrum – Artificial Intelligence
- Axiom Math Official Documentation