🤖 AI

HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs

Das Papier stellt Hermes vor, ein neuartiges werkzeuggestütztes Agentensystem, das informelles Schließen mit formal verifizierten Beweisen in Lean verzahnt, um im Vergleich zu bestehenden Ansätzen eine genauere, effizientere und verifizierbare mathematische Argumentation in großen Sprachmodellen zu erreichen.

Ursprüngliche Autoren: Azim Ospanov, Zijin Feng, Jiacheng Sun, Haoli Bai, Xin Shen, Farzan Farnia

Veröffentlicht 2026-06-01

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Azim Ospanov, Zijin Feng, Jiacheng Sun, Haoli Bai, Xin Shen, Farzan Farnia

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, ein sehr schwieriges mathematisches Rätsel zu lösen. Sie haben einen brillanten, aber etwas zerstreuten Assistenten (das Large Language Model, oder LLM), der großartig darin ist, Ideen zu brainstormen und lange, kreative Erklärungen zu schreiben. Der Assistent macht jedoch manchmal kleine logische Fehler, wird verwirrt oder „halluziniert“ Fakten, die richtig klingen, aber nicht wahr sind.

Auf der anderen Seite haben Sie einen strengen, unnachgiebigen Mathematik-Richter (ein formales Beweissystem namens Lean). Dieser Richter macht niemals Fehler, ist aber auch sehr starr. Er versteht Ihr kreatives Brainstorming nicht; er akzeptiert nur perfekt strukturierten, formalen Code. Wenn Sie ihm eine unordentliche Erklärung geben, sagt er nur: „Fehler.“

Hermes ist ein neues Werkzeug, das als Übersetzer und Qualitätskontrollmanager zwischen Ihrem kreativen Assistenten und dem strengen Richter fungiert. Es lässt Ihren kreativen Assistenten frei arbeiten, hält ihn aber nach jedem Schritt an, um den strengen Richter zu fragen: „Ist dieser spezifische Schritt tatsächlich wahr?“

So funktioniert Hermes, unterteilt in einfache Teile:

1. Das Problem: Der „lange Spaziergang“ vs. die „strenge Prüfung“

Der alte Weg (Informelle Argumentation): Ihr Assistent versucht, die gesamte Lösung in einem einzigen langen Gedankenstrom zu entwickeln. Er ist flexibel und schnell, aber wenn er frühzeitig eine falsche Abbiegung nimmt, könnte er noch lange in die falsche Richtung weiterlaufen, bevor er den Fehler bemerkt. Es ist, als würde man ein Auto mit geschlossenen Augen fahren, in der Hoffnung, nicht gegen eine Wand zu prallen.
Der andere Weg (Formale Beweisführung): Ihr Assistent versucht, von Anfang an einen strengen Code zu schreiben. Das ist perfekt genau, aber es ist so langsam und schwierig, dass der Assistent oft stecken bleibt oder aufgibt. Es ist, als würde man versuchen, ein Haus Stein für Stein zu bauen, während man jeden einzelnen Stein gegen einen Bauplan prüft, bevor man den nächsten setzt.

2. Die Hermes-Lösung: Das „Checkpoint“-System

Hermes kombelt das Beste aus beiden Welten. Es lässt Ihren Assistenten einige Schritte seiner kreativen Erklärung schreiben und führt dann einen „Checkpoint“ durch.

Der Übersetzer (Formalisierungsmodul): Wenn der Assistent sagt: „Daraus folgt, dass der Winkel 45 Grad beträgt“, übersetzt Hermes diesen Satz in den strengen Code, den der Richter versteht.
Der Richter (Beweismodul): Der strenge Richter überprüft diesen Code.
- Wenn er besteht: Großartig! Hermes speichert diesen Schritt in einer Gedächtnisbank und sagt dem Assistenten: „Du bist auf dem richtigen Weg, mach weiter.“
- Wenn er fehlschlägt: Der Richter sagt: „Nein, das ist falsch.“ Hermes sagt zum Assistenten: „Stopp! Du hast hier einen Fehler gemacht. Geh zurück und korrigiere ihn.“
Die Gedächtnisbank: Da mathematische Probleme oft lange Ketten von Logik beinhalten, erinnert sich Hermes an alle Schritte, die bereits erfolgreich geprüft wurden. Dies stellt sicher, dass der Assistent die bereits bewiesenen Regeln nicht vergisst, wodurch die gesamte Argumentation konsistent bleibt.

3. Warum es besser ist (Die Ergebnisse)

Das Paper testete Hermes bei schwierigen Mathematik-Wettbewerben (wie AIME und HARDMath2) unter Verwendung verschiedener KI-Modelle.

Genauigkeit: Hermes machte die KI viel intelligenter. Bei den schwierigsten Problemen verbesserte Hermes die Erfolgsquote der KI um bis zu 40 %. Es stoppte die KI dabei, selbstbewusst falsche Antworten zu geben.
Effizienz: Man könnte denken, dass das Überprüfen jedes Schritts langsam und teuer wäre. Überraschenderweise war Hermes tatsächlich schneller und kostengünstiger (in Bezug auf die Rechenleistung) als andere Methoden, die versuchen, 5 oder 10 verschiedene Antworten zu generieren und die beste auszuwählen. Es ist wie das Nehmen eines direkten, verifizierten Pfades gegenüber dem Umherirren in einem Labyrinth, während man 10 verschiedene Routen ausprobiert.
Klarheit: Im Gegensatz zu anderen Methoden, die nur sagen: „Diese Antwort ist zu 80 % wahrscheinlich richtig“, liefert Hermes ein klares „Ja“ oder „Nein“ für spezifische Schritte, was es einfacher macht zu sehen, warum eine Antwort korrekt oder falsch ist.

Das Fazit

Hermes ist wie ein intelligenter, automatisierter Editor, der die Arbeit Ihres kreativen Mathematik-Assistenten in Echtzeit überprüft. Es hindert den Assistenten nicht daran, kreativ zu denken; es stellt nur sicher, dass er nicht von einer Klippe stürzt. Das Ergebnis ist eine KI zur Lösung mathematischer Probleme, die nicht nur genauer, sondern auch effizienter und leichter zu vertrauen ist.

Technisches Resümee: HERMES – Hin zu effizienter und verifizierbarer mathematischer Argumentation in LLMs

1. Problemstellung

Große Sprachmodelle (LLMs) haben durch informelle Methoden wie Chain-of-Thought (CoT) eine signifikante Kompetenz in der mathematischen Argumentation bewiesen. Rein informelles Schließen ist jedoch anfällig für logische Lücken, subtile Fehler und Halluzinationen, insbesondere bei langen Argumentationsketten. Formale Theorembeweissysteme (z. B. Lean4, Coq) bieten zwar rigorose, maschinell verifizierbare Argumentation, lassen aber oft die explorative Flexibilität und Ausdrucksstärke der natürlichen Sprachproblemlösung vermissen. Aktuelle Ansätze, die diese Lücke zu schließen versuchen – wie etwa Process Reward Models (PRMs) und Outcome Reward Models (ORMs) – verlassen sich auf Black-Box-Evaluatoren, die numerische Scores zuweisen, ohne eine explizite Verifizierung der mathematischen Korrektheit vorzunehmen. Darüber hinaus erfordern diese belohnungsbasierten Methoden eine erhebliche menschliche Kuratierung und können die Stochastik und die Biases der als Evaluatoren genutzten LLMs erben, was zu einer Fehlleitung (Misalignment) gegenüber der tatsächlichen schrittweisen Korrektheit führt.

Die Kernherausforderung, die mit dieser Arbeit adressiert wird, ist das Fehlen eines prinzipgesteuerten Mechanismus, mit dem LLM-basierte Mathematik-Agenten die Flexibilität informeller Argumentation mit der Verifizierbarkeit formaler Beweise kombinieren können – und zwar in einer Weise, die sowohl effizient als auch interpretierbar ist.

2. Methodik: Das Hermes-Framework

Die Autoren führen Hermes ein (Hybrid Agent for Reasoning in Mathematics with NEuro-Symbolic Lean4 verification), einen multi-modularen, werkzeuggestützten Agenten, der darauf ausgelegt ist, informelle Argumentation mit formal verifizierten Beweisen in Lean4 zu verzahnen. Das Framework arbeitet durch einen iterativen Inferenzprozess, der aus vier Schlüsselmodulen besteht:

Reasoning LLM: Generiert natürliche Sprachschritte der Argumentation. Das Modell wird angewiesen, jeden kritischen mathematischen Schritt, der zum finalen Beweis beitsteuert, zu verifizieren.
Formalisierungsmodul: Übersetzt den natürlichen Sprachbeweisschritt in eine entsprechende Lean4-Aussage. Um die semantische Treue zu gewährleisten, nutzt dieses Modul einen zweistufigen Verifizierungsprozess:
1. Kompilierungsprüfung: Der generierte Lean-Code muss erfolgreich kompilieren.
2. Rückübersetzung: Der kompilierte Lean-Code wird zurück in natürliche Sprache übersetzt. Das LLM evaluiert die Äquivalenz zwischen dem ursprünglichen Schritt und der rückübersetzten Version.
  Dieser Prozess wird bis zu einem Budget $K_f$ wiederholt, um eine gültige Formalisierung sicherzustellen.
Prover-Modul: Erhält die validierte Lean-Aussage und versucht, das Ziel oder dessen Negation ( $\neg \text{goal}$ ) unter Verwendung einer Kombination aus einem Modell zur Generierung des Gesamtbeweises (z. B. Goedel-Prover-V2) und eingebauten Lean-Solvern zu beweisen. Dieses Modul operiert unter einem Sampling-Budget $K_p$ . Es gibt ein binäres Signal zurück: CORRECT (Beweis gefunden), INCORRECT (Gegenbeweis gefunden) oder VERIFICATION FAILURE (unfähig zu beweisen oder zu widerlegen).
Memory Block: Eine strukturierte Datenbank, die validierte Beweisschritte zusammen mit ihren Vektorrepräsentationen speichert. Sie nutzt einen Top- $k$ -Retrieval-Mechanismus, um relevanten, zuvor verifizierten Kontext in den aktuellen Argumentationsschritt einzuspeisen, wodurch Kontinuität gewährleistet und die Fehlerfortpflanzung über lange Argumentationsketien hinweg verhindert wird.

Feedback-Schleife: Basierend auf dem Signal des Provers kann das LLM entweder mit dem aktuellen Argumentationspfad fortfahren (wenn verifiziert), den Schritt revidieren (wenn ein Gegenbeweis gefunden wurde) oder alternative Ansätze explorieren. Das System ist modular aufgebaut, sodass Komponenten wie der Autoformalizer oder der Prover ausgetauscht werden können, sobald diese sich verbessern.

Komplexitätsanalyse: Die Autoren liefern eine theoretische Analyse der Token-basierten Inferenzkomplexität. Sie argumentieren, dass Hermes, welches die Verifizierung während der Inferenz auf einer Teilmenge kritischer Schritte verzahnt, eine Komplexität von $O(\tilde{T} K N^2)$ aufweist. Dies ist theoretisch durch die Komplexität von PRM-basierten Methoden ( $O(T K N^2)$ ) begrenzt und signifikant effizienter als das Generieren mehrerer vollständiger Spuren für eine Best-of-N-Selektion.

3. Zentrale Beiträge

Das Paper beansprucht die folgenden primären Beiträge:

Erster Werkzeug-basierter Lean4-Agent: Hermes wird als der erste werkzeugbasierte Agent präsentiert, der im Zuge der Inferenz durchführbare Zwischenbeweisschritte verifiziert und den LLMs so Korrektheitssignale aus einem Kernel-basierten Compiler statt aus einem gelernten Belohnungsmodell zur Verfügung stellt.
Lean4-gestützter Speicher: Die Einführung eines Memory Blocks, der Zwischenbehauptungen akkumuliert und validiert, um die Konsistenz über die Schritte hinweg sicherzustellen und die Fehlerfortpflanzung in langen Argumentationsketten zu reduzieren.
Gewinne bei Effizienz und Genauigkeit: Empirische Belege zeigen, dass Hermes die Argumentationsgenauigkeit verbessert und gleichzeitig den Token-Verbrauch sowie die Rechenkosten im Vergleich zu belohnungsbasierten Ansätzen erheblich senkt.

4. Experimentelle Ergebnisse

Das Framework wurde auf vier anspruchsvollen Benchmarks für mathematische Argumentation evaluiert: MATH-500, AIME'25, CollegeMath und HARDMath2, unter Verwendung von LLMs unterschiedlicher Skalierung (Qwen3-8B, OpenAI o3-mini, DeepSeek-V3.1/V3.2).

Verbesserungen der Genauigkeit: Über alle Einstellungen hinweg übertraf Hermes konsistent Zero-Shot CoT, Majority Vote und verschiedene Reward-Modell-Baselines (ORMs und PRMs).
- Im Durchschnitt verbesserte Hermes die Genauigkeit über die vier Benchmarks hinweg um 23%.
- Auf dem schwierigen AIME'25 Datensatz erreichte Hermes eine 40%ige Steigerung der Genauigkeit gegenüber dem Basismodell (z. B. DeepSeek-V3.2), während es im Vergleich zu belohnungsbasierten Methoden 80% weniger Inferenz-FLOPs verbrauchte.
- Bei der Skalierung zur Testzeit (Hermes@5 mit Best-of-N Sampling) verbesserte sich die Genauigkeit zusätzlich um weitere 20%.
Effizienz: Hermes nutzte signifikant weniger Token als Score-basierte Methoden (Safe, ORMs, PRMs). Während belohnungsbasierte Methoden oft 5–60 Argumentationsspuren generieren mussten, um eine konkurrenzfähige Genauigkeit zu erreichen, erzielte Hermes mit einer einzigen Spur (@1) oder minimalem Sampling überlegene Ergebnisse und reduzierte die Token-Budgets um den Faktor 4–6.
Ablationsstudien: Das Entfernen des Prover-Moduls verursachte den größten Leistungsabfall (z. B. ein relativer Rückgang von 25% auf AIME), was die Notwendigkeit der Beweis-Suchmaschine unterstreicht. Das Entfernen des Memory-Buffers störte die Kontinuität der Argumentation, insbesondere bei schwierigeren Datensätzen mit längeren Argumentationsketten.
Domänensensitivität: Die Leistungssteigerungen waren auf schwierigeren Datensätzen (HARDMath2, AIME) im Vergleich zu leichteren (MATH-500) am ausgeprägtesten, was darauf hindeutet, dass Hermes besonders effektiv bei der Korrektur von Fehlern in fortgeschrittener Argumentation ist. Das System zeigte eine starke Leistung in Algebra und Gleichungen (wo Mathlib dicht besetzt ist) und etwas geringere Zuwächse in der Geometrie, was auf den aktuellen Stand der formalen Bibliothek zurückzuführen ist.

5. Bedeutung und Ansprüche

Die Autoren positionieren Hermes als einen bedeutenden Schritt zur Vereinigung von informeller und formaler mathematischer Argumentation. Sie behaupten, dass das Framework durch die Integration formaler Verifizierung direkt in den Argumentationszyklus Folgendes bietet:

Interpretierbarkeit: Im Gegensatz zu Black-Box-Belohnungsmodellen liefert Hermes explizites Feedback zur Korrektheit auf Schrittebene und zeigt auf, warum ein Argumentationspfad valide oder fehlerhaft ist.
Skalierbarkeit und Modularität: Das Design ermöglicht die nahtlose Integration verbesserter Autoformalizer und Prover, sobald sich das Feld weiterentwickelt, und stellt sicher, dass das System über die aktuellen Fähigkeiten von Lean4 hinaus relevant bleibt.
Ressourceneffizienz: Die Arbeit zeigt, dass qualitativ hochwertige mathematische Argumentation nicht zwangsläufig massive Rechenbudgets erfordert, die mit der Generierung tausender Kandidaten-Spuren verbunden sind; stattdessen liefern gezielte, verifizierbare Zwischenprüfungen überlegene Effizienz und Genauigkeit.

Das Paper schließt mit der Feststellung, dass Hermes eine Bewegung hin zu skalierbaren, verifizierbaren und interpretierbaren Agenten für mathematische Argumentation darstellt, die die Lücke zwischen der Flexibilität von LLMs und der Strenge formaler Theorembeweise effektiv überbrückt.