Autoformalisierung
Autoformalisierung bezeichnet das automatische Übersetzen von Mathematik in normaler Sprache in eine streng formale Schreibweise, die ein Computer Schritt für Schritt auf Fehler prüfen kann. KI-Modelle übernehmen dabei die Übersetzungsarbeit, die bisher Menschen mühsam von Hand erledigen mussten.
Mathematik wird normalerweise in einer Mischung aus Sprache, Formeln und Skizzen aufgeschrieben. Ein Mensch versteht so einen Beweis, ein Computer nicht. Damit ein Programm einen Beweis wirklich nachrechnen kann, muss jeder Schritt in einer streng festgelegten Kunstsprache stehen, in der es keine Lücken und keine Mehrdeutigkeit gibt. Das Umschreiben in diese Kunstsprache nennt man Formalisieren, und es ist extrem aufwendig: Für eine einzige Seite Lehrbuchtext gehen leicht Tage drauf. Autoformalisierung heißt, diese Übersetzung von einer KI erledigen zu lassen. Aus einem Satz wie « jede gerade Zahl größer als zwei ist die Summe zweier Primzahlen » wird dann automatisch ein Ausdruck, den eine Prüfsoftware verarbeiten kann.
Was formale Beweise so wertvoll macht
Bei einem formal geprüften Beweis gibt es keine Zweifelsfälle mehr. Die Software akzeptiert ihn, oder sie akzeptiert ihn nicht. Menschliche Gutachter übersehen dagegen manchmal Fehler, gerade bei Beweisen über hunderte Seiten. Es gab in der Mathematikgeschichte mehrfach Ergebnisse, die jahrelang als bewiesen galten und sich später als lückenhaft herausstellten.
Der zweite Grund betrifft die KI selbst. Sprachmodelle erfinden bekanntlich Dinge, die plausibel klingen, aber falsch sind. Bei Mathematik fällt das oft erst spät auf. Wenn ein Modell seine Beweise aber in formaler Form abliefert, kann die Prüfsoftware sofort ein Urteil fällen. Damit hat man ein Signal, das nicht auf Meinung beruht, sondern auf Rechnung.
Genau dieses Signal lässt sich zum Training nutzen. Ein Modell kann tausende Beweisversuche produzieren, die Software sortiert die falschen aus, und mit den korrekten wird weitertrainiert. Solche Kreisläufe gelten als einer der aussichtsreichsten Wege, KI im logischen Denken besser zu machen. Der Engpass dabei ist die Menge an formalisierten Aufgaben – und den soll Autoformalisierung beseitigen.
Von der Textzeile zum prüfbaren Ausdruck
Die formale Kunstsprache stammt von sogenannten Beweisassistenten. Bekannte Vertreter heißen Lean, Isabelle oder Coq. Man kann sie sich als Programmiersprachen für Mathematik vorstellen. Sie kennen nur wenige Grundregeln und leiten alles andere daraus ab. Ein Beweis ist darin ein Programm, und die Prüfung ist im Grunde ein sehr strenger Compiler-Durchlauf.
Ein Sprachmodell wird nun auf Paare trainiert: links der Text in normaler Sprache, rechts die formale Fassung. Nach genug Beispielen kann es die Übersetzung selbst versuchen. Der Vorschlag geht anschließend direkt an den Beweisassistenten. Meldet der einen Fehler, geht die Fehlermeldung zurück ans Modell, das einen neuen Anlauf nimmt. Oft laufen dutzende solcher Runden, bis ein Ausdruck durchgeht.
Ein Fallstrick bleibt trotzdem. Der Beweisassistent prüft nur, ob eine Aussage korrekt bewiesen ist – nicht, ob es die gemeinte Aussage ist. Übersetzt das Modell die Aufgabe schief, entsteht ein tadelloser Beweis für die falsche Behauptung. Man unterscheidet deshalb zwei Aufgaben: die Formalisierung der Aussage und das anschließende Finden des Beweises. Nur die zweite prüft die Software wirklich zuverlässig.
Wettbewerbsaufgaben, Mathlib und Chip-Design
Am sichtbarsten ist das Thema bei Mathematikolympiaden. Systeme wie AlphaProof von Google DeepMind formalisierten Wettbewerbsaufgaben automatisch und lösten sie anschließend in Lean. 2024 reichte das für eine Silbermedaille bei der Internationalen Mathematik-Olympiade. Solche Meldungen tauchen inzwischen regelmäßig in Tech-News auf.
Parallel wächst Mathlib, eine gemeinsame Bibliothek formalisierter Mathematik für Lean. Sie enthält weit über eine Million Beweiszeilen, getippt von Freiwilligen aus aller Welt. Autoformalisierung soll dieses Tempo vervielfachen. Große Projekte, etwa die Formalisierung moderner Forschungsarbeiten, wären sonst kaum zu stemmen.
Außerhalb der reinen Mathematik nutzen Chip- und Softwarefirmen dieselbe Technik. Prozessoren und sicherheitskritische Programme werden formal verifiziert, damit bestimmte Fehler nachweislich ausgeschlossen sind. Auch dort ist das Aufschreiben der Anforderungen die teure Arbeit. Wer sie automatisieren kann, spart erhebliche Kosten – deshalb interessiert sich nicht nur die Forschung für das Thema, sondern auch die Industrie.