Axiom Math formalno verifikovao Stacks Project u Leanu
Axiom Math je objavio formalnu verifikaciju Stacks Projecta, velike otvorene matematičke biblioteke od približno 7.654 stranice. Kompanija je sadržaj prevela u oko 16 miliona linija koda za programski jezik Lean, koje proverava alat za formalnu proveru dokaza.
Stacks Project je 2005. pokrenuo Johan de Jong kao otvoreni referentni projekat. Tokom godina doprinosi matematičara izgradili su zbirku koja se proteže od univerzitetske algebre do naprednih oblasti algebre, geometrije i teorije brojeva.
Provera ne obuhvata samo pojedinačne teoreme
Formalizacija pretvara matematički dokaz u kod. Dokazni asistent zatim proverava taj kod red po red, pa prolaz provere znači da je dokaz logički ispravan u okviru primenjenog formalnog sistema.
Poseban izazov kod Stacks Projecta bila je njegova međusobna povezanost. Definicije i teoreme oslanjaju se jedne na druge, zbog čega je bilo potrebno očuvati veze kroz približno 16 miliona linija Lean koda. Axiom navodi da su agenti imali hijerarhijsku organizaciju, ali ne i potpuno unapred propisan raspored rada: pronalazili su zadatke koji su mogli da se obavljaju paralelno.
Kompanija je za taj rad trenirala sopstvene modele za matematiku. U ranoj fazi, njen stručnjak za Lean usmeravao je agente u načinu rada na formalizaciji, dok Axiom sada smatra da su agenti preuzeli deo tog obrasca odabira i izgradnje dokaza.
Nova osnova za algebraičku geometriju i softver
Axiom ističe da formalizovana biblioteka popunjava veliku prazninu u algebraičkoj geometriji. Istraživači koji žele da proveravaju novi rad u Leanu sada imaju širu bazu postojećih, mašinski proverenih rezultata na koju mogu da se oslone.
Takav pristup ima širu primenu od matematike. Formalna verifikacija se već koristi za proveru dizajna čipova, a u Francuskoj je primenjena i za otkrivanje grešaka u softveru za obračun porodičnih naknada. Axiom želi da isti princip postane oslonac za softver koji će sve češće pisati AI agenti.
Za poslovanje je ključna pouka da automatizovano generisanje koda ne rešava pitanje pouzdanosti samo po sebi. Kada sistemi rade sa kritičnim pravilima, bezbednosnim zahtevima ili složenim zavisnostima, proverljive komponente i jasno provereni temelji ostaju važan uslov za održiv razvoj.