Axiom Math je sporočil, da je formalno verificiral Stacks Project, eno najobsežnejših zbirk matematike, ki so jo napisali ljudje. Podjetje je približno 7654 strani gradiva pretvorilo v okoli 16 milijonov vrstic računalniško preverjene kode v jeziku Lean.
Stacks Project je leta 2005 kot odprtokodni vir začel Johan de Jong z Univerze Columbia. Od takrat so ga matematiki dopolnjevali z rezultati od univerzitetne algebre do zahtevnejših tem iz algebre, geometrije in teorije števil. Matematik Peter Woit s Columbie je projekt primerjal s znamenitimi knjigami skupine Bourbaki, ki so v 20. stoletju gradile matematiko iz njenih temeljev.
Formalna verifikacija pomeni, da matematiki dokaz zapišejo kot programsko kodo, nato pa ga tako imenovani pomočnik za dokazovanje preveri vrstico za vrstico. Če dokaz uspešno prestane preverjanje, ga lahko obravnavajo kot logično veljavnega.
Preveriti je bilo treba tudi povezave med dokazi
Pri Stacks Projectu ni bilo dovolj preveriti posameznih izrekov. Definicije in izreki so medsebojno povezani, posamezni rezultati pa se naslanjajo na predhodne. Ekipa Axioma je morala te povezave ohraniti v vseh približno 16 milijonih vrstic kode Lean.
»Velike in občutljive stvari v življenju običajno ne sodijo skupaj,« je za TechCrunch dejala izvršna direktorica Axioma Carina Hong. Stacks je po njenih besedah zbirka matematičnih rezultatov, ki predstavlja temelj matematike, zato morajo biti izreki med seboj skladni, definicije pa si ne smejo nasprotovati.
Hong, stara 25 let, je pred ustanovitvijo podjetja marca 2025 zapustila doktorski študij matematike na Stanfordu. Axiom je marca letos zbral 200 milijonov dolarjev v krogu financiranja serije A, ki ga je vodil Menlo Ventures. Startup je vreden 1,6 milijarde dolarjev.
Agenti so delo razdelili med seboj
Axiom je za pretvorbo Stacks Projecta uporabil skupino agentov umetne inteligence. Po besedah člana tehničnega osebja Ashvina Swaminathana so agentom določili okvirno hierarhijo, niso pa jim natančno predpisali vsake naloge. Agenti so sami iskali opravila, ki so jih lahko izvajali vzporedno.
Podjetje je razvilo tudi lastne modele, prilagojene matematiki. Hong je povedala, da je ekipa sprva uporabila strokovnjaka za Lean, ki je agente usmerjal pri presoji kakovosti formalizacij. Sčasoma naj bi agenti takšno presojo razvili sami.
Swaminathan je dejal, da formalizirana matematika doslej ni dobro pokrivala algebrske geometrije. Raziskovalci, ki so želeli novo delo na tem področju preverjati z Leanom, so imeli po njegovih besedah malo gradnikov, na katere bi se lahko oprli. Z zdaj formaliziranim Stacks Projectom se to spreminja.
Axiom cilja tudi na razvoj programske opreme
Axiom trdi, da lahko vsak preverjen matematični rezultat postane gradnik za prihodnje dokaze. Matematik Terence Tao z UCLA in prejemnik Fieldsove medalje je to povzel z besedami: »Več formaliziranih dokazov kot imate, več formaliziranih dokazov lahko ustvarite.«
Podjetje ne meri le na matematike. Axiom želi z verificiranimi temelji podpreti tudi programsko opremo, saj razvijalci težko zagotavljajo, da je koda brez napak in varnostnih pomanjkljivosti. Po oceni podjetja bo to še posebej pomembno, ker agenti umetne inteligence pišejo vse več kode.
»Verjamemo, da je matematika področje, na katerem začnete graditi te stvari, in da je to prenosljiva veščina,« je povedal Swaminathan. Agenti lahko po njegovih besedah berejo Axiomovo kodo, jo razumejo in na njej gradijo novo infrastrukturo.
Hong meni, da bodo agenti za delo potrebovali kakovostno in ponovno uporabljivo zbirko znanja. »Želite, da imajo agenti knjižnico, na kateri lahko gradijo in širijo meje,« je dejala. Ob tem je podjetjem, ki razvijajo orodja za programiranje, javno predlagala, naj se lotijo formalizacije v takšnem obsegu.
