Re:Form -- Riduzione dei Pregiudizi Umani nella Verifica Formale Scalabile del Software con RL nei Modelli Linguistici: Uno Studio Preliminare su Dafny

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

July 22, 2025

Autori: 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

Abstract

I modelli linguistici su larga scala (LLM) esistenti basati su linguaggio informale (ad esempio, linguaggio umano) addestrati con apprendimento per rinforzo (RL) affrontano una sfida significativa: i loro processi di verifica, che forniscono segnali di addestramento cruciali, non sono né affidabili né scalabili. In effetti, i modelli proprietari di grandi dimensioni prevalenti difficilmente riescono a generare programmi verificabili. Un'alternativa promettente ma ancora largamente inesplorata è il ragionamento basato su linguaggio formale. Ancorare gli LLM a sistemi formali rigorosi, in cui i modelli generativi operano in spazi di linguaggio formale (ad esempio, Dafny), consente la verifica automatica e matematicamente dimostrabile dei loro processi e risultati di ragionamento. Questa capacità è fondamentale per ottenere una verifica formale del software su larga scala e affidabile. È pratica comune impiegare catene di pensiero annotate da esseri umani e altri precedenti umani per indurre le capacità di ragionamento e codifica degli LLM. Sfortunatamente, diventa inaccettabilmente dispendioso fornire tali precedenti per supervisionare compiti di programmazione complessi. In questo lavoro, esploriamo sistematicamente modi per ridurre i precedenti umani utilizzando il linguaggio formale Dafny come ambiente principale per il nostro studio pilota. La nostra pipeline si basa principalmente sull'introduzione di una pipeline di curatela dei dati automatica e scalabile, e su attenti progetti di RL integrati con feedback dal verificatore di linguaggio formale. Introduciamo DafnyComp, un benchmark di programmi formali compositivi con specifiche auto-formalizzate per il ragionamento sulle specifiche. La nostra fase di fine-tuning supervisionato (SFT) consente anche a modelli di piccole dimensioni (ad esempio, 0.5B) di generare codice Dafny sintatticamente valido e verificabile, superando i modelli proprietari. L'RL con regolarizzazione migliora ulteriormente le prestazioni, ottenendo una generalizzazione più forte per compiti fuori dominio e superando tutte le baseline forti sul benchmark impegnativo di 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.