Re:Form – Reduzierung menschlicher Vorwissen bei skalierbarer formaler Softwareverifikation mit RL in LLMs: Eine Vorstudie zu Dafny

Bestehende, auf natürlicher Sprache basierende (z. B. menschliche Sprache) große Sprachmodelle (Large Language Models, LLMs), die mit Verstärkendem Lernen (Reinforcement Learning, RL) trainiert werden, stehen vor einer erheblichen Herausforderung: Ihre Verifikationsprozesse, die entscheidende Trainingssignale liefern, sind weder zuverlässig noch skalierbar. Tatsächlich können die gängigen großen proprietären Modelle kaum verifizierbare Programme generieren. Eine vielversprechende, jedoch weitgehend unerforschte Alternative ist die formale, sprachbasierte Reasoning. Die Verankerung von LLMs in strengen formalen Systemen, in denen generative Modelle in formalen Sprachräumen (z. B. Dafny) arbeiten, ermöglicht die automatisierte und mathematisch beweisbare Verifikation ihrer Schlussfolgerungsprozesse und Ergebnisse. Diese Fähigkeit ist entscheidend für die Erreichung einer großflächigen, zuverlässigen formalen Softwareverifikation. Es ist üblich, menschlich annotierte Chain-of-Thought-Unterstützungen und andere menschliche Vorwissen einzusetzen, um die Reasoning- und Codierungsfähigkeiten von LLMs zu induzieren. Leider wird es unannehmbar zeitaufwendig, solche Vorwissen für die Überwachung komplexer Programmieraufgaben bereitzustellen. In dieser Arbeit untersuchen wir systematisch Möglichkeiten, das menschliche Vorwissen zu reduzieren, wobei Dafny als Hauptumgebung für unsere Pilotstudie dient. Unser Prozess basiert hauptsächlich auf der Einführung einer automatisierten und skalierbaren Daten-Kurierungs-Pipeline sowie sorgfältig gestalteter RL-Entwürfe, die mit Feedback aus dem formalen Sprach-Verifikator integriert sind. Wir führen DafnyComp ein, eine Benchmark für komponierbare formale Programme mit automatisch formalisierten Spezifikationen für Spezifikations-Reasoning. Der während der Supervised Fine-Tuning (SFT)-Phase erzielte Effekt ermöglicht es sogar kleinen Modellen (z. B. 0,5B) syntaktisch korrekte und verifizierbare Dafny-Code zu generieren, wodurch sie proprietäre Modelle überbieten. RL mit Regularisierung verbessert die Leistung weiter, wodurch eine stärkere Generalisierung auf außerhalb des Domänenbereichs liegende Aufgaben erreicht wird und die Modelle auf der anspruchsvollen DafnyComp-Benchmark allen starken Baselines überlegen sind.