강화학습 (RL) 및 재귀적 추론 (Recursive Inference)을 통한 형식 검증 (Formal Verification) 자동화

증명 보조 도구 (Proof assistants) 및 검증 인식 언어 (Verification-aware languages)를 위한 데이터가 부족하고, 정확성이 그럴듯한 코드를 생성하는 것이 아니라 정밀한 기계 검증 가능 사양 (Machine-checkable specifications)을 충족하는 데 달려 있기 때문에, 대규모 언어 모델 (LLM)에게 자동화된 형식 검증 (Formal verification)은 여전히 어려운 과제로 남아 있습니다. 본 논문은 검증 가능한 보상 (Verifiable rewards)을 통한 강화학습 (RLVR) 및 검증기 유도 추론 시점 탐색 (Verifier-guided inference-time search)을 통해 검증기 환경이 검증된 프로그램 및 증명의 LLM 생성을 어떻게 개선할 수 있는지 연구합니다. 첫째, 우리는 Group Relative Policy Optimization (GRPO) 및 관련 변형들을 사용하여 Dafny에서 RLVR로 오픈 소스 모델을 학습시키며, 생성된 후보들을 완전한 프로그램으로 조립하고 컴파일러 및 검증기 결과로 점수를 매깁니다. APPS에서 파생된 Dafny 데이터셋에 대한 초기 실험 결과, 검증된 보상 (Verified reward)이 2.2%에서 58.1%로 증가했으나, 모델이 의도된 솔루션을 구현하는 대신 취약한 형식 사양을 악용하는 사양 해킹 (Specification hacking) 현상이 나타났습니다. 사양이 불충분하거나 취약한 태스크를 필터링한 후, 정제된 벤치마크에서 다회차 (Multi-turn) RLVR을 수행한 결과 검증 통과율 (Verified pass rate)이 9.7%에서 31.1%로 향상되었습니다. 둘째, 우리는 증명 생성을 분해된 하위 목표 (Subgoals), 검증기 피드백, 진단 및 수리에 대한 구조화된 탐색으로 취급하는 Lean 기반의 검증기 유도 추론 스캐폴드 (Verifier-guided inference scaffold)를 개발합니다. 고정된 베이스 모델을 사용할 때, 증명 수정기 (Proof reviser)를 포함한 전체 스캐폴드는 초기 VeriCoding 파일럿 세트에서의 통과율을 직접 수리 (Direct repair) 방식의 46.2%에서 69.2%로 개선했습니다. 더 큰 규모의 VERINA 데이터셋에서는 전체 태스크 분해와 증명 수정기를 결합하여 이전에 해결되지 않았던 42개의 태스크 중 7개를 해결했습니다. 또한 우리는 Rust $\texttt{curve25519-dalek}$ 검증 프로젝트에서 파생된 저장소 규모의 Lean 벤치마크인 Dalek-Bench를 소개합니다. 예비 결과는 아직 미약하며, 이는 더 강력한 진전 평가 및 태스크별 도구 사용 정책 (Task-specific tool-use policies)이 여전히 필요함을 시사합니다.