O inteligență de la Google a rezolvat probleme deschise de 56 de ani cu câteva sute de dolari

Un sistem de cercetare de la Google DeepMind a produs demonstrații complete, verificate de mașină, pentru nouă probleme deschise puse de matematicianul Paul Erdős, două dintre ele nerezolvate de 56 de ani. Același sistem a închis 44 de conjecturi luate din Enciclopedia online a șirurilor de numere întregi, a rezolvat o întrebare de geometrie algebrică deschisă de 15 ani și a strâns o margine cunoscută în optimizarea convexă. Cifra care atrage atenția contează mai puțin decât metoda. Fiecare dintre aceste demonstrații a fost verificată de o mașină, nu doar afirmată de ea.

Erdős, mort în 1996, a lăsat sute de întrebări precise și încăpățânate, multe ușor de enunțat și cumplit de greu de încheiat. De-a lungul deceniilor au devenit un fel de examen permanent pentru domeniu. Conjecturile de șiruri provin dintr-o bază de date publică pe care matematicienii o scormonesc după tipare, unde o formulă ghicită poate sta nedovedită ani la rând. Nu sunt teste fabricate ca să flateze un model. Sunt restanța reală a matematicii deschise.

Această distincție este toată povestea. Sistemul, numit AlphaProof Nexus, își scrie argumentele în Lean, un limbaj formal al cărui compilator respinge orice pas pe care nu îl poate confirma. O demonstrație trece sau nu trece, fără loc pentru un paragraf sigur pe sine care se dovedește apoi greșit. Pentru cine încearcă să judece dacă o ‘descoperire’ a IA este reală, aceasta este granița dintre un comunicat de presă și un rezultat.

Lecturi recomandateO scanare a 380.000 de aplicații construite cu IA găsește mii fără niciun fel de autentificare

Pe dedesubt, demonstratorul rulează pe Gemini 3.1 Pro, cu un model mai ușor care se ocupă de clasificare. Bucla este aproape plictisitoare. Modelul redactează o demonstrație în Lean, compilatorul întoarce erorile, iar acele erori hrănesc încercarea următoare. Ceea ce păstrează onestitatea este răspunsul simbolic, nu proza fluentă. Echipa a construit patru versiuni de complexitate crescândă, una capabilă să genereze și să claseze schițe de demonstrație rivale. Și totuși, versiunea cea mai simplă, o simplă buclă de model și compilator, a rezolvat singură toate cele nouă probleme ale lui Erdős.

Economia este partea surprinzătoare pe tăcute. Fiecare problemă rezolvată a costat câteva sute de dolari în timp de calcul. Întrebări care mâncaseră cariere întregi au fost închise cam la prețul unei escapade de weekend. Asta nu îl pensionează pe matematician. Cineva tot trebuie să aleagă ce probleme merită atacate, să le formuleze într-o formă pe care sistemul o poate citi și să decidă ce înseamnă un răspuns. Ceea ce se schimbă este aritmetica a ceea ce merită încercat.

Rezervele cântăresc mai greu decât titlul. Nouă rezolvate din 353 de probleme Erdős încercate este o rată de reușită de aproximativ 2,5 la sută. Cifra șirurilor, 44 din 492, stă sub nouă la sută. Autorii recunosc fără ocolișuri că cele mai multe dintre aceste probleme rămân de neatins, cu atât mai mult cele care cer teorie nouă și amplă, și că reușitele se adună acolo unde biblioteca matematică a Lean este deja adâncă. Scoate schela construită de oameni și lista aleasă de ținte, iar sistemului îi rămâne puțin teren solid.

Prudența este meritată. Într-un episod mult batjocorit, un laborator rival a anunțat că modelul său rezolvase zece probleme Erdős, până când matematicienii au arătat că răspunsurile se aflau deja în literatura publicată. Modelul le găsise, nu le demonstrase. AlphaProof Nexus este construit ca să fie imun la acea greșeală. O demonstrație în Lean a unui rezultat cunoscut rămâne valabilă, iar o demonstrație în Lean a ceva cu adevărat nou nu poate fi mimată. Demis Hassabis, aflat la conducerea DeepMind, a ținut să spună că lucrarea nu este inteligență artificială generală, o notă de prudență neobișnuită pentru o companie rareori timidă cu modelele sale.

Există un câștig mai subtil pe care cercetătorii îl subliniază. Până și eșecurile au fost utile. Pentru că fiecare demonstrație parțială este verificată formal, matematicienii au putut vedea exact ce subobiective putea și ce nu putea închide sistemul, fără să reverifice manual întregul argument. Mașina încetează să fie un oracol și devine o colaboratoare neobosită care își arată munca și indică unde se mai ascunde partea grea.

Rezultatul nu vine singur. Cade în aceeași perioadă cu o altă afirmație, a unui model de raționament rival, despre care s-a relatat că a infirmat o conjectură Erdős de circa 80 de ani din geometria discretă, o constatare pe care matematicieni în activitate au rafinat-o și au girat-o. Două laboratoare, două metode, unul sprijinit pe verificarea formală, celălalt pe lanțuri brute de raționament, au atins aceeași frontieră la câteva săptămâni distanță. Competiția nu mai este despre chatboți care sună deștept.

Lucrarea a fost detaliată într-un articol publicat luna aceasta, iar metodele se sprijină pe unelte deschise, anume Lean și biblioteca sa construită de comunitate, astfel încât grupuri din afară pot inspecta și rerula demonstrațiile în loc să creadă un blog corporativ. DeepMind nu a spus dacă sistemul va ajunge la cercetători din afara companiei. Numărul de urmărit nu este nouă. Este dacă acele 2,5 la sută devin zece, apoi douăzeci, fiindcă în ziua aceea discuția despre rostul acestor mașini va trebui să o ia de la capăt.

Mai multe articole similare

Claude instalează singur pachete npm, iar unul rău îți poate fura fișierele

Maestro: Jocul de dirijat în VR primește un DLC Star Wars și se lansează pe PSVR2

Îmblânzirea conversațiilor de grup: Cum ne reproiectează WhatsApp viața socială digitală

Spotify Premium primește 1.400 de antrenamente Peloton gratuit — fără bicicletă

SuperX lansează serverul AI XN9160-B200, valorificând GPU-ul NVIDIA Blackwell pentru a oferi performanțe de clasă supercomputer

Fitbit Air fără ecran de la Google ajunge la 99 de dolari și redă liniștea încheieturii