Axiom Math saavutab laiahaardelise Stacks Projecti ametliku verifitseerimise turvaliseks AI-põhiseks matemaatikaks

Pilt: TechCrunch · Allikas

Axiom Math on tehisintellekti abil ametlikult verifitseerinud ulatusliku Stacks Projecti, luues usaldusväärsete matemaatiliste tõestuste tugeva aluse ja avades tee turvalisele AI-toega matemaatikale ning tarkvaraarendusele.

Tehisintellekti genereeritud matemaatiliste tõestuste kiire voog on tekitanud kõhklusi nende töö usaldusväärsuse ja täpsuse osas. Viimastel kuudel on AI mudelid esitanud sadu käsikirju, milles väidetakse keeruliste matemaatiliste probleemide lahendusi, kuid isegi tavapärased arvuti kontrollid ei ole alati suutnud vigu märkida. Selle väljakutse lahendamiseks keskendub 1,6 miljardi dollari väärtuses idufirma Axiom Math rangelt verifitseeritud matemaatiliste alustalade loomisele läbi ametliku verifitseerimise, tagades, et AI süsteemid suudavad usaldusväärselt genereerida ja kasutada korrektset matemaatikat.

5. novembril 2026 teatas Axiom Math läbimurdest: Stacks Projecti, ühest suurimast ja mõjukamast matemaatikateosest, ametlikust verifitseerimisest. Algatatud 2005. aastal Columbia ülikooli matemaatiku Johan de Jongi poolt, on Stacks Project kasvanud avatud lähtekoodiga, koostööl põhinevaks tööks, mis käsitleb teemasid algebrast geomeetria ja aritmeetilise teooriani, hõlmates ligi 7654 lehekülge.

Axiom'i tehisintellekti agendid tõlkisid kogu Stacks Projecti ligikaudu 16 miljoniks Lean programmeerimiskeeles kirjutatud koodireaks. See tõlge võimaldas tõestusabilise tarkvaral iga tõestuse põhjalikult kontrollida, kinnitades loogilise korrektsuse kogu ulatusliku ja tugevalt omavahel seotud töökorra ulatuses. Nende seoste terviklikkuse tagamine oli märkimisväärne väljakutse, mida tegevjuht Carina Hong võrdles õrnade struktuuride kooskõlla saatmisega massiivses tervikus ilma vastuoludeta.

Ettevõtte asutas 2025. aasta märtsis Hong, endine Stanfordi matemaatikafödrandi kandidaat. Axiom kogus selle aasta alguses Series A voorus 200 miljonit dollarit, mida juhtis Menlo Ventures. Ettevõtte lähenemisviis hõlmab AI agentidele paindlikku koostööraamistikku, võimaldades paralleelset tööd erinevate ülesannete kallal, hoides samal ajal üleüldist hierarhilist struktuuri, mis säilitab sõltuvused Stacks Projectis.

Erinevalt paljudest muudest verifitseerimisalgatustest investeeris Axiom oma AI mudelite koolitamisse spetsiaalselt selleks, et omandada matemaatika ja ametliku tõestamise nüansid, õpetades agente arendama matemaatilist „maitset“. See edasiminek täidab olulise lünga formaliseeritud matemaatikas, eelkõige algebra geomeetrias, pakkudes laia ja usaldusväärset alust tulevaste ametlike tõestuste tegemiseks Lean keskkonnas.

Puhas matemaatika kõrval näeb Axiom oma verifitseeritud aluseid olulisena ka tarkvaraarenduses, eriti AI üha kasvava koodi genereerimise taustal. AI väljundite seostamine rangelt kontrollitud matemaatikaga aitab vähendada AI kirjutatud koodis levinud vigu ja turvaaukusid.

Matemaatikud, sealhulgas Fieldsi medalist Terence Tao, on seda formaliseerimist tähtsaks pidanud, märkides, et verifitseeritud tõestused võimaldavad luua uusi verifitseeritud tõestusi. Axiomi jaoks on verifitseeritud Stacks Project korduvkasutatav alus, millele AI agendid saavad ehitada uut matemaatilist ja teaduslikku infrastruktuuri.

Tegevjuht Hong rõhutab, et AI tulevik teadusuuringutes ja inseneritöös sõltub ligipääsetavatest, korduvkasutatavatest ja hoolikalt ehitatud teadmuskehadest, et vältida vigade ja "sodi" levikut. Ta kutsub teisi koodimisele keskenduvaid ettevõtteid üles proovima võrdväärsel tasemel ametlikku verifitseerimist ning ootab, et strateegiliselt asünkroonselt töötavad koostööagentid muutuvad teadus- ja tarkvaraarenduse tavapäraseks.

Ühendades inimliku matemaatilise ranguse ja AI arvutusvõimsuse, tähistab Axiom Mathi töö Stacks Projectiga suurt sammu usaldusväärse AI-toetatud matemaatika ja tarkvara loomise suunas ning võib lähiaastatel oluliselt kujundada, kuidas keerukaid teadmisi formaliseeritakse ja laiendatakse.