Osegi
AI·2 min czytania

Axiom Math weryfikuje Stacks Project, by ograniczyć AI slop w matematyce

Agenci AI startupu Axiom Math formalnie zweryfikowali Stacks Project, jedną z największych bibliotek matematycznych. Firma stawia na zweryfikowane fundamenty dla AI.

Abstract illustration of mathematical formulas and lines of code representing formally verified proofs checked by AI agents.
Zdjęcie: TechCrunch
SUMODialoediviewergiftdetect

Startup Axiom Math ogłosił w środę, że jego agenci AI formalnie zweryfikowali Stacks Project, jeden z największych zbiorów matematyki spisanych przez ludzi. Firma wyceniana na 1,6 mld dolarów chce w ten sposób zbudować sprawdzone fundamenty, na których agenci AI będą mogli pisać oprogramowanie, a w przyszłości także prowadzić badania naukowe.

Czym jest Stacks Project

Projekt w 2005 roku zainicjował Johan de Jong z Uniwersytetu Columbia jako otwarty zbiór referencyjny. Od tamtej pory dokładają się do niego matematycy, a zakres sięga od algebry na poziomie studiów po zaawansowane zagadnienia algebry, geometrii i teorii liczb. Peter Woit z Columbii uważa, że „nie ma nic naprawdę porównywalnego”, zestawiając go z książkami Bourbakiego.

Agenci Axiom przełożyli około 7654 stron na mniej więcej 16 mln linii kodu w języku Lean, który sprawdza asystent dowodzenia. Jeśli dowód przejdzie weryfikację, można zakładać, że jest logicznie poprawny. Trudność polegała na tym, że twierdzenia i definicje w Stacks wzajemnie się na siebie powołują, więc trzeba było zachować wszystkie powiązania. Zespół początkowo nie był pewien powodzenia. Jak mówiła CEO Carina Hong, rzeczy duże i delikatne rzadko idą w parze.

Agenci pracujący równolegle

Zespół nadał agentom luźną hierarchię i pozwolił działać równolegle. Według Ashvina Swaminathana agenci sami znajdowali zadania. Axiom trenuje też własne modele matematyczne, czego, jak twierdzi Hong, większość startupów od weryfikacji nie robi.

Wynik wypełnia jedną z największych luk w sformalizowanej matematyce: geometrię algebraiczną. Swaminathan podkreśla, że badacze sprawdzający nowe prace w Lean mają teraz na czym się oprzeć.

Dlaczego to ważne

Axiom argumentuje, że każdy zweryfikowany wynik staje się cegiełką dla kolejnych dowodów. Terence Tao ujął to tak: im więcej sformalizowanych dowodów, tym więcej można stworzyć kolejnych. Docelowo chodzi także o programistów, którzy od dawna próbują gwarantować, że kod nie ma błędów i luk bezpieczeństwa, a problem rośnie wraz z tym, jak wiele kodu pisze AI.

Hong uważa, że agenci potrzebują wielokrotnego użytku bazy wiedzy, by nie produkować „slopu”. Wyzwanie rzuciła też konkurencji: wezwała firmy programistyczne do pracy nad formalizacją na podobną skalę. Axiom założono w marcu 2025 roku, a w marcu tego roku firma pozyskała 200 mln dolarów w rundzie Series A pod przewodnictwem Menlo Ventures.

Aplikacje warte uwagi

SUMO: łamigłówka liczbowa

Wybierz właściwe pola, dodaj je i trafiaj w cel. Łatwa do nauczenia, trudna do opanowania. Za darmo, dla każdego wieku.

Tagi:axiom mathstacks projectleanformal verificationai agentsmathematics

Więcej z tego dnia

Zobacz wszystkie →

Więcej w kategorii: AI

Zobacz wszystkie →