OpenBMB hat sein gesamtes MathForm-System zur automatischen Formalisierung von Mathematik als Open Source veröffentlicht: die Gewichte des 8B-Modells, einen Datensatz mit rund 367.000 verifizierten Lean-4-Beispielen, den Evaluierungscode und die Pass@k-Skripte. Das Modell steht auf Hugging Face bereit, lizenziert unter Apache 2.0, basierend auf Qwen3-8B mit BF16-Gewichten. Hinter dem Projekt steht ein Team von OpenBMB, unterstützt vom Tsinghua NLP Lab und ModelBest; die gleichnamige Studie mit zehn Autoren wurde Mitte des Monats auf arXiv eingereicht.
Automatische Formalisierung übersetzt mathematische Aussagen aus natürlicher Sprache in maschinell verifizierbare formale Sprachen wie Lean 4. Die Schwierigkeit liegt nicht in der wörtlichen Übersetzung. Mathlibs Typhierarchie und sein Begriffsapparat sind enorm umfangreich – Begriffe wie „stetige Funktion" oder „endliche Gruppe" müssen exakt auf die passende Definition in der Bibliothek abgebildet werden, während die formalisierte Aussage inhaltlich mit dem Original übereinstimmen muss. Weicht eines der beiden ab, nickt der Compiler unter Umständen trotzdem ab.
Wie die Daten entstanden sind
Die MathForm-Pipeline läuft in vier Schritten ab: Ein Planer durchsucht Mathlib zunächst nach den in der Aussage vorkommenden mathematischen Konzepten, wobei das Retrieval-Tool LeanExplore jeweils die obersten 22 Treffer liefert. Das Modell generiert daraufhin, gestützt auf diesen Retrieval-Kontext, die Lean-4-Aussage. Die Kandidaten durchlaufen anschließend eine Formatprüfung und einen Kompiliertest, bevor ein LLM-Richter die semantische Konsistenz beurteilt. Erfolgreiche Pfade werden rückwirkend zu sauberen Trainingstrajektorien rekonstruiert.
Eine Zahl aus der Studie zeigt, wie nötig die Iteration ist: Spätere Runden trugen zusätzliche 31,0 % zu allen letztlich verwendeten Beispielen bei. Würde man also nur einen einzigen Durchlauf machen und ungeeignete Kandidaten verwerfen, ginge fast ein Drittel der nutzbaren Daten verloren.
Das Retrieval ist der kosteneffizienteste Baustein des gesamten Ansatzes. Ein Modell aus dem Gedächtnis den exakten Namen und die Signatur einer Mathlib-Definition abrufen zu lassen, prüft im Grunde, ob es eine sich ständig weiterentwickelnde Bibliothek auswendig gelernt hat. Überlässt man die Bibliothek stattdessen einem Retrieval-Tool und lässt das Modell nur noch zusammensetzen, sinkt der nötige Parameterbedarf von selbst. Das erklärt auch, warum ein 8B-Modell mit 32B-Modellen mithalten kann: Beide Seiten lösen im Grunde nicht dieselbe Aufgabe.
Der entstandene Datensatz heißt FormalVerse und umfasst rund 367.000 verifizierte Beispiele aus DeepTheorem, NuminaMath, AceReason-Math, Lean Workbook, Principia-Collection, DeepMath und OpenR1-Math, ergänzt um Inhalte aus klassischen Lehrbüchern. Der Datensatz hat auf Hugging Face bereits 358 Likes erhalten.
Die Ergebnisse und ihre zwei Maßstäbe
Trainiert wurde per überwachtem Feintuning gefolgt von Reinforcement Learning. Die Auswertung deckt sechs Benchmarks ab: FormalMATH-Lite und DeepSeek-ProverBench prüfen Wettbewerbsmathematik, CombiBench testet Kombinatorik, und die FATE-Reihe ist nach algebraischem Schwierigkeitsgrad in die Stufen M, H und X unterteilt.
MathForm-8B erreicht im Schnitt eine Syntaxprüfung von Pass@8 88,06 % und eine Konsistenzprüfung von 72,37 %; die Konsistenz-Erfolgsquoten der drei FATE-Stufen liegen bei 97,33 %, 63,00 % und 37,00 %. Zu den Vergleichsmodellen zählen Herald Translator-7B, Kimina-Autoformalizer-7B, Mathesis-HPO-7B sowie jeweils die 7B/8B- und 32B-Varianten von StepFun-Formalizer, Goedel-Formalizer-V2 und ReForm. Das 8B-Modell übertrifft dabei auf mehreren Testsets die spezialisierten 32B-Formalisierungsmodelle.
Die Lücke zwischen den beiden Maßstäben sagt mehr aus als die absoluten Werte. Die Syntaxprüfung fragt nur, ob der Code kompiliert; die Konsistenzprüfung fragt, ob die formalisierte Aussage inhaltlich dasselbe bedeutet wie das Original – 88 % gegenüber 72 %, und genau in diesen gut zehn Prozentpunkten liegt der eigentliche Flaschenhals der Pipeline. Was kompiliert, ist nicht zwangsläufig der Satz, den man eigentlich beweisen wollte.
Die Hürde sinkt auf eine einzelne Workstation
Vor kurzem ging es hier um Terence Taos Warnung, dass KI-generierte Beweise bald in einer Menge anfallen könnten, die niemand mehr lesen kann. Formalisierung liefert die andere Hälfte der Antwort auf dieses Problem: Solange ein Beweis den Lean-Compiler durchläuft, ist es keine Voraussetzung mehr, ihn zu verstehen, um ihn zu akzeptieren. Voraussetzung bleibt aber, dass die Aussage selbst richtig übersetzt ist – und die 37 % auf FATE-X zeigen, dass bis dahin noch ein gutes Stück Weg liegt.
Grob gerechnet benötigt ein 8B-Modell mit BF16 etwa 16 GB VRAM, ein gleich präzises 32B-Modell rund 64 GB. Ersteres läuft auf einer einzelnen 24-GB-Consumer-Grafikkarte, Letzteres braucht mehrere oder professionelle Karten. Für mathematische Fakultäten, die Community der Beweisassistenten und kleine Teams sinkt die Hardwarehürde für eine Formalisierungs-Pipeline damit vom Cluster- auf Einzelrechner-Niveau. Da Datensatz und Auswertungscode gleichzeitig offengelegt wurden, sinken auch die Kosten für Nachbau und Kritik durch Dritte.
Auch die Liste der Vergleichsmodelle zeigt, wie umkämpft dieses Feld inzwischen ist: Herald, Kimina, Mathesis, StepFun-Formalizer, Goedel-Formalizer-V2, ReForm – allesamt spezialisierte Formalisierungsmodelle aus den letzten ein, zwei Jahren, durchweg quelloffen. Formalisierung setzt sich anders als klassische Dialogsysteme nicht primär durch Rechenleistung ab, sondern durch die Qualität der Datenkonstruktion und den Verifikationskreislauf – die Parametergröße wird hier eher zur Nebensache. Dass eine Pipeline so schnell vom Paper-Demo zur quelloffenen Auslieferung kommt, geht schneller, als die meisten erwartet hätten.
Quellen: OpenBMB-Projektrepository und Modellkarte, CocoLoop, arXiv-Preprint 2608.14221, Hugging-Face-Datensatzseite; geprüft wurden Parametergröße, Lizenz, Stichprobenumfang von FormalVerse und die Pass@8-Werte der einzelnen Testsets.