Re:Form -- Reduzindo Prioridades Humanas na Verificação Formal Escalável de Software com RL em LLMs: Um Estudo Preliminar sobre Dafny

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

July 22, 2025

Autores: Chuanhao Yan, Fengdi Che, Xuhan Huang, Xu Xu, Xin Li, Yizhi Li, Xingwei Qu, Jingzhe Shi, Zhuangzhuang He, Chenghua Lin, Yaodong Yang, Binhang Yuan, Hang Zhao, Yu Qiao, Bowen Zhou, Jie Fu

cs.AI

Resumo

Os modelos de linguagem de grande escala (LLMs) baseados em linguagem informal (por exemplo, linguagem humana) treinados com Aprendizado por Reforço (RL) enfrentam um desafio significativo: seus processos de verificação, que fornecem sinais de treinamento cruciais, não são confiáveis nem escaláveis. Na verdade, os grandes modelos proprietários predominantes dificilmente conseguem gerar programas verificáveis. Uma alternativa promissora, mas ainda pouco explorada, é o raciocínio baseado em linguagem formal. Ancorar LLMs em sistemas formais rigorosos, onde modelos generativos operam em espaços de linguagem formal (por exemplo, Dafny), permite a verificação automática e matematicamente comprovável de seus processos e resultados de raciocínio. Essa capacidade é fundamental para alcançar a verificação formal de software em grande escala e confiável. É uma prática comum empregar cadeias de pensamento anotadas por humanos e outros conhecimentos prévios humanos para induzir as capacidades de raciocínio e codificação dos LLMs. Infelizmente, torna-se inaceitavelmente exaustivo fornecer tais conhecimentos prévios para supervisionar tarefas complexas de programação. Neste trabalho, exploramos sistematicamente maneiras de reduzir os conhecimentos prévios humanos utilizando a linguagem formal Dafny como o ambiente principal para nosso estudo piloto. Nossa abordagem depende principalmente da introdução de um pipeline de curadoria de dados automático e escalável, e de projetos cuidadosos de RL integrados com feedback do verificador de linguagem formal. Introduzimos o DafnyComp, um benchmark de programas formais composicionais com especificações auto-formalizadas para raciocínio sobre especificações. Nossa etapa de ajuste fino supervisionado (SFT) permite que até mesmo modelos pequenos (por exemplo, 0.5B) gerem código Dafny sintaticamente válido e verificável, superando modelos proprietários. O RL com regularização melhora ainda mais o desempenho, alcançando uma generalização mais forte para tarefas fora do domínio e superando todas as linhas de base fortes no desafiador benchmark DafnyComp.

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.