Verifier-Grounded Agentic RL for Provably Correct Code

이 논문은 강화학습용 보상을 검증기의 합격 여부 대신 진단 정보에서 만들어, 모든 입력에 대해 증명되는 코드를 학습시키는 문제를 풀었다.

이 논문은 한마디로 정형 검증기의 진단 메시지를 밀도 있는 보상으로 바꿔 코드 모델을 학습시키는 방법이다. 저자들은 증명 항목 해결 비율에 보상을 주고 명세를 몰래 바꾸는 행동을 무결성 심사로 걸러냈다. 그 결과 코드 생성 검증 통과율이 DafnyBench에서 66.1%에서 93.5%로, SWE-Proof에서 56.3%에서 100%로 올랐다.

핵심 요약

• 연구진은 검증기의 합격·불합격 판정 대신 진단 정보를 읽어, 인스턴스가 요구하는 증명 항목 가운데 얼마나 해결했는지 비율로 점수를 주는 보상을 만들었다.
• 무결성 심사를 검증기보다 우선하여, 명세를 몰래 약화하거나 증명할 내용을 가정으로 대신한 제출을 걸러낸다.
• Qwen3 모델(1.7B부터 14B까지)과 35B 혼합 전문가 모델을 학습한 결과, 코드 생성의 검증 통과율이 DafnyBench에서 66.1%에서 93.5%로, SWE-Proof에서 56.3%에서 100%로 올랐다.
• 같은 설정의 합격·불합격 이진 보상은 코드 생성에서 71.0%에 그쳤고, 증명 전문가 모델을 고정 협력자로 넣으면 DafnyBench에서 4.8점이 더 올랐다.
• 저장소 패치까지 제출해야 하는 과제에서 각 프로젝트의 숨겨진 테스트를 통과한 문제 해결 비율이 59.6%에서 72.5%로 올랐다.
• 학습에 쓰지 않은 세 검증 벤치마크에서도 성적이 올라, 학습에 없는 Rust 언어와 Verus 검증기 환경에서도 실력이 옮겨 갔다.

논문 링크

외부 연구를 정리한 자료입니다. HDATF가 발표한 논문이나 제품 성능을 측정한 결과는 아닙니다.