AlphaProof Code vs. MathForm-8B: Zwei Stufen derselben Lean-Pipeline, keine zwei Rivalen

Liest man das AlphaProof-Code-Paper genau, fällt eine Zahl auf, die in der Ankündigung nicht betont wird: Von den vier Wochen, die die fünf Forschenden von DeepMind damit verbrachten, Signal zu verifizieren, war der Teil, der sich nicht automatisieren ließ, der vordere Teil. Menschliche Expertinnen und Experten arbeiteten mit einer Mischung aus Modellen zusammen, um die Sicherheitsziele von Signal in formale Lean-Spezifikationen zu übersetzen, und eine Expertin oder ein Experte prüfte jede einzelne davon, bevor irgendeine Beweisfarbeit begann. Das ist der Engpass. MathForm-8B, OpenBMBs Autoformalisierungsmodell mit 8 Milliarden Parametern, das am 14. August 2026 auf Hugging Face veröffentlicht wurde, ist ein direkter Versuch, genau diesen Schritt zu automatisieren – eine mathematische Aussage in natürlicher Sprache zu nehmen und eine Lean-4-Theoremaussage auszugeben, die bereit dafür ist, von jemand anderem bewiesen zu werden. Stellt man sie nebeneinander, vergleicht man nicht zwei Produkte. Man betrachtet zwei aufeinanderfolgende Stufen einer Pipeline, getrennt durch den Unterschied zwischen Mathematik und Protokollsicherheit.

Die Pipeline, in der Reihenfolge, in der die Arbeit abläuft

Die formale Verifikation realer Software hat drei Aufgaben. Erstens: entscheiden, was wahr sein muss, und es in einer formalen Sprache aufschreiben. Zweitens: beweisen, dass die Implementierung dies erfüllt. Drittens: die Beweise maschinell prüfen, denn ein falscher Beweis ist schlimmer als kein Beweis.

MathForm-8B erledigt Aufgabe eins, und zwar für eine enge Eingabeklasse: mathematische Aussagen im Lehrbuchstil. Gibt man ihm „für jede reelle Zahl x ist x² nicht negativ“, liefert es die Importe, die Typen und einen Theorem-Kopf in Lean 4 zurück. Was es nicht zurückliefert, ist ein Beweis, und seine Autoren stellen ausdrücklich klar, dass die Beweissuche das Problem von jemand anderem ist. Seine gemeldeten Zahlen – alle vom Anbieter angegeben und nicht reproduziert – sind 88,06 % durchschnittliches Pass@8 unter einer Syntaxprüfung und 72,37 % unter der strengeren Konsistenzprüfung über sechs Benchmarks hinweg – die Lücke zwischen diesen beiden Werten ist das ehrliche Maß dafür, wie oft eine syntaktisch gültige Aussage etwas anderes bedeutet als das, wonach gefragt wurde.

AlphaProof Code erledigt Aufgaben zwei und drei, plus eine Spezifikationsphase, die MathForm-8B nicht bewältigen konnte. Die Signal-Sicherheitsziele sind keine mathematischen Aussagen in dem Sinne, in dem MathForm trainiert wurde; es sind Aussagen über ein Protokoll — dass Nachrichten sowohl vor als auch nach einer vorübergehenden Kompromittierung eines Geräts geschützt bleiben, dass Initiator und Responder die sind, für die sie sich ausgeben. Sie in Lean zu überführen erforderte Protokollexpertise, über die kein 8B-Autoformalizer verfügt. Als die Spezifikation erst einmal vorlag, wurde die Beweisführung vollständig an Agenten übergeben und die Prüfung an Lean-Kernel plus einen Gatekeeper-Agenten, der mithilfe von comparator einen Abgleich mit einer zurückgehaltenen Kopie der Spezifikation vornahm.

Was dich die Nutzung jedes Einzelnen tatsächlich kostet

• Gewichte — MathForm-8B: herunterladbar, Apache 2.0, vier Safetensors-Shards in BF16, feinabgestimmt aus Qwen3-8B. AlphaProof Code: nicht vorhanden. Bei der Veröffentlichung handelt es sich um eine Lean-Entwicklung, eine AArch64-Semantik und ein libsignal-Binding unter github.com/google-deepmind/code-verification.

• Betrieb — MathForm-8B: Transformers, vLLM oder SGLang, alle mit einem OpenAI-kompatiblen Endpunkt, auf eigener Hardware. AlphaProof Code: kein Endpunkt, keine API, keine Warteliste, kein Preis; es ist ein Forschungsframework, von dem DeepMind sagt, dass es „weitere Forschung“ braucht, bevor es skaliert.

• Eingabe — MathForm-8B: eine mathematische Aussage in natürlicher Sprache. AlphaProof Code: eine formale Spezifikation plus die Binärdatei, die dagegen bewiesen werden soll.

• Ausgabe — MathForm-8B: eine unbewiesene Theoremaussage in Lean 4. AlphaProof Code: ein maschinell geprüfter Beweis oder eine Widerlegung, wenn der Code fehlerhaft ist.

• Menschliche Überprüfung — MathForm-8B: Sie prüfen die ausgegebene Aussage, und bei 72,37 % Konsistenz werden Sie viele davon prüfen. AlphaProof Code: Expertinnen und Experten prüfen jede Spezifikation, bevor die Beweisführung beginnt; anschließend markieren Agenten etwa 1 % der Codebasis für eine zweite Prüfung.

• Bekannte Einschränkungen — MathForm-8B: nur mathematische Aussagen, keine Beweiserzeugung, und das in seiner README verlinkte Code-Repository war zum Veröffentlichungszeitpunkt noch ein Platzhalter. AlphaProof Code: keine Post-Quanten-Garantie für SPQR-Heilung, keine Nutzlast-Privatsphäre, eine Sitzung pro Promotion und eine MAC-Fälschungsschranke, die nahe 25.000 Nachrichten in einer einzigen Sitzung nichtssagend wird.

Die Lücke, die MathForm-8B schließen müsste

Es ist verlockend zu sagen, ein Autoformalisierer hätte Signals Spezifikationen schreiben und den Forschern ihre vorgelagerten Wochen ersparen können. Die Darstellung im Paper selbst sagt etwas anderes, und der Grund dafür ist ein spezifischer. Eine Spezifikation eines Protokolls ist keine Wiederholung einer Behauptung; sie ist eine Entscheidung über das Angreifermodell. Die Signal-Arbeit enthält eine symbolische Spur in Dolev–Yao mit einem Quantenangreifer, der Diffie–Hellman nach dem Handshake bricht, und eine rechnerische Spur mit klassischen Angreifern und einer konkreten Schranke. Diese beiden Spuren formulieren unterschiedliche Theoreme über denselben Code, und die Wahl zwischen ihnen ist eine Ingenieursentscheidung mit sicherheitsrelevanten Konsequenzen. Kein Modell, das darauf trainiert wurde, „zeige, dass x² ≥ 0“ in Lean umzuwandeln, wird diese Entscheidung treffen.

Was ein Autoformalisierer plausibel tun könnte, ist der mechanische Teil dieser Arbeit: mit einem in Prosa formulierten Sicherheitsziel und einer Bibliothek vorhandener Lean-Definitionen einen ersten Entwurf der Aussage im eigenen Idiom des Projekts zu erstellen, den ein Experte korrigieren kann. Das ist eine echte Ersparnis – und eine viel kleinere, als die Schlagzeile nahelegt. Das Paper berichtet von einem Katalog von Spezifikationsabweichungen mit über 200 komputationellen Einträgen und etwa 35 symbolischen – fünfzehn davon Lücken oder Fehler in der Double-Ratchet-Analyse –, was der menschliche Prüfschritt ergab. Ein Modell, das Aussagen entwirft, müsste an diesem Katalog gemessen werden, nicht an einem Pass@8-Score bei Mathematik-Benchmarks.

Wo die beiden Zahlen überhaupt nicht vergleichbar sind

Die 88,06 % von MathForm-8B und die 6,5 Millionen Zeilen von AlphaProof Code messen unterschiedliche Dinge und sollten niemals in derselben Spalte stehen. Das eine ist eine Trefferquote bei einer Benchmark-Suite, die die Autoren selbst erstellt haben; das andere ist eine Menge an Beweisen, die für ein einziges Ziel erzeugt wurde. Der Anbieter räumt offen ein, dass die 88,06 % auf einer Syntaxprüfung beruhen, einem schwachen Kriterium – eine Aussage kann kompilieren und dennoch die falsche Behauptung formalisieren, weshalb die Konsistenzzahl 16 Punkte niedriger liegt.

Die vergleichbar gelagerte Kennzahl von AlphaProof Code ist die Validierungsarbeit: Zwei zuvor behobene Signal-Bugs – ein Weak-State-Bug und ein Small-Subgroup-Bug – wurden in eine isolierte Kopie wieder eingeführt, und in beiden Fällen erzeugte das System einen maschinell geprüften Beweis dafür, dass die fehlerhafte Version das Sicherheitstheorem verletzt. Das ist ein Negativtest, und ein Negativtest ist genau das, was einem Autoformalizer-Benchmark vollständig fehlt. MathForm-8B meldet kein Ergebnis der Form „Bei einer absichtlich falschen Aussage sagte das Modell, dass sie falsch sei.“

Wie du sie tatsächlich zusammen verwenden würdest

Konkret – und dies ist der einzige Teil des Vergleichs, für den es einen kurzfristig gangbaren Weg gibt: einen Autoformalisierer den Entwurf erstellen lassen, ein starkes allgemeines Modell den Entwurf kritisieren lassen und einen Beweisagenten den Beweis versuchen lassen. Jede Stufe hat einen anderen Fehlermodus, und alle drei über einen Schlüssel zu leiten, ist der praktische Vorteil. Bei OrcaRouter stehen mehr als 200 Modelle hinter einer einzigen API zum Listenpreis des Anbieters mit 0 % Aufschlag, sodass eine Spezifikationsentwurfs-Schleife, die dieselbe Aussage an zwei Modelle sendet und deren Lean-Ausgaben vergleicht, ein Routing-DSL-Aufruf ist und nicht drei Verträge und drei SDKs. Automatisches Failover deckt den Fall ab, dass das von Ihnen gewählte Modell gerade einen schlechten Nachmittag hat.

Was nichts davon bietet, ist die Garantie. MathForm-8B liefert eine Aussage, die Modelle liefern eine Kritik, und irgendetwas muss sie noch beweisen. Derzeit ist das einzige veröffentlichte System, das diesen Kreislauf bei tatsächlich eingesetztem Code schließt, AlphaProof Code, und es ist nicht käuflich.

Der Grund, beide Arbeiten zu lesen, statt einen Gewinner zu küren

MathForm-8B ist ein nützliches Artefakt mit einer eng umrissenen Aufgabe und einer realen, gemessenen Genauigkeitsobergrenze. AlphaProof Code ist eine Workflow-Demonstration, deren am besten übertragbare Erkenntnis nicht das Beweisvolumen ist, sondern die Aufteilung: Spezifikationsarbeit braucht Menschen und ein starkes allgemeines Modell, Beweisarbeit braucht Agententeams und einen Kernel, und die Grenze zwischen beiden ist der Ort, an dem die gesamte Schwierigkeit liegt. Wer eine Verifikationspipeline baut, sollte diese Aufteilung ernst nehmen und Autoformalisierung als den Teil behandeln, der die Kosten der ersten Phase senkt – nicht als den Teil, der sie ersetzt.

Die ehrliche Zusammenfassung für ein Team, das entscheidet, was es diesen Monat herunterladen soll: MathForm-8B, ja, wenn Sie mit Lean arbeiten und eine Entwurfshilfe möchten. AlphaProof Code: Lesen Sie das Artefakt-Repository und den Katalog der Spezifikationsabweichungen, denn der Katalog sagt Ihnen mehr darüber, was formale Verifikation von Produktionscode noch immer nicht erreichen kann, als jede Ankündigung es tun wird.