Axiom Math veic milzīgā Stacks Project formālo pārbaudi, lai nodrošinātu AI vadītu matemātiku

Attēls: TechCrunch · Avots

Axiom Math ir formāli pārbaudījusi plašo Stacks Project, izmantojot AI aģentus, radot stabilu pamatu uzticamu matemātisko pierādījumu izveidei un atverot ceļu uzticamai ar AI atbalstītai matemātikai un programmatūras izstrādei.

Ātrā mākslīgā intelekta ģenerēto matemātisko pierādījumu plūsma ir radījusi bažas par šādu darbu uzticamību un precizitāti. Pēdējos mēnešos AI modeļi ir iesnieguši simtiem manuskriptu, apgalvojot, ka tie atrisinājuši sarežģītas matemātiskas problēmas, taču pat parastās datoru pārbaudes reizēm nav spējušas atklāt kļūdas. Lai risinātu šo izaicinājumu, 1,6 miljardu dolāru vērtā jaunuzņēmuma Axiom Math uzmanības centrā ir stingri verificētu matemātisko pamatu izveide, izmantojot formālu pārbaudi, nodrošinot, ka AI sistēmas var uzticami ģenerēt un izmantot pareizu matemātiku.

2026. gada 5. novembrī Axiom Math paziņoja par nozīmīgu sasniegumu: Stacks Project, vienu no lielākajiem un cienījamākajiem matemātikas kompendiumiem, formālu pārbaudi. Šis projekts, kas tika uzsākts 2005. gadā Kolumbijas matemātiķa Johan de Jong vadībā, ir attīstījies kā atvērtā koda, sadarbības projekts, aptverot plašu tēmu loku no algebras līdz ģeometrijai un skaitļu teorijai, aptuveni 7 654 lappusēs.

Axiom AI aģenti pārtulkoja visu Stacks Project aptuveni 16 miljonos rindkopu Lean valodā, kas ir formālas pierādīšanas valoda. Šī tulkošana ļāva pierādījumu asistenta programmatūrai rūpīgi pārbaudīt katru pierādījumu, apstiprinot loģisko pamatotību visā plašajā un cieši savienotajā darbā. Šo saišu integritātes nodrošināšana bija nozīmīgs izaicinājums, ko valdes priekšsēdētāja Carina Hong salīdzināja ar smalku struktūru saskaņošanu milzīgā kopumā bez pretrunām.

Uzņēmumu 2025. gada martā dibināja Hong, bijusī Stanfordas matemātikas doktorantūras kandidāte. Šogad agrāk uzņēmums piesaistīja 200 miljonu dolāru A sērijas finansējumu, ko vadīja Menlo Ventures. Uzņēmuma pieeja paredzēja sniegt AI aģentiem elastīgu sadarbības ietvaru, kas ļauj paralēli strādāt pie dažādiem uzdevumiem, vienlaikus saglabājot kopējo hierarhisko struktūru, lai uzturētu atkarības Stacks Project.

Atšķirībā no daudziem citiem pārbaudes iniciatīvām, Axiom ieguldīja laiku un resursus, lai apmācītu savus AI modeļus speciāli matemātikas un formalizācijas niansēs, efektīvi mācot aģentiem attīstīt matemātisku „gaumi“. Šis progress aizpilda būtisku plaisu formalizētajā matemātikā, īpaši algebraiskajā ģeometrijā, nodrošinot plašu un uzticamu pamatu nākotnes formāliem pierādījumiem, izmantojot Lean.

Papildus tīrai matemātikai Axiom redz savus verificētos pamatus kā būtiskus programmatūras izstrādē, it īpaši ar AI pieaugošu koda ģenerēšanu. Balstot AI rezultātus stingri pārbaudītā matemātikā, uzņēmums cenšas samazināt kļūdas un drošības ievainojamības, kas raksturīgas AI rakstītajiem kodiem.

Matemātiķi, piemēram, Fields Medal laureāts Terence Tao, ir atzinīgi novērtējuši šādu formalizāciju, atzīmējot, ka verificēti pierādījumi ļauj radīt vēl vairāk verificētu pierādījumu. Axiom gadījumā verificētais Stacks Project ir atkārtoti izmantojama platforma, uz kuras AI aģenti var būvēt jaunu matemātisku un zinātnisku infrastruktūru.

Valdes priekšsēdētāja Hong uzsver, ka AI nākotne pētniecībā un inženierzinātnēs ir atkarīga no pieejamām, atkārtoti izmantojamām un rūpīgi veidotām zināšanu kopām, lai novērstu kļūdu vai „netīrumu“ izplatīšanos. Viņa izaicina citus programmēšanas uzņēmumus mēģināt veikt formālu pārbaudi līdzīgā apjomā un prognozē, ka sadarbības AI aģenti, kas strādā asinhroni un stratēģiski, kļūs par standartu zinātnes un programmatūras attīstībā.

Apvienojot cilvēka matemātisko stingrību ar AI aprēķinu jaudu, Axiom Math darbs pie Stacks Project nozīmē nozīmīgu soli uzticamā AI atbalstītā matemātikā un programmatūras radīšanā, kas iespējams būtiski mainīs to, kā nākotnē formalizē un paplašina sarežģītas zināšanu jomas.