DeepMind razvil umetno inteligenco, ki izvaja matematične dokaze
Veliki jezikovni modeli, ki so najbolj vroča izvedba umetne inteligence v zadnjih letih, niso nikoli sloveli po dobri aritmetiki, a se tudi to popravlja. Še boljši pa so specializirani modeli, kakršen je AlphaProof, ki ga je DeepMind razvil za reševanje matematičnih zagonetk. O njem pišejo v najnovejši številki revije Nature.
AlphaProof so preizkusili na najtežjem matematičnem tekmovanju na svetu, na matematični olimpijadi za srednješolce. Na lanskem tekmovanju bi AlphaProof osvojil srebrno medaljo, le točka (od 42) bi mu bila zmanjkala do zlata.
Razlog za sorazmerno slabe rezultate običajnih modelov pri reševanju matematičnih nalog je ustroj teh modelov. Naučeni so na velikih količinah besedil in statistično ugibajo, kako bi določena besedila dopolnili, nimajo pa konceptualnega razumevanja. Lahko preberejo 500 strani Russlove knjige Principia Mathematica, a ne bodo razumeli.
Zato je DeepMind problem rešil drugače. Svoj model je naučil razmišljali matematično. Večina matematičnih dokazov je namreč zapisana v človeškem jeziku, kar računalniško umetno inteligenco zmede. Zato so naučili Gemini, da matematične dokaze in izreke prevede v formalistični zapis (Lean), torej da odstrani vso človeško navlako. Nič besed, nič stavkov, nič ločil.
Nato se je AlphaProof učil na takšni zbirki. Najprej se je prvi del modela z milijardami parametrov učil prebrati Lean in dokazovati izreke. Drugi del je komponenta, ki sodeluje pri odločanju, katere načine dokazov bo AlphaProof izvajal in kako. Tretja komponenta je simulirala delovanje človeških matematikov, saj je ustvarila variacije prvotnih izrekov in nalog, nekatere enostavne, druge posplošene, tretje zgolj podobne. Nato jih je poizkusila dokazati ali ovreči. Ta komponenta je omogočila, da se AlphaProof uči in izboljšuje.
