Axiom Math převedla rozsáhlý matematický projekt do ověřitelného kódu Lean
Společnost Axiom Math oznámila, že její AI agenti formálně ověřili rozsáhlý matematický zdroj Stacks Project. Výsledkem je přibližně 16 milionů řádků kódu, které mají výzkumníkům i dalším AI systémům nabídnout spolehlivý základ pro další práci.
Matematika jako obrana proti chybám AI
Umělá inteligence podle titulků každý týden řeší nové matematické problémy. Zároveň ale zůstává otázka, zda jsou takové výsledky skutečně správné. Článek TechCrunch připomíná, že OpenAI minulý měsíc zveřejnila 719 rukopisů, které tvrdily, že řeší některé z nejtěžších problémů oboru. Ani počítačové kontroly, jež mají výsledky potvrdit, však podle článku nemusejí být bezchybné.
Startup Axiom Math chce riziko nekvalitních výstupů omezit tím, že AI poskytne pevnější základ. Ve středu oznámil formální ověření Stacks Projectu, rozsáhlé otevřené matematické příručky, na níž odborníci pracují od roku 2005. Projekt založil Johan de Jong z Kolumbijské univerzity a postupně do něj přispívali další matematici.
Tisíce stran převedené do kódu
Stacks Project má přibližně 7 654 stran a pokrývá témata od algebraických základů až po pokročilé oblasti algebry, geometrie a teorie čísel. Axiom Math uvádí, že jeho AI agenti převedli knihovnu do zhruba 16 milionů řádků kódu v jazyce Lean. Ten umožňuje matematický důkaz zapsat tak, aby jej mohl krok za krokem zkontrolovat specializovaný program zvaný proof assistant.
Takové formální ověřování má potvrdit, že důkaz je logicky správný. Nejde přitom jen o kontrolu jednotlivých tvrzení. Výsledky ve Stacks Projectu na sebe navazují a každý může vycházet z dřívějších definic a důkazů. Tým proto musel při převodu zachovat vazby napříč celým dílem a zajistit, aby si jeho části neodporovaly.
Agenti pracovali souběžně
Axiom Math zpočátku pochybovala, zda se tak rozsáhlý a propojený projekt podaří dokončit. Její generální ředitelka Carina Hong řekla TechCrunch, že firma si nebyla jistá, zda „vibe coding“ dokáže zachovat krásu Stacks Projectu. Agenti dostali určitou strukturu, ale podle člena technického týmu Ashvina Swaminathana měli prostor sami vyhledávat úkoly a pracovat na nich souběžně.
Firma si také vytrénovala vlastní modely zaměřené na matematiku. Hong uvedla, že zpočátku agentům pomáhal odborník na Lean, který je učil rozpoznávat vhodná řešení. Postupně si podle ní agenti tento cit osvojili sami. Hong, která založila Axiom Math v březnu 2025 po odchodu z doktorského studia matematiky na Stanfordu, firmu označila za startup v hodnotě 1,6 miliardy dolarů. V březnu získala investiční kolo Series A ve výši 200 milionů dolarů, které vedla Menlo Ventures.
Základ pro další důkazy i software
Formálně ověřený Stacks Project má zaplnit výraznou mezeru v matematice, zejména v algebraické geometrii. Swaminathan uvedl, že výzkumníci, kteří chtěli ověřovat nové práce v této oblasti pomocí Lean, dosud měli jen málo hotového materiálu, o který by se mohli opřít. Nyní podle něj takový základ mají. Každý ověřený výsledek může sloužit jako stavební kámen pro další důkazy, místo aby se vše začínalo od nuly.
Axiom Math míří také na vývojáře. S rostoucím podílem kódu psaného AI agenty podle firmy poroste potřeba ověřovat, že software neobsahuje chyby ani bezpečnostní nedostatky. Společnost sází na to, že matematické ověřování lze využít i při budování spolehlivějšího softwaru. Hong proto vyzvala firmy vyvíjející programovací nástroje, aby pracovaly na formalizaci v podobném rozsahu.