OpenAI dokazima iz matematike nedostaje proverljiv ljudski kontekst
OpenAI je objavio 719 rukopisa sa navodnim rešenjima nekih od najtežih otvorenih matematičkih problema, ali je uz samo 10 njih dostupan lanac zaključivanja modela, dok 42% dokaza nije prošlo formalizaciju. Objavu je pratila reakcija Advisory Group on Mathematics and Artificial Intelligence, grupe od devet istraživača koju ugošćava Institute for Advanced Study pri Univerzitetu Prinston.
Smernice i objavljeni materijal nisu u potpunosti usklađeni
AGMAI je krajem septembra objavio smernice za laboratorije koje koriste granične modele na matematičkim problemima. Prva preporuka bila je da se napredno otvoreno matematičko istraživanje ne testira na vlasničkim modelima. OpenAI je, međutim, izričito naveo da svoje vlasničke modele procenjuje na otvorenim istraživačkim problemima iz matematike.
Grupa je ocenila da će matematička zajednica na kraju proceniti u kojoj su meri preporuke uspešno primenjene. OpenAI je ispunio deo načela: rezultate je objavio brzo i pružio određene informacije o načinu na koji su modeli došli do zaključaka. Ipak, ograničena dostupnost lanca zaključivanja i nepotpuna formalizacija ostavljaju otvoreno pitanje odgovornosti za ljudsko razumevanje rezultata.
Za takve objave AGMAI je predložio i finansijsku podršku matematičarima koji bi proveravali i tumačili rezultate. Terens Tao je upozorio da osobe koje podstiču modele da reše ciljani problem često ne mogu da odgovore na pitanja o rezultatu, održe predavanje ili ga uključe u širi rad discipline.
Rizik nastaje pri prelasku iz teksta u formalni kod
Istraživači Univerziteta Kembridž i King’s College London objavili su rad koji ispituje odnos između objašnjenja na prirodnom jeziku i Lean koda za rešenje problema izvedenog iz Navje-Stoksovih jednačina. Lean je programski jezik u kojem se dokaz može proveriti kompajliranjem, ali njegova potvrda ne rešava automatski pitanje da li se kod i tekstualno obrazloženje zaista poklapaju.
Autori su dokumentovali najmanje dva nesklada između prirodnojezičkog dokaza koji je ponudio OpenAI i formalnog Lean zapisa. Ti nalazi sami po sebi ne pobijaju nijedno rešenje, ali pokazuju zašto automatski preveden formalni dokaz ne bi trebalo prihvatiti bez uobičajene stručne recenzije i detaljne provere.
AGMAI je zato tražio mašinski čitljive metapodatke koji bi povezali tekstualne i formalne artefakte, a takvi podaci nisu bili deo ove objave. U širem kontekstu saradnje velikih AI laboratorija, OpenAI ostaje važan akter na AI događajima potvrđuje da OpenAI ostaje važan akter na događajima posvećenim razvoju veštačke inteligencije.
Šta ovo znači za organizacije
U matematici vrednost novog rezultata ne čini samo tačan završni iskaz, već i mogućnost da ga ljudi provere, objasne, prenesu na druge probleme i primene. Profesorka Harvarda Melani Vud istakla je da pri objavljivanju modelskog rešenja ljudsko razumevanje često još ne postoji i da tada tek počinje rad.
Za poslovne timove to je praktična granica pri uvođenju AI alata u procese sa visokim ulozima: rezultat modela treba tretirati kao materijal za proveru, uz jasnu sledljivost između objašnjenja i formalnih ili operativnih artefakata, kao i odgovorne stručnjake koji mogu da ga brane pred korisnicima i revizorima.