Re:Form -- LLMs에서 RL을 활용한 확장 가능한 공식 소프트웨어 검증에서 인간 사전 지식 줄이기: Dafny에 대한 사전 연구

기존의 비공식적인 언어 기반(예: 인간 언어) 대규모 언어 모델(Large Language Models, LLMs)은 강화학습(Reinforcement Learning, RL)을 통해 훈련받을 때 중요한 훈련 신호를 제공하는 검증 과정이 신뢰성과 확장성 측면에서 큰 한계를 보인다. 실제로 현재 널리 사용되는 대규모 전용 모델들은 거의 검증 가능한 프로그램을 생성할 수 없다. 그러나 공식적인 언어 기반의 추론 방식은 희망을 주는 대안이지만 여전히 탐색이 부족한 분야이다. 엄격한 공식 시스템에 기반한 LLMs는 공식 언어 공간(예: Dafny)에서 생성 모델이 작동하도록 하여, 그 추론 과정과 결과를 자동적으로 수학적으로 증명 가능한 방식으로 검증할 수 있다. 이 능력은 대규모이고 신뢰할 수 있는 소프트웨어 공식 검증을 달성하는 데 필수적이다. 일반적으로 LLM의 추론 및 코딩 능력을 유도하기 위해 인간의 주석이 달린 사고 과정(chain-of-thought)과 기타 인간의 사전 지식(priors)을 사용하는 것이 일반적이다. 그러나 복잡한 프로그래밍 작업을 감독하기 위해 이러한 사전 지식을 제공하는 것은 수용 불가능할 정도로 시간과 자원을 과도하게 소모하게 된다. 본 연구에서는 공식 언어인 Dafny를 주요 실험 환경으로 삼아 인간 사전 지식을 줄이는 방법을 체계적으로 탐구한다. 우리의 파이프라인은 주로 자동적이고 확장 가능한 데이터 정제(data curation) 파이프라인을 도입하고, 공식 언어 검증기(formal language verifier)의 피드백을 통합한 주의 깊은 강화학습(RL) 설계에 의존한다. 우리는 사고 과정 추론을 위한 자동 공식화된 명세를 갖춘 조합형 공식 프로그램의 벤치마크인 DafnyComp을 도입한다. 우리의 감독적 미세 조정(supervised fine-tuning, SFT) 단계는 작은 모델(예: 0.5B)도 문법적으로 올바르고 검증 가능한 Dafny 코드를 생성할 수 있도록 하여, 전용 모델들을 능가한다. 정규화(regularization)를 적용한 강화학습은 성능을 더욱 향상시키며, 영역 외부(out-of-domain) 작업에 대한 더 강한 일반화 능력을 보여주고, 어려운 DafnyComp 벤치마크에서 모든 강력한 기준 모델보다 우수한 성능을 달성한다.