Cele nouă demonstrații DeepMind, testate pentru noutate

O demonstrație matematică poate fi elegantă și totuși să ascundă o lacună pe care nimeni să nu o observe ani la rând. Agentul AI AlphaProof Nexus, creat de Google DeepMind, a produs demonstrații pentru nouă probleme formulate de Paul Erdős, iar un program a verificat fiecare pas. Rezultatele au apărut mai întâi într-un preprint din mai (arXiv), apoi, după evaluarea inter pares, în revista Science, pe 8 octombrie (Science). Programul putea confirma logica demonstrațiilor; matematicienilor le revenea să stabilească dacă ele aduceau ceva nou.

Un arbitru care nu poate fi impresionat

Chatboții pot scrie matematică ce pare corectă. Un paragraf sigur pe sine poate ascunde un pas lipsă, pe care doar un cititor atent îl observă. AlphaProof Nexus evită această capcană lucrând în Lean, un limbaj de programare în care definițiile, afirmațiile și demonstrațiile sunt formulate atât de precis, încât un computer le poate verifica.

Lean funcționează ca un arbitru care citește fiecare rând al unei demonstrații și aplică reguli fixe. Stilul nu contează. Dacă un pas nu decurge din cei anteriori, demonstrația este respinsă, oricât de elegantă ar fi în rest.

Echipa descrie agentul ca pe un sistem care caută demonstrații scrise în Lean. Cercetătorii i-au dat acces și la AlphaProof, un sistem DeepMind mai vechi, creat special pentru demonstrații. În testele echipei, o variantă mai simplă a obținut aceleași rezultate: un model lingvistic asociat cu Lean, fără AlphaProof, a demonstrat toate cele nouă afirmații ale lui Erdős (The Decoder). Pentru aceste probleme, componenta specializată nu s-a dovedit necesară.

Lucrarea prezintă demonstrații verificate pentru cele nouă afirmații ale lui Erdős și pentru 44 de conjecturi, adică afirmații considerate adevărate, dar încă nedemonstrate, din Online Encyclopedia of Integer Sequences, un vast catalog de tipare numerice (Science). Printre rezultatele legate de Erdős se află o problemă în două părți despre numere întregi, formulată de Erdős și András Sárközy în 1970. A rămas nerezolvată mai bine de jumătate de secol (ABC).

Ce nu poate vedea arbitrul

Garanția oferită de Lean are limite precise. Sistemul confirmă că demonstrația stabilește afirmația exact așa cum a fost scrisă în cod. Trei întrebări rămân în afara verificării: dacă formularea din cod surprinde ce a vrut să spună Erdős, dacă altcineva a răspuns deja la întrebare și dacă răspunsul aduce ceva nou.

Problema din 1970 arată de ce contează ultimele două întrebări. A doua parte a problemei o implică pe prima, astfel că o singură demonstrație le rezolvă pe amândouă. După ce demonstrațiile agentului au fost făcute publice, s-a constatat că o modificare minoră a unei construcții din articolul original din 1970 răspunde și ea ambelor părți (arXiv). Demonstrațiile agentului erau corecte. Problema fusese pur și simplu mai aproape de rezolvare decât sugera eticheta „nerezolvată”.

Pentru a observa astfel de lucruri sunt necesari oameni care cunosc domeniul. Gergely Bérczi, matematician la Universitatea Aarhus din Danemarca și unul dintre autorii lucrării, a contribuit la alegerea problemelor potrivite și la validarea soluțiilor (Aarhus University). A ajutat și la redactarea unor versiuni ale demonstrațiilor pe care le pot urmări cititorii. Lean a verificat fiecare pas; Bérczi și colegii săi au judecat ce rezultă din toți acești pași.

Această împărțire a muncii diferențiază studiul de un reper atins luna trecută. Atunci, Claude, sistemul Anthropic, a transpus în Lean demonstrația deja cunoscută a Marii teoreme a lui Fermat (To Brief). Traducerea unei demonstrații celebre nu ridică întrebări despre noutate. Căutarea printre afirmații considerate nerezolvate ridică asemenea întrebări, iar verificarea noutății devine esențială.

Echipa și-a publicat fișierele demonstrațiilor, astfel încât alți cercetători să le poată verifica folosind același arbitru (GitHub). Studiul arată un progres bine delimitat: un agent AI a produs demonstrații verificabile de computer pentru unele afirmații pe care matematicienii le considerau nerezolvate, iar garanția se aplică afirmațiilor exact așa cum au fost scrise în Lean. Matematicienilor care au analizat demonstrațiile le-a revenit să stabilească ce adaugă fiecare la cunoașterea matematică.