Forschungsarbeit verbindet Lean-Beweissuche mit automatisch erzeugten Codeaufgaben

Hohe Werte auf etablierten Benchmarks

Für EasyProver berichten die Autoren 669 gelöste Aufgaben unter 672 Problemen des PutnamBench sowie Beweise für alle sechs Formalisierungen der Internationalen Mathematik-Olympiade 2026. Bei Codeverifikations-Aufgaben löste das System 597 von 600 Bedingungen aus NTP4VC und alle 189 Aufgaben aus VERINA, jeweils durch einen Beweis oder eine Widerlegung. Diese Formulierung ist relevant: Die Zahlen für NTP4VC und VERINA bedeuten nicht, dass jede Aussage als wahr bewiesen wurde; laut Paper konnten die Aufgaben durch Beweis oder Gegenbeweis entschieden werden. [1][2][4]

Die Arbeit sagt, dass sämtliche ausgewiesenen Resultate kernel-geprüfte Beweise oder Widerlegungen sind. Zugleich beschreibt sie den verwendeten Modellzugang als ein Modell von der Stange ohne zusätzliches Training. Im Methodenteil benennt sie Anthropic Fable-5 und führt aus, dass weder ein separat trainiertes Modell für Beweisstrategien noch ein zusätzliches proprietäres Beweiskorpus verwendet worden sei. Diese Angaben charakterisieren das Versuchsdesign der Autoren; die bereitgestellten Quellen enthalten keine unabhängige Replikation der Messungen. [1][2][4]

Die Autoren ordnen die sehr hohen Quoten als Hinweis darauf ein, dass einige bestehende Benchmarks für leistungsfähige Systeme an Aussagekraft verlieren, wenn viele Aufgaben bereits lösbar sind. Das ist ein Benchmark-Problem, nicht automatisch ein Nachweis, dass entsprechende Systeme in realen Entwicklungsumgebungen dieselbe Zuverlässigkeit erreichen. Die Aufgaben, Laufzeitbudgets und formalen Umgebungen bestimmen, was die Ergebnisse tatsächlich messen. [4]

Aegis erzeugt Verifikationsaufgaben aus Rust

Aegis soll die Lücke zwischen weitgehend gelösten Testsets und schwierigeren Verifikationsfragen verkleinern. Die Pipeline beginnt laut Abstract mit Aufgaben aus dem kompetitiven Programmieren, erzeugt sichere Rust-Lösungen, übersetzt diese mit Aeneas in Lean und lässt anschließend Spezifikationen formulieren. Für jede eingefrorene Aussage wird ein Beweis oder eine Widerlegung erzeugt und mit dem Lean-Kernel geprüft. [1][2][4]

Die Autoren berichten 2.045 differenziell validierte Paare aus Rust-Programm und Lean-Übersetzung sowie 11.533 Kandidatenspezifikationen. Die Aufgaben sollen nicht nur abstrakte Eigenschaften eines Algorithmus betreffen, sondern auch Umsetzungsdetails berücksichtigen: etwa Festbreitenarithmetik, explizite Fehlerfälle, generierte Schleifen, Typumwandlungen und eine funktionale Darstellung veränderlicher Zustände. Das erhöht die Nähe zur konkreten Implementierung, macht die Spezifikation aber nicht automatisch zu einer vollständigen Abbildung aller betrieblichen Anforderungen. [1][2]

Eine zentrale methodische Unterscheidung betrifft das Objekt des Beweises. Ein Aegis-Beweis gilt zunächst für die aus Rust extrahierte Lean-Repräsentation und die daran formulierte Aussage. Die Autoren halten ausdrücklich fest, dass ein Label auch dann für das Lean-Programm korrekt sein kann, wenn die Übersetzung nicht vollkommen wäre; differenzielle Tests sollen gesondert Hinweise darauf liefern, ob Lean-Modell und Rust-Quelle dasselbe Verhalten zeigen. Tests sind hier also eine zusätzliche Validierungsschicht, nicht der formale Beweis selbst. [4]

Die gemessene Schwierigkeit bleibt erheblich

In einer geschichteten Stichprobe von 2.000 Aegis-Aussagen bewies EasyProver 1.054, entsprechend 52,7 Prozent, innerhalb eines Budgets von 30 Minuten pro Aussage. Die Zahl bezieht sich auf diese Stichprobe und darf nicht auf alle 11.533 Kandidatenspezifikationen übertragen werden. Außerdem berichtet das Abstract die Quote der bewiesenen Aussagen in der Stichprobe; daraus folgt nicht, dass alle übrigen Aussagen falsch oder grundsätzlich unbeweisbar wären. [1][2]

Die Autoren sehen die neue Aufgabensammlung als deutlich weniger gesättigt als die etablierten Benchmarks, auf denen EasyProver sehr hohe Erfolgswerte meldet. Für Forschungsteams kann Aegis damit eine Ergänzung für den Vergleich von Beweisern und für Lernverfahren sein, bei denen überprüfbare Beweise als Rückmeldesignal dienen. Die Arbeit nennt beide Verwendungen ausdrücklich; sie berichtet damit jedoch noch keine erfolgreiche Übertragung eines solchen Trainingsverfahrens in ein Produkt. [1][2][4]

Eine zusätzliche Vergleichsfolie bietet VeriBench-FTP, ein auf einer NeurIPS-Workshopseite beschriebenes Lean-4-Benchmark für Codeverifikation. Es umfasst 857 Theoreme aus 140 Programmierproblemen und berichtet für Goedel-Prover V2-8B einen Wert von 39,56 Prozent Pass@32. Die Aufgaben und Auswertungsbedingungen unterscheiden sich von Aegis; die Kennzahlen lassen sich daher nicht als direkter Leistungsvergleich zwischen den Systemen lesen. Sie unterstreichen lediglich, dass Codeverifikation als eigener Benchmarkbereich bereits mit unterschiedlichen Aufgabensammlungen untersucht wird. [5]

Bedeutung für Unternehmen: Prüfwerkzeug, kein Produktnachweis

Für Unternehmen, die formale Methoden evaluieren, liegt der mögliche Nutzen zunächst in einer skalierbaren Testumgebung: Agenten können alternative Beweiswege parallel prüfen, während maschinell kontrollierte Labels Vergleiche zwischen Systemen und wiederholbare Experimente erleichtern sollen. Das ist eine Analyse der beschriebenen Architektur und der von den Autoren genannten Einsatzmöglichkeiten, kein Nachweis für geringere Fehlerquoten in einem konkreten Unternehmenssystem. [1][4]

Besonders bei sicherheitskritischer Software sollte die Trennung zwischen Aussage, Spezifikation und Implementierung im Vordergrund stehen. Eine formale Prüfung kann zuverlässig feststellen, ob ein Beweis die vorgegebene Aussage in der festgelegten Lean-Umgebung erfüllt; ob diese Aussage Geschäftsregeln, Sicherheitsanforderungen und Randfälle richtig erfasst, bleibt eine eigene Engineering-Aufgabe. Bei Aegis kommt die Frage hinzu, wie gut die Lean-Übersetzung das Rust-Programm repräsentiert. Die Arbeit begegnet diesem Punkt mit differenzieller Validierung, weist aber keinen allgemeinen Nachweis für beliebige Rust-Projekte aus. [3][4]

Die vorliegenden Ergebnisse sind deshalb als Fortschritt bei automatisierter formaler Suche und bei der Erzeugung von Evaluationsdaten einzuordnen. Die beschriebenen Aufgaben entstehen aus Wettbewerbsprogrammierung, und die Studie berichtet Benchmarkwerte sowie eine Stichprobenmessung; sie weist keine Einführung in Produktionssystemen, keinen Produktivbetrieb und keine Kosten-Nutzen-Bilanz für Unternehmenscode nach. Für eine Beschaffungs- oder Einsatzentscheidung wären zusätzliche Prüfungen mit den eigenen Spezifikationen, Codebasen und Bedrohungsmodellen erforderlich. Diese Einschätzung folgt aus dem Umfang der berichteten Experimente, nicht aus einer Aussage der Autoren über konkrete Unternehmenseinsätze. [1][4]

Quellenlage und Veröffentlichungsstand

Der arXiv-Eintrag führt Version 1 als am 28. Oktober 2026 eingereicht; die Hugging-Face-Seite nennt den 27. Oktober als Veröffentlichungsdatum. Die bereitgestellten Einträge erklären die abweichenden Plattformangaben nicht. Der arXiv-Datensatz dokumentiert eine Einreichung und verlinkt auf den Volltext; die vorliegenden Quellen nennen keine begutachtete Konferenz- oder Zeitschriftenveröffentlichung. [1][2]

Die zentralen Leistungszahlen stammen aus dem Paper beziehungsweise seiner Zusammenfassung und sind daher als Ergebnisse der Autoren zu verstehen, nicht als unabhängig bestätigte Benchmarks. Die ergänzende Lean-Dokumentation erläutert den Einsatz des Proof Assistants und von Aeneas, während VeriBench-FTP einen eigenständigen Vergleichspunkt für Lean-Codeverifikation liefert. Diese Quellen stützen den technischen Kontext, replizieren aber EasyProver oder Aegis nicht. [3][4][5]

Quellen

1. [1] Paper page - Scaling Lean Theorem Proving for Real-World Code Verification — https://huggingface.co/papers/2610.38174 (abgerufen am 2026-11-01)
2. [2] [2610.38174] Scaling Lean Theorem Proving for Real-World Code Verification — https://arxiv.org/abs/2610.38174 (abgerufen am 2026-11-01)
3. [3] Lean Programming Language — https://lean-lang.org/ (abgerufen am 2026-11-01)
4. [4] Scaling Lean Theorem Proving for Real-World Code Verification — https://arxiv.org/html/2610.38174v1 (abgerufen am 2026-11-01)
5. [5] NeurIPS VeriBench-FTP: A Formal Theorem Proving Benchmark in Lean 4 for Code Verification — https://neurips.cc/virtual/2025/131044 (abgerufen am 2026-11-01)