Forscher von Meta und der New York University haben ein schlankes KI-System zum Beweisen mathematischer Theoreme entwickelt, das sorgfältig konstruierte Lean-Beweis-Workflows erreichte oder übertraf – und das zu geringeren Kosten.

Das System namens h1 vertritt ein einfaches Argument: Beim automatisierten Theorembeweisen kann Einfachheit Komplexität schlagen, sofern das Modell gutes Feedback erhält.

Eine minimale agentische Schleife

Die Arbeit stammt vom FAIR-Forschungsteam von Meta und von der NYU. In einer am 25. Oktober 2026 veröffentlichten Studie mit dem Titel "h1: A Taste of the Bitter Lesson in Automated Theorem Proving" beschreiben die Forscher h1 als eine minimale agentische Schleife, die große Frontsprachmodelle mit Lean 4 verbindet und ihnen Verifizierer-Ergebnisse in Echtzeit liefert.

Lean 4 ist ein Open-Source-Beweisassistent, in dem mathematische Argumente als Code geschrieben werden, sodass ein Compiler statt eines menschlichen Prüfers jeden Schritt kontrolliert. Dieses Setup gibt dem Verifizierer das letzte Wort: Ein Beweis zählt erst, wenn er kompiliert.

Die meisten automatisierten Beweiser hüllen das Sprachmodell in eine aufwendige Architektur ein und verwenden vordefinierte Workflows, die Probleme in Teile zerlegen, Unteraufgaben verteilen und viele bewegliche Komponenten orchestrieren. Das h1-Framework verzichtet auf diese Maschinerie und stützt sich stattdessen auf einige einfache Mechanismen:

• Persistente Dateibearbeitung, sodass das Modell an einer Beweisdatei arbeitet, die ihren Zustand zwischen den Schritten beibehält
• Sofortiges Compiler-Feedback nach jeder Bearbeitung, sodass Fehler sofort sichtbar werden
• Reflexion, wobei die eigene Fähigkeit des Sprachmodells genutzt wird, über Fehlerursachen nachzudenken

Laut der Studie stammt h1s Leistung hauptsächlich aus einer effizienten Schnittstelle zu Lean – nicht aus ausgefeilter Orchestrierung.

Benchmark-Ergebnisse

Die Forschung berichtet, dass h1 auf mehreren Benchmarks für formales Theorembeweisen Ergebnisse auf neuestem Stand der Technik erzielte. Auf PutnamBench, einem Benchmark auf Grundlage der Probleme des William-Lowell-Putnam-Wettbewerbs – des jährlichen Mathematikwettbewerbs für nordamerikanische Studierende –, erreichte es mit GPT-5.5 670 von 672 Punkten. Bei der FATE-X-Bewertung erzielte h1 90 von 100 Punkten.

Das System löste außerdem acht offene Probleme der FormalConjectures-Sammlung. Darunter sind Varianten der Erdős-Probleme, einer Reihe von Fragen, die nach dem produktiven Mathematiker Paul Erdős benannt sind. Da solche Probleme in Leans formaler Sprache formuliert sind, bedeutet ihre Lösung die Erstellung maschinell überprüfter Beweise statt prosaischer Argumentationen.

Der direkteste Vergleich ist DeepMinds AlphaProof Nexus. Bei den Lösungen von Erdős-Problemen erreichte h1 eine Erfolgsquote von 82,5 %, während AlphaProof Nexus auf 76 % kam. Die Kostenlücke war größer als die Genauigkeitslücke: h1 gab 121 US-Dollar pro erfolgreichem Beweis aus, AlphaProof Nexus hingegen 317 US-Dollar.

Die bittere Lektion, angewandt auf die Mathematik

Der Titel der Arbeit verweist auf die "bittere Lektion" – ein Begriff, den der KI-Forscher Rich Sutton 2019 in einem Essay prägte und der die Idee beschreibt, dass skalierbare, allgemeine Methoden mit hoher Rechenleistung mit der Zeit spezialisierte, handgefertigte Verfahren übertreffen.

Dies ist nicht Metas erster Versuch in diesem Bereich. Die Forschung baut auf früheren Meta-Arbeiten auf, darunter der 2022 vorgestellte neuronale Theorembeweiser HTPS, und spiegelt einen Ansatzwechsel wider. Frühere Systeme konzentrierten sich darauf, schlauere Suche um das Modell herum aufzubauen, während h1 darauf setzt, das Modell direkt mit dem Verifizierer interagieren zu lassen.

Auch das Timing spielt eine Rolle. h1s Ergebnisse hängen von Frontmodellen wie GPT-5.5 ab, und die starke PutnamBench-Punktzahl wurde mit diesem Modell erreicht.

Was das bedeutet

Die Kostenangaben sind der praktischste Teil der Arbeit. Ein Rückgang von 317 auf 121 US-Dollar pro erfolgreichem Beweis verändert, welche Probleme sich überhaupt zu lösen lohnen. Wenn jeder Versuch weniger kostet, können Teams mehr Versuche an schwierigeren oder spekulativeren Vermutungen unternehmen. Der maschinell überprüfte Charakter der Ergebnisse gehört ebenfalls zur Attraktivität: Fortschritte beim formalen Beweisen ziehen Aufmerksamkeit weit über die Mathematik hinaus, da Beweisassistenten auch zur Verifikation von Software- und Hardware-Designs eingesetzt werden.

Einige Einschränkungen gelten. Benchmark-Punktzahlen zeigen die Leistung auf bestimmten Testsätzen, und PutnamBench ist mit 670 von 672 nahezu gesättigt. Wie Systeme daher bei Sammlungen offener Probleme wie FormalConjectures abschneiden, ist künftig die aussagekräftigste Messgröße. Der h1-Ansatz hängt zudem stark vom darunterliegenden Frontmodell ab.

Die breitere Botschaft der Arbeit lautet, dass ein starkes Basismodell in Kombination mit sauberem Verifizierer-Feedback wichtiger sein kann als aufwendige Architektur – eine Wette, die sich bei diesen Benchmarks auszahlte.

Quelle: CryptoBriefing