FormaRL: Autoformalisation ohne gelabelte Daten verbessert

In der formalen Verifikation ist die automatische Formalisierung ein zentrales Ziel, das bislang durch fehlende Daten und ineffiziente Methoden gehemmt war. Mit dem neuen Ansatz FormaRL wird dieses Hindernis überwunden: Das System nutzt nur wenige unlabelte Daten und kombiniert dabei einen Syntax‑Check des Lean‑Compilers mit einer Konsistenzprüfung durch ein großes Sprachmodell, um die Belohnung zu bestimmen. Anschließend wird der Formalisierer mit dem GRPO‑Algorithmus optimiert.

Um die Forschung weiter voranzutreiben, hat das Team ein neues Datenset namens uproof aus Lehrmaterialien der Grundstudiengänge Mathematik zusammengestellt. Dieses Set ermöglicht die Untersuchung von Autoformalisation und Theorem‑Proving in fortgeschrittener Mathematik.

Die Ergebnisse sind beeindruckend: Auf dem Benchmark ProofNet steigt die Pass@1‑Genauigkeit von 4,04 % auf 26,15 % – ein Mehrfacher von 4 bis 6. Auf dem eigenen uproof‑Set verbessert sich die Genauigkeit von 2,4 % auf 9,6 %. Darüber hinaus zeigt FormaRL bei Aus‑der‑Distribution‑Tests eine starke Steigerung: Pass@1 von 6,2 % auf 9,6 % und Pass@16 von 24,4 % auf 33,6 %. Diese Fortschritte übertreffen die aktuellen Open‑Source‑State‑of‑the‑Art‑Autoformalizer.

Der Trainingscode von FormaRL ist frei verfügbar unter https://github.com/THUNLP-MT/FormaRL und eröffnet neue Möglichkeiten für die automatisierte Formalisierung in der Mathematik und darüber hinaus.