Re:Form -- 확장 가능한 형식 소프트웨어 검증에서 인간의 사전 지식을 줄이는 RL과 LLM의 활용: Dafny에 대한 예비 연구

초록

기존의 비공식 언어 기반(예: 인간 언어) 대형 언어 모델(LLMs)은 강화 학습(Reinforcement Learning, RL)을 통해 훈련되지만, 중요한 훈련 신호를 제공하는 검증 과정이 신뢰할 수 없고 확장 가능하지 않다는 중대한 문제에 직면해 있습니다. 실제로, 널리 사용되는 대형 독점 모델들은 검증 가능한 프로그램을 생성하기 어려운 상황입니다. 이에 대한 유망하면서도 아직 많이 탐구되지 않은 대안은 형식 언어 기반 추론입니다. 형식적 시스템에 기반을 둔 LLMs는 형식 언어 공간(예: Dafny)에서 생성 모델이 작동하도록 함으로써, 그들의 추론 과정과 결과를 자동적이고 수학적으로 검증 가능하게 만듭니다. 이 능력은 대규모의 신뢰할 수 있는 형식적 소프트웨어 검증을 달성하는 데 핵심적입니다. 일반적으로 인간이 주석을 단 사고의 연쇄(chain-of-thought) 및 기타 인간의 사전 지식을 활용하여 LLMs의 추론 및 코딩 능력을 유도합니다. 그러나 복잡한 프로그래밍 작업을 감독하기 위해 이러한 사전 지식을 제공하는 것은 현실적으로 감당하기 어려울 정도로 많은 비용을 요구합니다. 본 연구에서는 형식 언어인 Dafny를 주요 환경으로 삼아 인간의 사전 지식을 줄이는 방법을 체계적으로 탐구합니다. 우리의 파이프라인은 주로 자동적이고 확장 가능한 데이터 큐레이션 파이프라인을 도입하고, 형식 언어 검증기의 피드백과 통합된 신중한 RL 설계에 의존합니다. 우리는 사양 추론을 위한 자동 형식화된 사양을 포함한 구성적 형식 프로그램 벤치마크인 DafnyComp를 소개합니다. 우리의 지도 미세 조정(Supervised Fine-Tuning, SFT) 단계는 작은 모델(예: 0.5B)조차도 구문적으로 유효하고 검증 가능한 Dafny 코드를 생성할 수 있게 하여 독점 모델들을 능가합니다. 정규화를 적용한 RL은 성능을 더욱 개선하여 도메인 외 작업에 대한 더 강력한 일반화를 달성하고, 도전적인 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.

Re:Form -- 확장 가능한 형식 소프트웨어 검증에서 인간의 사전 지식을 줄이는 RL과 LLM의 활용: Dafny에 대한 예비 연구

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

초록

Support