Das KI-Startup «Axiom Math» hat den Erfolg seines Systems autonomer Agenten bei der formalen Verifizierung (Formal Verification) des gesamten Inhalts des «Stacks Project» bekannt gegeben, das als eines der umfangreichsten mathematischen Referenzwerke gilt, die jemals von Mathematikern verfasst wurden.
Umwandlung mathematischen Wissens in prüfbaren Code
Das Stacks Project, das 2005 von Johan de Jong, Professor für Mathematik an der Columbia University, initiiert wurde, umfasst etwa 7.654 Seiten, die Prinzipien der Algebra und algebraischen Geometrie bis hin zu fortgeschrittenen Theorien der Zahlentheorie abdecken. Die Agentenschwärme von Axiom Math konnten diese komplexen und miteinander verknüpften Texte in etwa 16 Millionen Zeilen Code in der Sprache «Lean» übersetzen. Lean ist eine spezialisierte Programmiersprache, die es Prüfsoftware ermöglicht, jeden mathematischen Beweis Zeile für Zeile auf seine strikte logische Korrektheit zu überprüfen.
Das Unternehmen, das nach einer von «Menlo Ventures» angeführten ersten Finanzierungsrunde mit 200 Millionen US-Dollar einen Marktwert von 1,6 Milliarden US-Dollar erreicht hat, zielt darauf ab, eine zuverlässige und formal verifizierte Wissensbasis aufzubauen. Auf dieser sollen zukünftige KI-Systeme in der Softwareentwicklung und wissenschaftlichen Forschung aufbauen, um irreführende oder ungenaue Schlussfolgerungen, bekannt als «generativer Abfall» (AI slop), zu vermeiden.
Arbeitsweise der Software-Agenten und Herausforderungen der strukturellen Kohärenz
Carina Hong, die 25-jährige Gründerin und CEO des Unternehmens, die ihr Mathematik-Promotionsprogramm an der Stanford University abbrach, um Axiom im März 2025 zu gründen, erklärte, dass die größte Herausforderung darin bestand, die Kohärenz von Tausenden von Theoremen zu wahren und konzeptionelle Widersprüche zu vermeiden. Ashvin Swaminathan, Mitglied des technischen Teams des Unternehmens, wies darauf hin, dass die KI-Agenten nicht bei jedem Schritt direkt gesteuert wurden. Stattdessen wurde ihnen eine flexible hierarchische Struktur vorgegeben, die es ihnen ermöglichte, Aufgaben parallel zu verteilen und auf spezialisierte Modelle zurückzugreifen, die auf mathematisches Denken trainiert wurden, anstatt sich auf allgemeine Code-Generierungsmodelle zu verlassen.
Was bedeutet dieser Durchbruch für den Technologiesektor?
Diese Entwicklung stellt einen praktischen Schritt zur Schließung einer großen Lücke bei der computergestützten mathematischen Beweisführung dar, insbesondere in Bereichen wie der algebraischen Geometrie. Der Nutzen der formalen Verifizierung beschränkt sich nicht nur auf akademische Kreise; die Dokumentation von Beweisen durch Computercode schafft eine wiederverwendbare fundamentale Umgebung. Das Unternehmen setzt darauf, dass Entwickler und Ersteller kritischer Software—etwa beim Chip-Design oder bei Berechnungen für sicherheitskritische Systeme—diese verifizierten Grundlagen benötigen werden, um Sicherheitslücken und versteckte Fehler zu verhindern, die durch die zunehmende Abhängigkeit von Agenten beim Schreiben von Software entstehen.