Fortschritte im automatisierten Theorembeweis durch den Numina-Lean-Agent

Die Forschung im Bereich der Künstlichen Intelligenz (KI) erzielt kontinuierlich Fortschritte, insbesondere in der Fähigkeit von Maschinen, komplexe logische Probleme zu lösen. Ein aktuelles Beispiel dafür ist die Entwicklung des Numina-Lean-Agent, eines agentenbasierten Systems, das darauf abzielt, das formale mathematische Denken zu revolutionieren. Dieses System, das im Rahmen des Projekts Numina entwickelt wurde, verbindet die Stärken grosser Sprachmodelle (LLMs) mit der Präzision des Lean-Beweisassistenten, um mathematische Beweise zu generieren und zu verifizieren.

Die Herausforderung des formalen mathematischen Denkens

Die Automatisierung des Theorembeweises ist seit Langem eine zentrale Herausforderung in der KI. Formale Beweisassistenten wie Lean stellen eine rigorose Umgebung dar, in der jeder Inferenzschritt eines mathematischen Beweises computergestützt verifiziert wird. Dies garantiert die Korrektheit des Beweises, erfordert jedoch einen immensen manuellen Aufwand und akribische Detailgenauigkeit. Herkömmliche LLMs zeigen zwar beeindruckende Fähigkeiten im mathematischen Denken in natürlicher Sprache, tun sich aber schwer damit, präzise und fehlerfreie formale Beweise zu erstellen. Spezialisierte Prover, die für Lean trainiert wurden, sind oft auf bestimmte Domänen beschränkt, schwer zu generalisieren und mit hohen Betriebs- und Wartungskosten verbunden.

Numina-Lean-Agent: Eine innovative Lösung

Der Numina-Lean-Agent, auch als Ax-Prover bekannt, wurde entwickelt, um diese Lücke zu schliessen. Er integriert generalistische LLMs mit dem Lean-Beweisassistenten durch eine Multi-Agenten-Architektur. Das System besteht aus drei Hauptagenten:

• Orchestrator: Dieser Agent verwaltet den gesamten Beweisprozess, weist Aufgaben zu, leitet Feedback weiter und entscheidet über die Beendigung des Prozesses.
• Prover: Der Prover ist das Herzstück des Systems. Er analysiert unbewiesene Theoreme, erstellt Beweisskizzen in natürlicher Sprache und generiert schrittweise Lean-Code. Dabei nutzt er eine Reihe von Lean-Tools, um Ziele zu inspizieren, nach relevanten Ergebnissen zu suchen, Fehler zu lokalisieren und Beweise zu verifizieren.
• Verifier: Der Verifier überprüft die Korrektheit des vom Prover generierten Beweises. Er kompiliert die Lean-Datei und erstellt einen Fehlerbericht. Ein Beweis gilt nur dann als verifiziert, wenn keine Fehler der Stufe 1 vorliegen und keine Platzhalter wie "sorry" oder "admit" enthalten sind.

Ein entscheidender Aspekt des Numina-Lean-Agent ist die Nutzung des Model Context Protocols (MCP), welches den LLMs direkten Zugriff auf Lean-Tools ermöglicht. Dies stellt sicher, dass das System stets mit der neuesten Version der Mathlib-Bibliothek arbeiten kann, ohne neu trainiert werden zu müssen, was die Generalisierbarkeit und Flexibilität erheblich verbessert.

Leistungsbewertung und neue Datensätze

Um die Leistungsfähigkeit des Numina-Lean-Agent zu bewerten, wurden umfangreiche Experimente auf verschiedenen Datensätzen durchgeführt. Neben etablierten Benchmarks wie NuminaMath-LEAN und PutnamBench wurden zwei neue, von den Entwicklern eingeführte Datensätze verwendet:

• AbstractAlgebra (AA): Dieser Datensatz enthält 100 Lean-Probleme aus Standardlehrbüchern der abstrakten Algebra. Im Gegensatz zu bestehenden Benchmarks, die sich auf Wettbewerbsaufgaben konzentrieren, zielt AA auf Mathematik auf Forschungsniveau ab und betont tiefere abstrakte Konzepte.
• QuantumTheorems (QT): Dieser Datensatz umfasst 134 Probleme aus Kernbereichen der Quantentheorie. Er stellt eine erste Brücke zwischen theoretischer Physik und formalen Verifikationsmethoden dar und bietet die Möglichkeit, Prover-Agenten auf Theoreme der Quantenmechanik zu testen.

Ergebnisse und Analyse

Die Ergebnisse zeigen, dass der Numina-Lean-Agent eine starke Leistung über alle Benchmarks hinweg erbringt. Insbesondere auf den neuen Datensätzen AbstractAlgebra und QuantumTheorems übertrifft er spezialisierte Prover und allgemeine LLMs, die nicht mit Lean-Tools ausgestattet sind, deutlich. Auf dem NuminaMath-Datensatz erreichte der Numina-Lean-Agent eine Genauigkeit von 51%, während DeepSeek-Prover bei 28% und Kimina bei 31% lagen. Auf AbstractAlgebra erzielte der Numina-Lean-Agent 64%, verglichen mit 24% für DeepSeek-Prover und 13% für Kimina. Bei QuantumTheorems erreichte das System sogar 96% Genauigkeit, gegenüber 61% für DeepSeek-Prover und 57% für Kimina.

Diese Ergebnisse deuten darauf hin, dass die Flexibilität des agentenbasierten Ansatzes, der die Adaption an verschiedene wissenschaftliche Domänen ermöglicht, ein entscheidender Vorteil gegenüber der Überspezialisierung herkömmlicher Modelle ist. Die Fähigkeit des Systems, diagnostische Meldungen von Lean zu nutzen, um Fehler frühzeitig zu erkennen und zu korrigieren, trägt wesentlich zur Robustheit und Transparenz des Beweisprozesses bei.

Werkzeugnutzung und Kosten-Effizienz

Die Analyse der Werkzeugnutzung zeigte, dass der Prover im Durchschnitt über 100 Tool-Aufrufe pro Lauf tätigt, mit einer Erfolgsquote von über 99%. Besonders häufig genutzte Tools sind "edit file", "lean diagnostic messages", "lean goal", "lean loogle" und "lean leansearch". Diese intensive Nutzung von Tools ermöglicht es dem Numina-Lean-Agent, sich wie ein vorsichtiger Mathematiker zu verhalten: Er entwirft einen Plan, erkundet und implementiert Ideen schrittweise, verifiziert deren Korrektheit in Lean und schreitet nur voran, wenn jeder Schritt validiert wurde.

Hinsichtlich der Bereitstellung und Kosten zeigt sich, dass spezialisierte Prover oft hochspezialisierte Hardware erfordern und mit erheblichen Kosten verbunden sind. Der Numina-Lean-Agent hingegen, der auf API-Aufrufen basiert, ist wesentlich zugänglicher und flexibler in der Bereitstellung. Obwohl die direkten Kosten pro Beweis auf den ersten Blick höher erscheinen mögen, relativiert sich dies, wenn man die hohen Rechenressourcen berücksichtigt, die für spezialisierte Modelle bei höheren "pass@n"-Werten anfallen würden. Zudem wird erwartet, dass die Effizienz des Numina-Lean-Agent mit der fortschreitenden Verbesserung generalistischer LLMs weiter zunehmen wird.

Zusammenarbeit zwischen Mensch und KI

Ein weiteres herausragendes Merkmal des Numina-Lean-Agent ist seine Fähigkeit zur Zusammenarbeit mit menschlichen Forschenden. Im Rahmen einer Fallstudie konnte ein Mathematiker das System nutzen, um ein komplexes kryptographisches Ergebnis zu verifizieren. Das System unterstützte den gesamten Prozess, indem es Zwischenlemmata überprüfte und Beweisstrategien leitete. Überraschenderweise deckte der Numina-Lean-Agent sogar einen Fehler im ursprünglichen informellen Beweis auf. Dies verdeutlicht das Potenzial des Systems, nicht nur bekannte mathematische Ergebnisse zu reproduzieren, sondern auch den Wissensstand durch formale Verifizierung zu erweitern und Fehler in informellen Schlussfolgerungen aufzudecken.

Die Möglichkeit, mit einem KI-Partner zusammenzuarbeiten, der in der Lage ist, Zwischenschritte zu überprüfen und präzises Feedback zu geben, stellt einen Paradigmenwechsel dar. Anstatt menschliches Denken zu ersetzen, ergänzt der Numina-Lean-Agent es und beschleunigt den Verifizierungsprozess erheblich, selbst bei forschungsrelevanten Problemen.

Fazit und Ausblick

Der Numina-Lean-Agent repräsentiert einen bedeutenden Fortschritt im Bereich des automatisierten Theorembeweises in formaler Mathematik. Durch die Kombination der breiten Schlussfolgerungsfähigkeiten von LLMs mit der formalen Strenge von Lean überwindet das System wesentliche Einschränkungen bestehender Ansätze. Seine modulare, agentenbasierte Architektur, die effiziente Werkzeugnutzung und die Fähigkeit zur Mensch-KI-Kollaboration eröffnen neue Möglichkeiten für die Forschung und Anwendung in mathematisch fundierten wissenschaftlichen Disziplinen.

Zukünftige Entwicklungen könnten die Einführung parallelisierter Agenten umfassen, die es dem System ermöglichen, mehrere Beweispfade gleichzeitig zu erkunden, sowie die Integration eines Langzeitgedächtnisses für vergangene Beweise und Interaktionen. Diese Innovationen werden dazu beitragen, das übergeordnete Ziel einer verifizierbaren wissenschaftlichen KI zu erreichen, in der KI-Systeme durch fehlerfreie, formal validierte Schlussfolgerungen zur wissenschaftlichen Entdeckung beitragen.

Bibliographie

- DeepSeek-AI. (2025). DeepSeek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning. arXiv preprint arXiv:2501.12948. - Dressler, O. (2025). Lean-lsp-mcp: Tools for agentic interaction with the lean theorem prover. - Hugging Face. (2026). Daily Papers. Abgerufen am 19. Januar 2026 von https://huggingface.co/papers - Lin, Y., et al. (2025). Goedel-Prover-V2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613. - Mishra, P. R., Kumar, Y., Samanta, S., & Gaur, A. (2024). A new algorithm for computing branch number of non-singular matrices over finite fields. arXiv preprint arXiv:2405.07007. - Model Context Protocol. (2024). What is the model context protocol (mcp)?. Abgerufen am 5. Oktober 2025 von https://modelcontextprotocol.io/docs/getting-started/intro - Moura, L. de, & Ullrich, S. (2021). The lean 4 theorem prover and programming language. In Automated Deduction—CADE 28: 28th International Conference on Automated Deduction, Virtual Event (pp. 625–635). Springer-Verlag. - Numina-Team. (2025). Numinamath-lean dataset. Abgerufen am 24. August 2025 von https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN - Project Numina. (n.d.). Abgerufen am 22. Januar 2026 von https://projectnumina.ai/ - Ren, Z. Z., et al. (2025). DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801. - Rousseau, S. (2024). Bug discovered in quantum algorithm for lattice-based crypto. Abgerufen am 22. April 2024 von https://sebastienrousseau.com/2024-04-22-bug-discovered-in-quantum-algorithm-for-lattice-base-index.html - Tsoukalas, G., et al. (2024). PutnamBench: Evaluating neural theorem-provers on the putnam mathematical competition. Advances in Neural Information Processing Systems, 37, 11545–11569. - Wang, H., et al. (2025). Kimina-Prover Preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354. - Xin, H., et al. (2024). DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. - Zheng, K., Han, J. M., & Polu, S. (2022). miniF2F: a cross-system benchmark for formal olympiad-level mathematics. International Conference on Learning Representations.