Axiom Math erreicht formale Verifikation des umfassenden Stacks-Projekts zur Sicherung KI-gestützter Mathematik

Image: TechCrunch · Source

Axiom Math hat das umfangreiche Stacks-Projekt mithilfe von KI-Agenten formal verifiziert, wodurch eine solide Grundlage für vertrauenswürdige mathematische Beweise geschaffen und der Weg für zuverlässige KI-unterstützte Mathematik und Softwareentwicklung geebnet wurde.

Der rasche Zustrom von mathematischen Beweisen, die durch künstliche Intelligenz generiert wurden, hat Bedenken hinsichtlich der Zuverlässigkeit und Genauigkeit solcher Arbeiten geweckt. In den letzten Monaten haben KI-Modelle Hunderte von Manuskripten eingereicht, die Lösungen für schwierige mathematische Probleme behaupten, doch selbst herkömmliche Computerprüfungen haben manchmal Fehler nicht entdeckt. Um diese Herausforderung anzugehen, konzentriert sich das 1,6 Milliarden Dollar bewertete Startup Axiom Math darauf, rigoros verifizierte mathematische Grundlagen mittels formaler Verifikation zu schaffen, um sicherzustellen, dass KI-Systeme korrektes Mathematikwissen zuverlässig erzeugen und verwenden können.

Am 5. November 2026 kündigte Axiom Math einen Meilenstein an: die formale Verifikation des Stacks-Projekts, eines der größten und angesehensten mathematischen Kompendien. Das Stacks-Projekt, das 2005 vom Mathematiker Johan de Jong von der Columbia University ins Leben gerufen wurde, entwickelte sich zu einem Open-Source-Kollaborationswerk, das ein breites Themenspektrum von Algebra über Geometrie bis Zahlentheorie abdeckt und etwa 7.654 Seiten umfasst.

Die KI-Agenten von Axiom übersetzten das gesamte Stacks-Projekt in etwa 16 Millionen Zeilen Code in Lean, einer formalen Beweissprache. Diese Übersetzung ermöglichte es einer Beweisassistenten-Software, jeden Beweis streng zu überprüfen und die logische Korrektheit dieses umfangreichen und tief vernetzten Werks zu bestätigen. Die Sicherstellung der Integrität dieser Verknüpfungen stellte eine bedeutende Herausforderung dar, die CEO Carina Hong damit verglich, fragile Strukturen in einem riesigen Ganzen widerspruchsfrei zusammenzuführen.

Gegründet im März 2025 von Hong, einer ehemaligen Stanford-Mathematik-Promovendin, sammelte Axiom Anfang dieses Jahres in einer Series-A-Finanzierungsrunde unter Führung von Menlo Ventures 200 Millionen Dollar ein. Der Ansatz des Unternehmens besteht darin, seinen KI-Agenten einen flexiblen Rahmen zu geben, in dem sie zusammenarbeiten können, sodass parallel an verschiedenen Aufgaben gearbeitet wird, während die übergeordnete hierarchische Struktur zur Erhaltung der Abhängigkeiten im Stacks-Projekt beibehalten wird.

Im Gegensatz zu vielen Verifikationsinitiativen investierte Axiom in die Ausbildung eigener KI-Modelle, die speziell die Feinheiten der Mathematik und Formalisierung meistern, und brachte den Agenten effektiv bei, ein mathematisches „Geschmacksempfinden“ zu entwickeln. Dieser Fortschritt schließt eine große Lücke in der formalisierten Mathematik, insbesondere in der algebraischen Geometrie, und bietet eine breite und verlässliche Basis für zukünftige formale Beweise mit Lean.

Über die reine Mathematik hinaus sieht Axiom seine verifizierten Grundlagen als kritisch für die Softwareentwicklung an, insbesondere da KI zunehmend Code generiert. Indem die Ausgaben der KI auf rigoros überprüften mathematischen Grundlagen basieren, zielt das Unternehmen darauf ab, in KI-geschriebenem Code verbreitete Fehler und Sicherheitslücken zu reduzieren.

Mathematiker wie der Fields-Medaillengewinner Terence Tao haben die Bedeutung einer solchen Formalisierung anerkannt und festgestellt, dass verifizierte Beweise die Grundlage für weitere verifizierte Beweise schaffen. Für Axiom ist das verifizierte Stacks-Projekt ein wiederverwendbares Substrat, auf dem KI-Agenten neue mathematische und wissenschaftliche Infrastrukturen aufbauen können.

CEO Hong betont, dass die Zukunft der KI in Forschung und Technik von zugänglichen, wiederverwendbaren und sorgfältig konstruierten Wissenskörpern abhängt, um die Verbreitung von Fehlern oder „Schlamperei“ zu verhindern. Sie fordert andere stark codierungsorientierte Unternehmen heraus, eine formale Verifikation in vergleichbarem Umfang zu versuchen, und erwartet, dass kollaborierende KI-Agenten, die asynchron und strategisch arbeiten, zum Standard in wissenschaftlichen und softwaretechnischen Entwicklungen werden.

Durch das Überbrücken der Lücke zwischen menschlicher mathematischer Strenge und der Rechenleistung der KI markiert die Arbeit von Axiom Math am Stacks-Projekt einen bedeutenden Schritt hin zu vertrauenswürdiger, KI-unterstützter Mathematik und Softwareentwicklung, mit dem Potenzial, die Formalisierung und Erweiterung komplexer Wissensbereiche in den kommenden Jahren grundlegend zu verändern.