Re:Form – Reduzierung menschlicher Vorannahmen in der skalierbaren formalen Softwareverifikation mit RL in LLMs: Eine Vorstudie zu Dafny

papers.abstract

Bestehende Large Language Models (LLMs), die auf informeller Sprache (z.B. menschlicher Sprache) basieren und mit Reinforcement Learning (RL) trainiert wurden, stehen vor einer erheblichen Herausforderung: Ihre Verifizierungsprozesse, die entscheidende Trainingssignale liefern, sind weder zuverlässig noch skalierbar. Tatsächlich können die weit verbreiteten großen proprietären Modelle kaum verifizierbare Programme erzeugen. Eine vielversprechende, aber weitgehend unerforschte Alternative ist das formale sprachbasierte Reasoning. Die Verankerung von LLMs in rigorosen formalen Systemen, in denen generative Modelle in formalen Sprachräumen (z.B. Dafny) operieren, ermöglicht die automatische und mathematisch beweisbare Verifizierung ihrer Denkprozesse und Ergebnisse. Diese Fähigkeit ist entscheidend für die Erreichung einer großflächigen, zuverlässigen formalen Softwareverifizierung. Es ist gängige Praxis, menschlich annotierte Gedankenketten (Chain-of-Thought) und andere menschliche Vorannahmen zu verwenden, um die Reasoning- und Programmierfähigkeiten von LLMs zu fördern. Leider wird es unannehmbar aufwendig, solche Vorannahmen für die Überwachung komplexer Programmieraufgaben bereitzustellen. In dieser Arbeit untersuchen wir systematisch Möglichkeiten, menschliche Vorannahmen zu reduzieren, wobei wir die formale Sprache Dafny als Hauptumgebung für unsere Pilotstudie verwenden. Unsere Pipeline stützt sich hauptsächlich auf die Einführung einer automatischen und skalierbaren Datenkuratierungspipeline sowie auf sorgfältige RL-Designs, die mit Feedback des formalen Sprachverifizierers integriert sind. Wir stellen DafnyComp vor, einen Benchmark für kompositionelle formale Programme mit automatisch formalisierten Spezifikationen für die Spezifikationslogik. Unser überwachter Feinabstimmungsprozess (Supervised Fine-Tuning, SFT) ermöglicht es sogar kleinen Modellen (z.B. 0,5B), syntaktisch gültigen und verifizierbaren Dafny-Code zu generieren, wodurch proprietäre Modelle übertroffen werden. RL mit Regularisierung verbessert die Leistung weiter und erreicht eine stärkere Generalisierung auf Aufgaben außerhalb des Trainingsbereichs, wobei alle starken Baseline-Modelle auf dem anspruchsvollen DafnyComp-Benchmark übertroffen werden.

English

Existing informal language-based (e.g., human language) Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes, which provide crucial training signals, are neither reliable nor scalable. In fact, the prevalent large proprietary models could hardly generate verifiable programs. A promising yet largely uncharted alternative is formal language-based reasoning. Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes. This capability is pivotal for achieving large-scale, reliable formal software verification. It is a common practice to employ human-annotated chain-of-thought and other human priors to induce the reasoning and coding capabilities of LLMs. Unfortunately, it becomes unacceptably all-consuming to provide such priors for supervising complex programming tasks. In this work, we systematically explore ways to reduce human priors with the formal language, Dafny, as the main environment for our pilot study. Our pipeline mainly relies on introducing an automatic and scalable data curation pipeline, and careful RL designs integrated with feedback from the formal language verifier. We introduce DafnyComp, a benchmark of compositional formal programs with auto-formalized specifications for specification reasoning. Our supervised fine-tuning (SFT) stage enables even small models (e.g., 0.5B) to generate syntactically valid and verifiable Dafny code, surpassing proprietary models. RL with regularization further improves performance, achieving stronger generalization to out-of-domain tasks and outperforming all strong baselines on the challenging DafnyComp benchmark.

Re:Form – Reduzierung menschlicher Vorannahmen in der skalierbaren formalen Softwareverifikation mit RL in LLMs: Eine Vorstudie zu Dafny

Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

papers.abstract

Support