Re:Form -- Reducción de sesgos humanos en la verificación formal escalable de software con aprendizaje por refuerzo en modelos de lenguaje grandes: Un estudio 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

Resumen

Los modelos de lenguaje de gran escala (LLMs, por sus siglas en inglés) basados en lenguaje informal (por ejemplo, lenguaje humano) entrenados con Aprendizaje por Refuerzo (RL, por sus siglas en inglés) enfrentan un desafío significativo: sus procesos de verificación, que proporcionan señales de entrenamiento cruciales, no son ni confiables ni escalables. De hecho, los modelos propietarios de gran escala predominantes difícilmente podrían generar programas verificables. Una alternativa prometedora pero en gran parte inexplorada es el razonamiento basado en lenguajes formales. Fundamentar los LLMs en sistemas formales rigurosos, donde los modelos generativos operan en espacios de lenguaje formal (por ejemplo, Dafny), permite la verificación automática y matemáticamente demostrable de sus procesos de razonamiento y resultados. Esta capacidad es fundamental para lograr una verificación formal de software confiable a gran escala. Es una práctica común emplear cadenas de pensamiento anotadas por humanos y otros conocimientos previos humanos para inducir las capacidades de razonamiento y codificación de los LLMs. Desafortunadamente, resulta excesivamente consumidor proporcionar tales conocimientos previos para supervisar tareas de programación complejas. En este trabajo, exploramos sistemáticamente formas de reducir los conocimientos previos humanos utilizando el lenguaje formal Dafny como el entorno principal para nuestro estudio piloto. Nuestra canalización se basa principalmente en la introducción de una canalización de curación de datos automática y escalable, y diseños cuidadosos de RL integrados con retroalimentación del verificador de lenguaje formal. Presentamos DafnyComp, un punto de referencia de programas formales composicionales con especificaciones auto-formalizadas para el razonamiento de especificaciones. Nuestra etapa de ajuste fino supervisado (SFT, por sus siglas en inglés) permite que incluso modelos pequeños (por ejemplo, 0.5B) generen código Dafny sintácticamente válido y verificable, superando a los modelos propietarios. El RL con regularización mejora aún más el rendimiento, logrando una mayor generalización para tareas fuera del dominio y superando a todos los puntos de referencia fuertes en el desafiante punto de referencia 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.