Fondatorul Cardano, Charles Hoskinson, a declarat pe 9 septembrie că inteligența artificială a avansat mai mult în matematica formală decât se aștepta.
Comentariile sale au urmat afirmației OpenAI conform căreia un sistem intern a produs o soluție la Problema Premiului Mileniului Navier–Stokes.
În timpul unei emisiuni, Hoskinson a numit capabilitățile raportate „destul de remarcabile”. Cu toate acestea, el a abordat și întrebări nerezolvate despre proveniența lucrării și confidențialitatea cercetărilor trimise serviciilor de AI bazate pe cloud.
Hoskinson a declarat că inițial se aștepta ca sistemele formale să ajute echipe mai mari de matematicieni să colaboreze și să verifice demonstrațiile scrise de oameni. Nu se aștepta ca modelele lingvistice mari să genereze singure demonstrații complete atât de curând.
„Nu am anticipat niciodată măsura în care AI va interveni”, a spus Hoskinson. El a adăugat că ideea ca AI să scrie integral o demonstrație părea anterior „destul de îndepărtată”.
Hoskinson are o legătură directă cu cercetarea în matematica formală. În 2021, el a donat 20 de milioane de dolari Universității Carnegie Mellon pentru a înființa Centrul Hoskinson pentru Matematică Formală, conform anunțului universității.
Ultimele sale comentarii se încadrează și în experimentarea mai amplă a Cardano cu inteligența artificială. Așa cum a raportat anterior crypto.news, Hoskinson a apărat experimentele cu agenți AI Cardano care implică comunicații, activitatea comunității și ecosistemul Midnight axat pe confidențialitate.
OpenAI și-a publicat cercetarea pe 8 septembrie. Compania a declarat că un model intern a coordonat aproximativ 10.000 de agenți și a produs o soluție propusă după 88 de ore. GPT-6 Astra a petrecut apoi încă 17 ore formalizând și verificând argumentul în Lean.
Demonstrația încearcă să stabilească faptul că un fluid inițial lin și staționar poate dezvolta o singularitate într-un timp finit atunci când este supus unei forțe externe netede. OpenAI a declarat că aceasta satisface afirmațiile C și D din formularea oficială a Premiului Mileniului.
Compania a lansat, de asemenea, o lucrare analitică și cod Lean. O formalizare Lean oferă o verificare care poate fi verificată de mașină, că pașii codificați rezultă din ipotezele declarate. Nu stabilește independent că fiecare definiție și ipoteză reprezintă cu exactitate problema matematică intenționată.
OpenAI a declarat că nu intenționează să solicite premiul asociat de 1 milion de dolari. Compania și-a descris totuși lucrarea ca o rezolvare a problemei.
Institutul de Matematică Clay încă etichetează problema Navier–Stokes ca fiind „nerezolvată”. Site-ul său web nu recunoscuse dovada propusă de OpenAI ca soluție acceptată la momentul raportării.
Clay nu acceptă soluții propuse prin trimiteri directe. Conform regulilor sale, o soluție trebuie să apară într-o publicație calificată. Apoi trebuie să treacă cel puțin doi ani, iar lucrarea trebuie să obțină acceptarea generală din partea comunității matematice globale.
Acest proces înseamnă că anunțul OpenAI și dovada formală nu constituie o recunoaștere instituțională imediată. Matematicienii trebuie să examineze dacă construcția satisface enunțul precis al problemei și dacă utilizarea forțelor externe răspunde la întrebare așa cum este înțeleasă în mod obișnuit.
Anunțul a atras, de asemenea, atenția asupra matematicianului Tristan Buckmaster de la Universitatea din New York și a cercetătorului Anthropic Levent Alpöge. Cercetătorii lucraseră la un rezultat legat de ecuația lui Euler folosind o abordare de forțare.
Buckmaster a pus la îndoială dacă lucrările private introduse în sistemul Codex al OpenAI ar fi putut contribui la rezultatul companiei. S-a abținut să pretindă o abatere dovedită, spunând: „Nu știu dacă datele noastre au fost folosite.”
OpenAI a negat accesul la lucrările lor specifice. Cu toate acestea, compania a declarat că nu poate exclude complet posibilitatea ca datele de-identificate din utilizarea produsului lor să fi contribuit la îmbunătățirea modelelor sale. OpenAI a susținut că dovada sa a fost dezvoltată independent și a diferit de lucrarea cercetătorilor.
Hoskinson a argumentat că disputa ar trebui să-i îngrijoreze pe cercetătorii care gestionează idei nepublicate. El a spus că academicienii care utilizează servicii centralizate de AI ar trebui să ia în considerare dacă prompturile, notele și jurnalele de cercetare rămân confidențiale.
Următoarea fază va implica examinarea publică a lucrării OpenAI și a formalizării Lean. Până când specialiștii vor revizui ipotezele și condițiile formale ale lui Clay vor fi îndeplinite, lucrarea rămâne o soluție revendicată, mai degrabă decât o rezolvare recunoscută.
ADA