Lean-Feedback statt komplexer Agenten-Workflows: Studie untersucht automatisiertes Beweisen

Was h1 praktisch tut

Lean ist eine Sprache und Proof-Assistant-Umgebung, in der mathematische Aussagen und Beweise formal notiert und mechanisch geprüft werden. Ein Modell muss dabei nicht nur eine plausible Erklärung liefern, sondern einen Beweis in einer Form erstellen, die Lean akzeptiert. Während der Entwicklung zeigt das System unter anderem offene Beweisziele und Compilerfehler an. Eine externe Validierung prüft die eingereichte Lösung gegen die ursprüngliche Aussage; laut Paper werden dabei auch Platzhalter für unvollständige Schritte und zusätzlich eingeführte Annahmen zurückgewiesen. [2]

h1 lässt ein Modell an einer persistenten Lean-Datei arbeiten. In einer Iteration kann es in mehreren Denk- und Werkzeugschritten Änderungen vornehmen; nach jeder Bearbeitung erhält es Lean-Rückmeldungen. Am Ende reicht es den Beweis zur externen Prüfung ein. Wird dieser abgelehnt, fasst ein Reflexionsmodell den bisherigen Verlauf, hilfreiche Fortschritte und Fehlerhinweise zusammen. Das Sprachmodell kann anschließend mit diesem komprimierten Kontext und dem aktuellen Arbeitsstand weiterarbeiten, bis ein Beweis akzeptiert wird oder das Kostenlimit greift. [2]

Zum Werkzeugkasten zählen laut Paper unter anderem Suchfunktionen für die Mathematikbibliothek Mathlib, die Inspektion von Definitionen, Tests von Beweisfragmenten in einer Lean-REPL sowie Rückmeldungen über den Sprachserver. Der entscheidende Unterschied zu stärker orchestrierten Systemen: h1 schreibt nicht vor, wie das Problem in Teilbeweise zu zerlegen ist oder welche Suchstruktur einzuhalten ist. Das Modell entscheidet, welche Werkzeuge es nutzt und wie es den Beweis entwickelt. [2]

Benchmarks decken unterschiedliche Schwierigkeitsgrade ab

PutnamBench umfasst laut Paper 672 Aufgaben aus früheren Putnam-Wettbewerben. Für kontrollierte Vergleiche mit AxProverBase verwendet das Team zusätzlich Putnam100, eine Teilmenge von 100 Aufgaben. FATE-X enthält 100 Algebraaufgaben auf oder oberhalb des Niveaus von Promotionsqualifikationsprüfungen. FormalConjectures100-Solved ist eine zufällige Auswahl von 100 formalisierten Forschungsproblemen, für die bereits informelle Lösungen bekannt sind. [2]

Die Auswahl ist relevant für die Interpretation der Resultate: PutnamBench dient den Autoren vor allem dazu, Effizienz zu vergleichen; FATE-X und FormalConjectures100-Solved seien bei den untersuchten Budgets noch nicht ausgeschöpft. Daneben betrachtet das Paper offene Forschungsprobleme, bei denen keine bekannte Lösung als Vorlage dient. Die Ergebnisse auf Wettbewerbsaufgaben, lösbaren formalisierten Aussagen und offenen Vermutungen messen daher nicht alle dieselbe Fähigkeit. [2]

Die Autoren berichten außerdem, h1 habe offene Probleme aus Formal Conjectures gelöst. Bei der Zahl ist eine Abweichung zwischen den bereitgestellten Fassungen zu beachten: Die arXiv-Fassung und die Hugging-Face-Seite nennen acht, die OpenReview-Zusammenfassung neun. Die Texte erklären nicht, ob sich die Differenz aus einem anderen Versionsstand oder einer abweichenden Zählung ergibt; sie sollte deshalb nicht zu einer scheinbar einheitlichen Zahl zusammengezogen werden. [1][2][3]

Vergleiche sprechen für längere Einzelversuche – unter bestimmten Bedingungen

Ein zentraler Befund betrifft die Frage, ob es günstiger ist, mehrere voneinander getrennte Versuche zu starten oder einen einzelnen Lauf länger fortzusetzen. Für fünf offene Erdős-Probleme berichten die Autoren, dass ein länger laufender h1-Versuch bei den betrachteten Kosten AlphaProof Nexus’ einfachem Agenten in drei Versuchen überlegen sein und auch den vollständigen AlphaProof-Nexus-Ansatz übertreffen könne. Die Aussagen beziehen sich auf die untersuchten Aufgaben und die im Paper vorgenommenen Vergleiche; sie belegen keine allgemeine Regel für alle offenen mathematischen Probleme. [2]

Dafür ist die Kennzahl pass@1 allein nur eingeschränkt aussagekräftig. Die Autoren weisen darauf hin, dass ein „Versuch“ je nach System sehr unterschiedliche Mengen an Inferenz umfassen kann: Ein verglichener Workflow kann innerhalb eines einzelnen Versuchs zahlreiche Überarbeitungen oder Agentenschritte zulassen. h1 variiert dagegen die verfügbare Rechenzeit, indem es denselben Lauf fortsetzt. Ein Vergleich gleicher Versuchszahlen ist deshalb nicht automatisch ein Vergleich gleicher Rechenbudgets. [2]

Die Arbeit stellt Kosten-Erfolgs-Kurven in den Vordergrund und vergleicht Inferenzkosten bei möglichst gleichem Modell. Die angegebenen Dollarbeträge sind laut Methodenbeschreibung API-äquivalente Schätzungen aus aufgezeichnetem Tokenverbrauch und angesetzten Tarifen. Das Team merkt zudem an, dass Ausgabetoken bis zu hundertmal so viel kosten können wie gecachte Eingabetoken. Ein System, das Kontext wiederverwendet oder weniger unnötige Ausgabe produziert, kann somit bei gleicher nomineller Versuchszahl deutlich andere Kosten verursachen. [2]

Die Schnittstelle bleibt ein wichtiger Teil des Systems

Die Arbeit argumentiert nicht, dass die Gestaltung des Harness bedeutungslos sei. In den beschriebenen Ablationen und Vergleichen mit AxProverBase, Claude Code und weiteren einfachen Schleifen sehen die Autoren erhebliche Unterschiede bei Erfolgsquote und Kosten. Als wichtige Faktoren nennen sie eine effiziente und zuverlässige Lean-Anbindung, unmittelbares Ausführungsfeedback, die Möglichkeit, Reparaturen fortzusetzen, Reflexion über frühere Schritte sowie effiziente Nutzung und Zwischenspeicherung von Kontext. [2]

Das unterstreicht eine Unterscheidung zwischen weniger Prozessvorgaben und weniger technischer Infrastruktur. h1 verzichtet nach Darstellung der Autoren auf eine festgeschriebene Beweiszerlegung, bietet dem Modell aber gezielte Bearbeitungsmöglichkeiten, Compiler-Rückmeldungen und Werkzeuge zur Suche und Prüfung. „Einfach“ bedeutet hier daher nicht, dass ein Sprachmodell ohne unterstützende Umgebung arbeitet. [2]

Für Unternehmen, die KI-Agenten in strukturierte Software- oder Verifikationsumgebungen einbinden, ergibt sich daraus eine begrenzte, aber praktische Analyse: Bevor Sie zusätzliche Agentenrollen und Prozessschritte einführen, sollten Sie messen, wie gut Ihr Modell mit schneller, verlässlicher Rückmeldung und einem fortsetzbaren Arbeitsstand arbeitet. Das ist keine im Paper getestete Aussage über beliebige Unternehmensanwendungen, sondern eine Übertragung der dortigen Befunde auf ähnliche Umgebungen mit maschinell überprüfbaren Zwischenschritten. [2]

Was die Resultate belegen – und was nicht

Die Autoren beschreiben ihre Befunde als Spitzenresultate auf mehreren Benchmarks und berichten bei ausgewählten Vergleichen Vorteile gegenüber spezialisierten Systemen. In der arXiv-Fassung heißt es etwa, h1 mit DeepSeek V4 Flash übertreffe auf PutnamBench die dort betrachtete Goedel-Architect-Variante nach der Pareto-Abwägung von Kosten und Erfolg; mit GPT-5.5 löse h1 alle als lösbar betrachteten Aufgaben, wie es laut Abbildungsbeschreibung auch Humanfia und Aleph Prover tun, jedoch zu geringeren Kosten. Diese Aussagen sind an konkrete Modelle, Baselines und Testbedingungen gebunden. [2]

Auch die OpenReview-Seite führt den Beitrag als Einreichung für ICLR 2027 und fasst die Ergebnisse zugunsten von h1 zusammen. Der bereitgestellte Eintrag weist ihn als „Conference Submission“ aus; daraus lässt sich keine Annahme oder unabhängige Replikation ableiten. Die Übereinstimmung zwischen arXiv- und OpenReview-Zusammenfassung stärkt die Aussage, was die Autoren beanspruchen, ersetzt aber keine externe Validierung der Experimente. [2][3]

Für die Einordnung sind zudem die gewählten Vergleichsbedingungen wichtig. Das Paper versucht, Modelle oder Harnesses getrennt zu vergleichen und Inferenzkosten einzubeziehen, weist aber selbst darauf hin, dass frühere Arbeiten Versuchszahlen mit sehr unterschiedlichen Rechenumfängen verwendet haben. Die SOTA-Aussagen gelten ausdrücklich für einen festgelegten Vergleichsstand und die untersuchten Benchmarks; daraus folgt nicht, dass h1 auf jeder mathematischen Aufgabe oder mit jedem Modell überlegen ist. [2]

Implikation für die Entwicklung von KI-Agenten

Die Studie verschiebt den Schwerpunkt von der Frage „Wie viele Agenten und Planungsebenen braucht ein System?“ hin zu „Wie effizient kann ein Modell mit seiner Ausführungsumgebung interagieren und aus Rückmeldungen weiterarbeiten?“. Für formale Beweise ist diese Umgebung besonders gut messbar, weil Lean fehlerhafte oder unvollständige Beweise zurückmelden und akzeptierte Beweise mechanisch prüfen kann. Das macht den Ansatz aussagekräftig für formal verifizierbare Aufgaben, aber nicht automatisch für Tätigkeiten ohne einen vergleichbaren Prüfer. [2]

Für die Beschaffung und Entwicklung solcher Systeme ist daher eine getrennte Bewertung von Modell, Harness und Budget sinnvoll. Analytisch folgt aus dem Paper, dass ein Benchmarkwert ohne Angaben zu Modellversion, erlaubter Inferenz, Werkzeuginteraktionen und Kosten nur begrenzt vergleichbar ist. Wenn Sie Agentenlösungen bewerten, sollten Sie Erfolg und Aufwand gemeinsam betrachten und prüfen, ob ein System tatsächlich mit weniger Kosten zum selben Ergebnis kommt – statt nur Versuche oder Agentenschritte zu zählen. [2]

Die zentrale Aussage der Arbeit ist damit enger als ein generelles Plädoyer gegen komplexe Agentenarchitekturen: In den untersuchten Lean-Aufgaben können ein leistungsfähiges Modell, effizientes Prüferfeedback und die Möglichkeit zur Fortsetzung spezialisierte Workflows konkurrenzfähig machen. Ob das auch in anderen strukturierten Umgebungen gilt, bleibt eine zu prüfende Übertragung und ist durch die vorliegenden Beweisbenchmarks allein nicht nachgewiesen. [1][2]

Quellen

1. [1] Paper page - h1: A Taste of the Bitter Lesson in Automated Theorem Proving — https://huggingface.co/papers/2610.35962 (abgerufen am 2026-10-28)
2. [2] h1 : A Taste of the Bitter Lesson in Automated Theorem Proving — https://arxiv.org/html/2610.35962v1 (abgerufen am 2026-10-28)
3. [3] h1: A Taste of the Bitter Lesson in Automated Theorem Proving | OpenReview — https://openreview.net/forum?id=XPRucpRJls (abgerufen am 2026-10-28)