Este inteligența artificială gata să demonstreze teoreme?11 min read
Noul Chat-GPT o1 de la OpenAI e un model AI conceput special pentru raționamente. Demonstrarea teoremelor matematice rămâne însă o problemă deschisă, deși progresul este semnificativ.
Computerele îi ajută pe matematicieni să calculeze încă de când au fost inventate. Dar, deși sunt instrumente de calcul excelente și pot fi programate pentru sarcini complexe, două abilități umane ale cercetătorilor sunt încă inegalabile: creativitatea cu care formulează rezultate noi relevante și ingeniozitatea raționamentului prin care le demonstrează.
Odată cu apariția inteligenței artificiale, creativitatea nu a mai părut imposibil de replicat, chiar dacă imperfect și, uneori, cu halucinații. // „Introducing OpenAI o1”, openai.com // urmărește să atace și problema raționamentului. Însă matematicienii aveau deja o soluție puternică și care nici măcar nu folosește inteligența artificială: demonstratoarele automate, numite și asistenți de demonstrație.
Verificarea demonstrațiilor
În anii 1980, matematicianul de origine rusă Vladimir Voevodsky, laureat Fields în 2002, a descoperit o eroare într-un articol propriu, publicat cu ani în urmă. Fusese atît de subtilă, încât scăpase complet specialiștilor și editorilor care i-au analizat și acceptat lucrarea.
Însă Voevodsky, care lucra la o problemă mai amplă, a descoperit-o cu ajutorul contextului și experienței. Pînă la urmă, el lucrase ani de zile la problema respectivă, în timp ce editorii, probabil, o vedeau pentru prima dată. Întâmplarea l-a făcut să caute o soluție de automatizare a verificării raționamentelor matematice, încât verdictul de corectitudine să nu mai depindă de factori umani.
// „The Coq Proof Assistant”, coq.inria.fr // unul dintre primele demonstratoare automate, dezvoltat cu ajutorul Institutului Național de Cercetare în Informatică din Franța (INRIA) și matematicianului Thierry Coquand.
Ideea nu era nouă, ci doar implementarea software. Încă din anii 1960, logicieni ca suedezul Per Martin-Löf și olandezul Arend Heyting formulaseră teorii prin care demonstrațiile și construcțiile matematice să poată fi urmărite algoritmic, similar modului în care operează un computer.
La rândul lor, ei continuau munca olandezului Luitzen E. J. Brouwer, unul dintre primii cercetători care propuseseră, la începutul secolului trecut, ideea îndrăzneață de a face întreaga matematică verificabilă pas cu pas.
Coq a evoluat spectaculos și este unul dintre cele mai populare demonstratoare automate. El a adus o adevărată revoluție a matematicii computaționale în 2008 prin verificarea completă a unei demonstrații atît de sofisticate, încât ar fi fost, practic, imposibilă pentru om: // „Formal Proof—The Four- Color Theorem”, ams.org (PDF) // Rezultatul fusese studiat cu ajutorul computerului vreme de cîteva decenii, dar abia în perioada 2005-2008 s-au făcut pașii decisivi, mulțumită lui Coq.
Un demonstrator funcționează asemănător unui limbaj de programare, dar cu un compilator special. În loc să transforme codul scris de programator în instrucțiuni pe care le poate înțelege hardware-ul, compilatorul demonstratoarelor folosește o logică preprogramată. Un raționament înseamnă o combinație anume de ipoteze și rezultate intermediare, cu ajutorul unor reguli logice, în încercarea de a ajunge la concluzia cerută. Compilatorul caută, așadar, o cale între ipoteza teoremei și concluzia ei, respectând la fiecare pas regulile de logică memorate. Dacă există, teorema este adevărată, iar pașii de la ipoteză la concluzie alcătuiesc demonstrația ei.
Așa se explică și varietatea demonstratoarelor apărute între timp. Pe lîngă Coq, s-au dezvoltat Isabelle, Agda, ACL2, F*, Lean și altele. Fiecare dintre aceste sisteme lucrează cu seturi mai mult sau mai puțin diferite în ce privește regulile logice memorate, ceea ce le face mai mult sau mai puțin potrivite pentru anumite teoreme.
Contribuția inteligenței artificiale
Îmbunătățirea demonstratoarelor automate cu ajutorul metodelor de inteligență artificială (AI) era doar o chestiune de timp. Modul de funcționare descris mai sus face verificarea demonstrațiilor o procedură algoritmică, deci programabilă și astfel, poate fi îmbunătățită cu metode specifice AI.
Totuși, nu este la fel de simplu cât ai zice Copilot. Căutarea și optimizarea căilor între ipoteza unei teoreme și concluzia ei funcționează diferit față de instrucțiunile unui program scris în Python sau C++. Detaliile stau în teoria pe care se bazează limbajele de programare și în alegerea regulilor incluse în compilator. Ambele probleme sunt mult mai sofisticate matematic pentru un demonstrator decât în cazul limbajelor de programare obișnuite.
Microsoft Research, implicați și în demonstrația teoremei celor patru culori, au lansat în 2013 propriul demonstrator, Lean, pe care îl îmbunătățesc treptat cu inteligență artificială. Inițiativa a atras atenția unuia dintre cei mai mari matematicieni ai prezentului, australianul Terence (Terry) Tao, fost copil precoce, devenit profesor universitar la UCLA cînd avea 24 ani – un record de vârstă în istoria universității californiene. (Ca fapt divers, singura teză de doctorat pe care a condus-o la UCLA aparține unei românce, // Detalii despre ea pe math.ucla.edu //)
Tao se implică în testarea și dezvoltarea Lean de câțiva ani și publică regulat actualizări, teste și încercări din munca sa pe // Disponibil pe terrytao.wordpress.com // și pe // Unde are contul @tao // După anunțul OpenAI, el // Detalii pe openai.com // alături de un fizician și alți cercetători în diverse domenii.
// Conform acestei postări: mathstodon.xyz/@tao // cîteva prompt-uri care se leagă de cercetările sale recente și folosesc Lean pentru teoreme sofisticate. Concluzia expertului a fost că, pentru un model cu un scop atît de ambițios – capacitatea de raționare în general –, o1 s-a descurcat surprinzător de bine în sarcini matematice de cel mai înalt nivel. Modelul a făcut și greșeli, însă Tao prevede că versiuni viitoare ar putea fi optimizate special pentru Lean sau alt demonstrator și integrate într-un sistem care ar ușura semnificativ munca matematicienilor.
Cât despre capacitatea AI de a demonstra teoreme, cel puțin până în prezent, aceasta este strict dependentă de regulile incluse în compilatoarele demonstratoarelor automate. Chiar și așa, formularea unor teoreme relevante rămâne exclusiv în sarcina matematicienilor.