Re:Form -- Réduction des préjugés humains dans la vérification formelle logicielle évolutive avec l'apprentissage par renforcement dans les LLM : Une étude préliminaire sur Dafny

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

July 22, 2025

papers.authors: 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

papers.abstract

Les grands modèles de langage (LLMs) existants basés sur le langage informel (par exemple, le langage humain) et entraînés par apprentissage par renforcement (RL) font face à un défi majeur : leurs processus de vérification, qui fournissent des signaux d’entraînement cruciaux, ne sont ni fiables ni évolutifs. En effet, les grands modèles propriétaires prédominants peinent à générer des programmes vérifiables. Une alternative prometteuse mais encore largement inexplorée est le raisonnement basé sur le langage formel. Ancrer les LLMs dans des systèmes formels rigoureux, où les modèles génératifs opèrent dans des espaces de langage formel (par exemple, Dafny), permet la vérification automatique et mathématiquement prouvable de leurs processus de raisonnement et de leurs résultats. Cette capacité est essentielle pour réaliser une vérification formelle de logiciels à grande échelle et fiable. Il est courant d’utiliser des chaînes de pensée annotées par des humains et d’autres connaissances a priori humaines pour induire les capacités de raisonnement et de codage des LLMs. Malheureusement, fournir de telles connaissances a priori pour superviser des tâches de programmation complexes devient inacceptablement chronophage. Dans ce travail, nous explorons systématiquement des moyens de réduire les connaissances a priori humaines en utilisant le langage formel Dafny comme environnement principal pour notre étude pilote. Notre pipeline repose principalement sur l’introduction d’un processus de curation de données automatique et évolutif, ainsi que sur des conceptions soignées de RL intégrant les retours du vérificateur de langage formel. Nous présentons DafnyComp, un benchmark de programmes formels compositionnels avec des spécifications auto-formalisées pour le raisonnement sur les spécifications. Notre étape de fine-tuning supervisé (SFT) permet même à de petits modèles (par exemple, 0,5 milliard de paramètres) de générer du code Dafny syntaxiquement valide et vérifiable, surpassant les modèles propriétaires. Le RL avec régularisation améliore encore les performances, obtenant une meilleure généralisation pour les tâches hors domaine et surpassant toutes les bases de référence solides sur le benchmark difficile de 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.