Neues Verfahren verbessert Autoformalierung durch direkte Abhängigkeitsabfrage

In einer aktuellen Veröffentlichung auf arXiv wird ein innovatives Verfahren vorgestellt, das die automatische Formalisierung mathematischer Aussagen deutlich verbessert. Durch die Kombination von Deep‑Learning‑Techniken mit einer neuen Retrieval‑Strategie namens Direct Dependency Retrieval (DDR) gelingt es, die Lücke zwischen informellen Beschreibungen und maschinell prüfbaren Darstellungen zu schließen.

Traditionelle Ansätze zur Autoformalierung leiden häufig unter fehlender Kontextsensitivität, was zu „Halluzinationen“ von falschen Definitionen und Sätzen führt. Zudem zeigen bestehende retrieval‑augmentierte Methoden oft niedrige Präzision und Recall bei der Suche nach passenden Bibliotheksabhängigkeiten und sind nicht skalierbar genug, um mit der stetig wachsenden Menge an öffentlichen Datenbanken Schritt zu halten.

DDR löst diese Probleme, indem es direkt aus der natürlichen Sprachbeschreibung potenzielle Bibliotheksabhängigkeiten generiert und deren Existenz mittels eines effizienten Suffix‑Array‑Checks verifiziert. Diese schnelle Suchmethode ermöglichte die Erstellung eines umfangreichen Datensatzes mit über 500.000 Beispielen, auf dem ein hochpräziser DDR‑Modell feinabgestimmt wurde.

Die experimentellen Ergebnisse zeigen, dass DDR die führenden Methoden in Bezug auf Retrieval‑Präzision und Recall deutlich übertrifft. Ein Autoformalizer, der DDR nutzt, erzielt konsistente Vorteile bei der Genauigkeit bei einzelnen Versuchen und bei der Stabilität über mehrere Versuche hinweg im Vergleich zu herkömmlichen, auf Auswahl basierenden Retrieval‑Augmented‑Generation‑Modellen.