Draft-and-Prune: Zuverlässigkeit der Auto-Formalisation für logisches Schließen

Auto-Formalisation (AF) wandelt natürliche Sprachaufgaben in solver‑ausführbare Programme um und ermöglicht symbolischen Solver:innen, logische Schlüsse zu ziehen. In der Praxis sind AF‑Pipelines jedoch fehleranfällig: Programme laufen häufig nicht, oder sie führen zwar aus, aber die semantische Bedeutung ist falsch. Während frühere Ansätze syntaktische Fehler durch Solver‑Feedback korrigieren, bleibt die Reduktion semantischer Fehler ein entscheidendes Hindernis.

Die neue Methode Draft-and-Prune (D&P) arbeitet auf Inferenzzeit und steigert die Zuverlässigkeit von AF‑basiertem logischem Schließen durch Vielfalt und Verifikation. Zunächst werden mehrere natürliche Sprachpläne entworfen, und die Programmgenerierung wird an diesen Plänen orientiert. Anschließend werden ausführbare, aber widersprüchliche oder mehrdeutige Formalisierungen entfernt. Die verbleibenden Pfade werden schließlich mittels Mehrheitsabstimmung aggregiert.

In vier repräsentativen Benchmarks – AR‑LSAT, ProofWriter, PrOntoQA und LogicalDeduction – demonstriert D&P eine deutliche Leistungssteigerung ohne zusätzliche Supervision. Auf AR‑LSAT erreicht D&P mit GPT‑4 eine Genauigkeit von 78,43 % und mit GPT‑4o 78,00 %, was die stärksten AF‑Baselines MAD‑LOGIC und CLOVER deutlich übertrifft. Auf den übrigen Aufgaben erreicht D&P nahezu perfekte Ergebnisse, darunter 100 % bei PrOntoQA und LogicalDeduction.

Diese Ergebnisse zeigen, dass die Kombination aus Planvielfalt, gezieltem Pruning und Mehrheitsabstimmung die Zuverlässigkeit von Auto‑Formalisation erheblich verbessert und damit den Weg für robuste logische Schließsysteme ebnet.