Zur Autoformaliserung von LLM-generierten Ausgaben für die Anforderungsverifikation

Grundinformationen

• Papier-ID: 2511.11829
• Titel: Towards Autoformalization of LLM-generated Outputs for Requirement Verification
• Autoren: Mihir Gupte, Ramesh S. (General Motors)
• Klassifizierung: cs.CL, cs.AI, cs.FL, cs.LO
• Veröffentlichungsdatum: 18. November 2025 (arXiv-Preprint)
• Papierlink: https://arxiv.org/abs/2511.11829

Zusammenfassung

Dieses Papier untersucht die Machbarkeit der Verwendung von Autoformaliserungstechniken zur Verifikation von Ausgaben großer Sprachmodelle (LLM). Da LLMs Potenzial bei der Umwandlung von natürlichsprachigen Anforderungen in strukturierte Ausgaben (wie Gherkin-Szenarien) zeigen, wird die Frage nach der formalen Verifikation der Genauigkeit dieser Ausgaben zum Schlüsselproblem. Das Forschungsteam führte zwei Versuchsgruppen durch: Die erste Gruppe identifizierte erfolgreich zwei unterschiedlich formulierte natürlichsprachige Anforderungen als logisch äquivalent; die zweite Gruppe identifizierte logische Inkonsistenzen zwischen LLM-generierten Ausgaben und ursprünglichen Anforderungen. Obwohl der Forschungsumfang begrenzt ist, deuten die Ergebnisse darauf hin, dass die Autoformaliserung erhebliches Potenzial bei der Gewährleistung der Treue und logischen Konsistenz von LLM-generierten Ausgaben hat.

Forschungshintergrund und Motivation

1. Kernproblem

Mit der weit verbreiteten Anwendung von LLMs, insbesondere bei der automatischen Generierung von Testszenarien in Ingenieuraufgaben, besteht eine kritische Herausforderung: Es fehlen formale Methoden zur Verifikation, ob LLM-generierte Ausgaben die ursprünglichen natürlichsprachigen Anforderungen korrekt widerspiegeln. Beispielsweise kann nach der Generierung eines Gherkin-Szenarios aus einer Anforderung wie „Wenn die Fahrzeuggeschwindigkeit ≥ 10 und der Sicherheitsgurt nicht angelegt ist, dann Sicherheitsgurt-Warnung aktivieren" nicht gewährleistet werden, dass der generierte Inhalt logisch korrekt ist.

2. Bedeutung des Problems

In sicherheitskritischen Bereichen wie der Automobilindustrie ist die Anforderungsverifikation von entscheidender Bedeutung. Fehlerhafte Anforderungsumwandlungen können zu folgenden Problemen führen:

• Unvollständige oder fehlerhafte Testfälle
• Systemverhalten, das nicht den Erwartungen entspricht
• Potenzielle Sicherheitsrisiken

3. Einschränkungen bestehender Methoden

• Traditionelle Formalisierungsmethoden: Hauptsächlich auf mathematische Theorembeweise angewendet, mangelnde Anwendung auf Ingenieuranforderungsverifikation
• LLM-Bewertungsmethoden: Abhängig von manueller Überprüfung oder heuristischen Methoden, mangelnde strenge logische Verifikation
• Autoformaliserungsforschung: Hauptsächlich auf Datensatzkonstruktion und Modelltraining konzentriert, weniger auf praktische Ingenieuranwendungen

4. Forschungsmotivation

Dieses Papier schlägt vor, Autoformaliserungstechniken auf die Verifikation von LLM-Ausgaben anzuwenden – ein neues Szenario – indem sowohl natürlichsprachige Anforderungen als auch LLM-generierte Ausgaben in formale logische Darstellungen (Lean 4) umgewandelt werden und ein Theorembeweiser zur Verifikation der logischen Äquivalenz verwendet wird.

Kernbeiträge

1. Vorschlag der ersten Autoformaliserungspipeline zur Verifikation von LLM-generierten Ausgaben: Umwandlung von natürlichsprachigen Anforderungen und LLM-Ausgaben in Lean 4-Formalisierungen und Verifikation der logischen Konsistenz durch bidirektionale Äquivalenzbeweise
2. Verifikation von zwei konkreten Anwendungsszenarien:
   • Identifikation der logischen Äquivalenz unterschiedlich formulierter natürlichsprachiger Anforderungen
   • Erkennung logischer Inkonsistenzen zwischen LLM-generierten Ausgaben und ursprünglichen Anforderungen
3. Identifikation kritischer technischer Herausforderungen:
   • Notwendigkeit und Automatisierungsschwierigkeiten der Variablenverankerung (variable grounding)
   • Auswirkungen der LLM-Nichtdeterminismus auf die Formalisierung
   • Behandlung von Mehrdeutigkeiten in natürlicher Sprache
4. Vorschlag zukünftiger Forschungsrichtungen: Grundlegung für den Aufbau eines zuverlässigen Verifikationsrahmens für LLM-Ausgaben

Methodische Details

Aufgabendefinition

Eingabe:

• Ein Paar von Aussagen, deren logische Beziehung verifiziert werden soll (S₁, S₂), die sein können:
  • Zwei natürlichsprachige Anforderungen
  • Eine natürlichsprachige Anforderung und ein LLM-generiertes Gherkin-Szenario

Ausgabe:

• Logische Äquivalenzbeurteilung: Äquivalent (S₁ ↔ S₂ ist beweisbar) oder nicht äquivalent (Beweis fehlgeschlagen)

Einschränkungen:

• Aussagen müssen in Aussagenlogik formalisierbar sein
• Systemkontextinformationen sind für die Variablenverankerung erforderlich

Modellarchitektur

Die Gesamtpipeline besteht aus vier Schlüsselschritten (wie in Abbildung 9 dargestellt):

Schritt 1: Automatische Formalisierung

Verwendung von DeepSeek-Prover-v2 (7B-Modell) zur Umwandlung natürlichsprachiger Aussagen in Lean 4-Propositionen:

-- Beispiel: Formalisierung der Anforderung R1
variable (vehicle_speed_avg : ℝ)
variable (calibratable_speed : ℝ)
variable (seatbelt_active : Bool)
variable (initiate_chime : Bool)

def seatbelt_chime_condition : Prop :=
  (vehicle_speed_avg ≥ calibratable_speed ∨ ¬seatbelt_active) → initiate_chime

Prompt-Vorlage (siehe Anhang A.1):

• Explizite Anforderung zur Generierung von Lean 4 def-Anweisungen
• Spezifikation der Verwendung von Aussagenlogik (Prop-Typ)
• Anforderung, Bedingungen als Implikationen auszudrücken (A ∧ B → C)

Schritt 2: Variablenverankerung (Variable Grounding)

Aktuelle Implementierung: Manuelle Identifikation und Vereinheitlichung von Variablen, die in verschiedenen Formalisierungen auf dasselbe Konzept verweisen

Problembeispiel:

• vehicle_speed_avg in R1 und mean_vehicle_speed in R2 verweisen auf die gleiche physikalische Größe
• Es ist erforderlich, dem Lean-Compiler diese Äquivalenz explizit mitzuteilen

-- Beispiel der manuellen Verankerung
(h_speed : vehicle_speed_avg = mean_vehicle_speed)
(h_belt : seatbelt_active = seatbelt_plugged_in)

Schritt 3: Konstruktion des bidirektionalen Äquivalenzsatzes

Konstruktion eines formalisierten Satzes zur Verifikation der logischen Äquivalenz:

theorem req1_eq_req2 
  (h_grounding : <Variablenverankerungsannahmen>) :
  (Proposition_A) ↔ (Proposition_B) := by
  <Beweisverlauf>

Schritt 4: Automatischer Theorembeweiser

Erneute Verwendung von DeepSeek-Prover-v2 zur Generierung von Lean-Beweiscode:

• Erfolgreicher Beweis → Zwei Aussagen sind logisch äquivalent
• Beweis fehlgeschlagen → Logische Inkonsistenz vorhanden

Technische Innovationen

1. Bereichsübergreifende Anwendungsinnovation: Erste Anwendung von Autoformaliserungstechniken aus dem mathematischen Theorembeweisbereich auf die Verifikation von Softwareingenieuranforderungen
2. Zweischichtige LLM-Verwendung:
   • Erste Schicht: Formalisierungsübersetzung (NL → Lean)
   • Zweite Schicht: Theorembeweiser (Verifikation der Äquivalenz)
3. Fehlerbasierter Verifikationsmechanismus: Nutzung des Fehlschlagens des Theorembeweisers als Indikator für logische Inkonsistenz – eine innovative Methode der negativen Verifikation
4. Identifikation der Variablenverankerung: Explizite Darlegung, dass die Variablenverankerung ein unverzichtbarer Schritt in der Autoformaliserungspipeline ist, was in früheren Forschungen nicht ausreichend betont wurde

Experimentelle Einrichtung

Datensatz

Experiment 1: Anforderungsäquivalenzverifikation

• R1: "If Vehicle Speed Average Driven ≥ CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is inactive then initiate SeatBelt Chime"
• R2: "If mean vehicle speed is greater than CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is not plugged in then initiate chime for seatbelt"

Experiment 2: LLM-Ausgabeverifikation

• R3: "When Front Passenger Seat Belt Status changes to 'Fastened' then the Front Passenger Seat Belt Reminder Indication On shall be set to FALSE."
• G3: Von LLM generiertes Gherkin-Szenario (enthält 4 Beispielzeilen, führt zusätzliche Variablen wie seat_occupancy ein)

Bewertungsmetriken

Qualitative Metriken:

• Lean 4-Kompilierung erfolgreich/fehlgeschlagen
• Theorembeweiser erfolgreich/fehlgeschlagen

Verifikationskriterien:

• Logische Äquivalenz: Satz PA ↔ PB ist beweisbar
• Logische Inkonsistenz: Theorembeweiser fehlgeschlagen oder Lean-Code kann nicht kompiliert werden

Implementierungsdetails

Modellauswahl:

• DeepSeek-Prover-v2 (7B)
• Auswahlgründe:
  1. Trainiert auf Lean 4
  2. Besitzt Fähigkeiten zum Verständnis natürlicher Sprache
  3. Verwendet Unterziel-Zerlegungsstrategie

Formalisierungssprache: Lean 4

• Starke Theorembeweisfähigkeiten
• Präzise logische Ausdrucksfähigkeit
• Kompatibilität mit DeepSeek-Prover-v2

Manuelle Eingriffe:

• Variablenverankerungsschritt vollständig manuell
• Verifikation der Formalisierungsausgabe abhängig vom Lean-Compiler

Experimentelle Ergebnisse

Hauptergebnisse

Experiment 1: Anforderungsäquivalenzverifikation (Erfolgreiches Beispiel)

Formalisierungsausgabe:

• R1 und R2 wurden erfolgreich in Lean-Propositionen umgewandelt (Abbildungen 3, 4)
• Variablenzuordnungen wurden manuell etabliert:
  • vehicle_speed_avg ≡ mean_vehicle_speed
  • seatbelt_active ≡ seatbelt_plugged_in

Verifikationsergebnis (Abbildung 5):

• ✅ Lean-Kompilierung erfolgreich
• ✅ Satz req1_eq_req2 erfolgreich bewiesen
• Schlussfolgerung: R1 und R2 sind logisch äquivalent

Bedeutung: Demonstriert, dass die Pipeline semantisch identische, aber unterschiedlich formulierte Anforderungen erkennen kann, was bei der Anforderungskonsistenzprüfung hilfreich ist.

Experiment 2: LLM-Ausgabeverifikation (Fehlgeschlagenes Beispiel)

Formalisierungsausgabe:

• R3: Einfache Proposition, enthält nur Bedingungen für Sicherheitsgurtwechsel (Abbildung 6)
• G3: Komplexe Proposition, enthält zusätzliche Variablen (seat_occupancy, initial_seatbelt_status) (Abbildung 7)

Wichtige Erkenntnisse:

• G3 führt Variablen ein, die in R3 nicht erwähnt werden
• Logische Struktur ist komplexer (enthält 4 Szenariobeispiele)

Verifikationsergebnis (Abbildung 8):

• ❌ Lean-Code-Kompilierung fehlgeschlagen oder Beweis fehlgeschlagen
• Schlussfolgerung: G3 ist logisch inkonsistent mit R3

Bedeutung: Erfolgreiche Erkennung des „Überproduktions"-Problems von LLM-generierten Ausgaben – Hinzufügung von Einschränkungen, die in der ursprünglichen Anforderung nicht vorhanden sind.

Fallstudienanalyse

Fall: Mehrdeutigkeitsproblem (R4)

Anforderung:

"When the seatbelt is Unfastened and the vehicle is in motion then the Front Passenger Seat Belt Reminder Indication On shall be set to TRUE."

Problem: Die Formalisierung von „vehicle in motion" ist mehrdeutig

Zwei mögliche Formalisierungen (Abbildung 10):

1. pass@1: Boolesche Variable vehicle_in_motion : Bool
2. pass@2: Numerische Variable vehicle_speed > 0

Analyse:

• Beide Formalisierungen können in der Systemsemantik korrekt sein
• Sie sind jedoch in der formalen Logik nicht äquivalent (unterschiedliche Typen)
• Unterstreicht die Auswirkungen der Mehrdeutigkeit natürlicher Sprache auf die Formalisierung

Experimentelle Erkenntnisse

1. Formalisierung hängt von Interpretierbarkeit ab: Die Nichtdeterminismus des LLM führt dazu, dass die gleiche Anforderung möglicherweise unterschiedliche, aber beide „angemessene" Formalisierungen erzeugt
2. Variablenverankerung ist ein Engpass:
   • Der zeitaufwändigste Schritt
   • Erfordert Systembereichswissen
   • Derzeit nur manuell durchführbar
3. Systemkontext ist entscheidend: Das Fehlen expliziter Systemdefinitionen (wie Datenwörterbücher) führt zu Formalisierungsinkonsistenzen
4. Negative Verifikation ist wirksam: Beweisfehlschlag kann logische Inkonsistenz wirksam anzeigen

Verwandte Arbeiten

Datensatzkonstruktion für Autoformaliserung

• ProofNet: Autoformaliserung auf Universitätsniveau Mathematik
• MiniF2F: Olympiade-Niveau Mathematik-Benchmark
• Mehrsprachige Datensätze: Kombiniertes Training mit Lean, Isabelle, Coq verbessert die Leistung

LLM-Trainingsstrategien

• "Entwurf-Skizze-Beweis"-Methode (Jiang et al.): Generierung von Beweisumrissen zur Anleitung der Formalisierung
• Unterziel-Zerlegung: Rekursive Suchstrategie, die von DeepSeek-Prover verwendet wird
• Verstärktes Lernen: Verbesserung der Theorembeweiserfolgsrate

Umgang mit Nichtdeterminismus

• Symbolisches Äquivalenz-Framework: Behandlung von Unterschieden zwischen pass@1 und pass@k
• RAG-Methode: Abruf präziser Formaldefinitionen zur Kontextbereitstellung

Anwendungsbereichserweiterung

• Mathematische Problemlösung: Mathematik von der Oberstufe bis zur Universität
• Codeverifikation: Verifikation der Programm-Korrektheit
• Biomedizin: Faktenchecks

Beitrag dieses Papiers: Erste Anwendung der Autoformaliserung auf Ingenieuranforderungsverifikation und LLM-Ausgabeverifikation, eröffnet neue Anwendungsrichtungen.

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

1. Machbarkeitsverifikation: Die Autoformaliserungspipeline kann effektiv die logische Konsistenz zwischen LLM-generierten Ausgaben und ursprünglichen Anforderungen verifizieren
2. Doppelter Anwendungswert:
   • Anforderungskonsistenzprüfung (Identifikation äquivalenter Anforderungen)
   • Qualitätskontrolle von LLM-Ausgaben (Erkennung logischer Fehler)
3. Konzeptnachweis: Obwohl die Stichprobe begrenzt ist, wurde erfolgreich demonstriert, dass Theorembeweistechniken auf Softwareingenieuraufgaben angewendet werden können

Einschränkungen

1. Skalierungsbeschränkung:
   • Nur 3 Anforderungspaare getestet
   • Mangelnde großflächige Bewertung
   • Keine statistische Signifikanzanalyse
2. Manuelle Abhängigkeit:
   • Variablenverankerung vollständig manuell
   • Zeitaufwändig und fehleranfällig
   • Begrenzt die Skalierbarkeit
3. Modellbeschränkungen:
   • Verwendung eines 7B-Modells (ressourcenbegrenzt)
   • Größere Modelle (671B) könnten bessere Leistungen zeigen
   • Formalisierungsqualität hängt von Modellkapazität ab
4. Mehrdeutigkeit nicht gelöst:
   • Inhärente Mehrdeutigkeit natürlicher Sprache
   • Mangelnde Unterstützung durch Systemontologie
   • Kann mehrere „korrekte", aber nicht äquivalente Formalisierungen erzeugen
5. Bereichsspezifität:
   • Experimente nur auf Automobilsicherheitsanforderungen begrenzt
   • Generalisierungsfähigkeit unbekannt

Zukünftige Richtungen

Das Papier schlägt drei Schlüsselforschungsfragen (RQ) vor:

RQ1: Optimale Formalisierungsmethode

• Erforschung von k-Pass-Strategien (Generierung mehrerer Formalisierungen, Auswahl der wahrscheinlichsten)
• Vergleich von Einzeltransformation und mehrfachem Sampling auf Genauigkeit

RQ2: Automatisierung der Variablenverankerung

• Methode 1: Kontextuelle Einzelformalisierung (Verarbeitung aller Aussagen in einem Aufruf)
• Methode 2: Ähnlichkeitsbasierte Verankerung (Verwendung von Einbettungsabgleich mit Systemontologie)
• Herausforderung: Wie kann die Korrektheit der LLM-Verankerungsannahmen selbst verifiziert werden?

RQ3: LLM-Verifikation in eingeschränkten Systemen

• Aufbau von Wissensgraphen für Systemaktionen
• Entwicklung von LLM-Traversierungsmechanismen
• Verwendung von Autoformaliserung zur Gewährleistung der logischen Konsistenz von Ausgaben
• Anwendungsszenarien: Intelligente Häuser, fahrzeuggestützte Assistenten und andere Systeme mit begrenztem Aktionsraum

Weitere Richtungen:

• Entwicklung automatisierter Variablennormalisierungstechniken
• Integration domänenspezifischer Ontologien (wie Automobilsystem-Datenwörterbücher)
• Erweiterung auf komplexere logische Darstellungen (wie Temporallogik)

Tiefgreifende Bewertung

Stärken

1. Neuartige Problemdefinition:
   • Erste systematische Anwendung der Autoformaliserung auf LLM-Ausgabeverifikation
   • Löst echte Schmerzen in der Ingenieurpraxis
   • Eröffnet neue Forschungsrichtungen
2. Klare Methodik:
   • Einfaches und verständliches Pipeline-Design
   • Verwendung etablierter Werkzeuge (Lean 4, DeepSeek-Prover)
   • Starke Reproduzierbarkeit
3. Tiefgreifende Problemidentifikation:
   • Explizite Darlegung der Kritikalität der Variablenverankerung
   • Tiefgehende Analyse von Mehrdeutigkeitsproblemen
   • Ehrliche Diskussion der Auswirkungen von LLM-Nichtdeterminismus
4. Hoher praktischer Wert:
   • Zielgruppe sicherheitskritischer Bereiche (Automobilindustrie)
   • Direkt anwendbar auf Anforderungsingenieur-Workflows
   • Hilft, die Vertrauenswürdigkeit von LLM-Anwendungen zu verbessern
5. Ausgezeichnete Schreibqualität:
   • Klare Struktur, strenge Logik
   • Detaillierte Prompt-Vorlagen (Anhang)
   • Reichhaltige Abbildungen, leicht verständlich

Mängel

1. Schwerwiegend unzureichende Experimentskala:
   • Nur 3 Stichproben: Keine statistischen Schlussfolgerungen möglich
   • Mangelnde Tests mit unterschiedlichen Bereichen und Komplexitätsgraden
   • Keine Bewertung der Leistung auf größeren Datensätzen
   • Empfehlung: Mindestens 50-100 Anforderungspaare für ausreichende Bewertung erforderlich
2. Mangelnde quantitative Bewertung:
   • Keine Genauigkeits-, Rückruf- und andere Metriken
   • Keine Berichterstattung über Formalisierungserfolgsrate
   • Kein Vergleich mit manueller Verifikation
   • Empfehlung: Erstellung eines annotierten Datensatzes, Berechnung von Präzisionsmetriken
3. Zu viele manuelle Eingriffe:
   • Variablenverankerung vollständig manuell, schwächt Automatisierungsanspruch
   • Keine konkreten Implementierungen von Automatisierungslösungen
   • Fragliche Skalierbarkeit
   • Empfehlung: Mindestens Implementierung eines Prototyp-Autoverankerungssystems
4. Begrenzte Modellauswahl:
   • Nur 7B-Modell aufgrund von Ressourcenbeschränkungen
   • Keine Erforschung von 671B-Modellen oder Alternativen
   • Keine Analyse der Auswirkungen der Modellgröße auf Ergebnisse
   • Empfehlung: Mindestens Vergleich verschiedener Modelle auf kleinen Stichproben
5. Mangelnde Analyse fehlgeschlagener Fälle:
   • Keine detaillierte Analyse der Gründe für Theorembeweisfehlschlag
   • Keine Unterscheidung zwischen Formalisierungsfehlern vs. echten logischen Inkonsistenzen
   • Keine Analyse von falsch positiven/falsch negativen Ergebnissen
   • Empfehlung: Aufbau eines Fehlerklassifizierungssystems
6. Einzelne Bewertungskriterien:
   • Nur abhängig von Lean-Kompilierungserfolg/Fehlschlag
   • Keine Berücksichtigung teilweise korrekter Fälle
   • Mangelnde Analyse feiner Fehlertypen
7. Unbekannte Generalisierungsfähigkeit:
   • Nur Automobilsicherheitsanforderungen getestet
   • Keine Verifikation der Anwendbarkeit in anderen Bereichen (Medizin, Finanzen usw.)
   • Die Besonderheit von Gherkin-Szenarien könnte die Universalität der Methode einschränken

Einfluss

Beitrag zum Bereich:

• ⭐⭐⭐⭐ Konzeptbeitrag hoch: Schlägt neue Forschungsrichtung und Anwendungsszenarien vor
• ⭐⭐ Technischer Beitrag mittel: Hauptsächlich Kombination bestehender Techniken
• ⭐⭐⭐ Praktischer Wert relativ hoch: Löst echte Probleme in der Ingenieurpraxis

Praktischer Wert:

• Kurzfristig: Bietet Anforderungsingenieuren Verifikationsideen
• Mittelfristig: Könnte spezialisierte Anforderungsverifikationswerkzeuge hervorbringen
• Langfristig: Könnte zum Standard-Workflow für LLM-Anwendungsqualitätssicherung werden

Reproduzierbarkeit:

• ✅ Verwendung von Open-Source-Werkzeugen (Lean 4, DeepSeek-Prover)
• ✅ Detaillierte Prompt-Vorlagen bereitgestellt
• ❌ Code oder Daten nicht veröffentlicht
• ❌ Manuelle Schritte schwer reproduzierbar
• Bewertung: ⭐⭐⭐ (Mittel)

Erwarteter Einfluss:

• Könnte mehr Forschung zur formalen Verifikation von LLM-Ausgaben auslösen
• Könnte die Kombination von Anforderungsingenieurwesen und formalen Methoden fördern
• Variablenverankerungsproblem könnte zum neuen Forschungsschwerpunkt werden

Anwendbare Szenarien

Hochgradig anwendbar:

• ✅ Anforderungsverifikation in sicherheitskritischen Systemen (Automobil, Luftfahrt, Medizin)
• ✅ Anforderungskonsistenzprüfung und Deduplizierung
• ✅ Qualitätskontrolle von LLM-generierten Testfällen

Mittelmäßig anwendbar:

• ⚠️ Verifikation komplexer Geschäftslogik (erfordert erweiterte Formalisierungsfähigkeiten)
• ⚠️ Multimodale Anforderungen (z.B. Anforderungen mit Diagrammen)
• ⚠️ Echtzeitsysteme (erfordert Temporallogik-Erweiterung)

Nicht anwendbar:

• ❌ Hochgradig mehrdeutige natürlichsprachige Texte
• ❌ Szenarien ohne explizite Systemdefinition
• ❌ Szenarien, die Echtzeitantwort erfordern (aktuelle manuelle Schritte zu langsam)

Verbesserungsvorschläge

1. Sofort durchführbar:
   • Erweiterung auf mindestens 50 Anforderungspaare
   • Implementierung eines grundlegenden automatischen Verankerungsprototyps
   • Aufbau eines Fehlerklassifizierungssystems
2. Kurzfristige Verbesserungen:
   • Vergleich verschiedener Modellgrößen
   • Einführung quantitativer Bewertungsmetriken
   • Tests in mehreren Bereichen
3. Langfristige Ziele:
   • Vollständige Automatisierung der Pipeline
   • Integration von Domänenwissensgraphen
   • Unterstützung für Temporallogik und komplexe Einschränkungen

Referenzen (Schlüsselliteratur)

1. Weng et al. (2025): Autoformalization in the era of large language models: A survey - Übersichtsliteratur
2. Wu et al. (2022): Autoformalization with large language models - Grundlagenarbeit zur Autoformaliserung
3. Ren et al. (2025): DeepSeek-Prover-v2 - Kernmodell in diesem Papier verwendet
4. Jiang et al. (2022): Draft, sketch, and prove - Unterziel-Zerlegungsmethode
5. de Moura & Ullrich (2021): The Lean 4 theorem prover - Formalisierungssprache

Gesamtbewertung: Dies ist ein konzeptnachweis-orientiertes Explorationspapier, das eine wertvolle neue Forschungsrichtung vorschlägt, aber unter schwerwiegend unzureichender experimenteller Verifikation leidet. Als Preprint und vorläufige Forschung identifiziert es erfolgreich Schlüsselprobleme und bietet einen praktikablen technischen Weg, liegt aber noch weit entfernt von einer reifen Lösung. Der Hauptwert des Papiers liegt in der Problemdefinition und Richtungsweisung, nicht in technischen Durchbrüchen. Es wird empfohlen, dass nachfolgende Arbeiten sich auf die Automatisierung der Variablenverankerung und großflächige Bewertungen konzentrieren.