Andriy Onufriyenko / Getty Images

Este inteligența artificială gata să demonstreze teoreme?11 min read

De Adrian Manea 10.10.2024

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. Modelul o1 de la OpenAI// „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.

Astfel a apărut Coq,// „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: teorema celor patru culori.// „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, Monica Vișan.// 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 blogul personal// Disponibil pe terrytao.wordpress.com // și pe Mastodon.// Unde are contul @tao // După anunțul OpenAI, el a fost invitat să testeze o1,// Detalii pe openai.com // alături de un fizician și alți cercetători în diverse domenii. 

Matematicianul i-a propus// 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.



Text de

Adrian Manea

Adrian Manea este matematician și profesor, fondator al Poligon Educational, proiect prin care îmbină matematica și științele cu istoria, filosofia, literatura și jocurile. Scrie și pe Substack, Laturi ale științei.

TEHNOLOGIE|OVERVIEW

Revoluția procesoarelor. De la x86 și ARM la cipuri pentru AI

De
Procesoarele pe arhitectura ARM domină piața portabilelor și, mai nou, câștigă teren și pe cea a laptopurilor care rulează Windows. Acest lucru începe să fie îngrijorător pentru producătorii de procesoare pe arhitectura x86, dar ei sunt mai preocupați de industria inteligenței artificiale. 
TEHNOLOGIE|OVERVIEW

Inundațiile din Valencia ar fi trebuit prevenite de o lucrare inginerească gigantică. Ceva însă n-a funcționat cum trebuie

De
Valencia a fost lovită de cele mai rele inundații din acest secol. Cu 60 de ani în urmă, râul Turia a fost mutat din centrul orașului pentru a preveni astfel de dezastre, dar nimeni n-a prevăzut amploarea pe care o pot lua inundațiile.
ȘTIINȚĂ|FYI

Universul timpuriu surprins de telescopul James Webb: quasari solitari și găuri negre supermasive

De
Un studiu recent arată că, la doar câteva sute de milioane de ani după Big Bang, universul era mult mai complex decât se credea, cu quasari solitari alimentați de găuri negre supermasive.
SĂNĂTATE|OVERVIEW

Fertilizarea in vitro, „un carusel de emoții”. Efectele psihologice ale tratamentului FIV

De
Fertilizarea in vitro este principala procedură la care apelează cuplurile care își doresc un copil, dar nu pot să-l aibă pe cale naturală. Pe lângă schimbările fizice din corpul persoanelor supuse tratamentului, ea are are și consecințe psihologice.