Lean을 통한 정리 증명을 위한 프로세스 검증 강화학습 (Process-Verified Reinforcement Learning)

검증 가능한 보상으로부터의 강화학습 (RLVR)은 일반적으로 단일 이진 검증 신호에 의존해 왔으나, 형식적 추론 (formal reasoning) 분야의 심볼릭 증명 보조 도구 (symbolic proof assistants)는 풍부하고 세밀한 구조적 피드백을 제공합니다. 이러한 구조화된 프로세스와 비구조화된 보상 사이의 간극은 밀도가 높으면서도 건전한 (sound) 피드백의 중요성을 강조합니다. 본 연구에서 우리는 Lean 증명 보조 도구 자체가 심볼릭 프로세스 오라클 (symbolic process oracle) 역할을 할 수 있음을 입증하며, 학습 과정 동안 결과 수준 (outcome-level) 및 세밀한 택틱 수준 (tactic-level)의 검증된 피드백을 모두 제공합니다. 증명 시도는 택틱 시퀀스 (tactic sequences)로 파싱되며, Lean의 정교화 (elaboration) 과정은 국소적으로 건전한 단계와 가장 처음 실패한 단계를 모두 표시하여, 유형 이론 (type theory)에 기반한 밀도 높고 검증기 기반인 크레딧 신호 (credit signals)를 생성합니다. 우리는 이러한 구조화된 보상을 첫 번째 오류 전파 (first-error propagation) 및 첫 번째 토큰 크레딧 (first-token credit) 방법과 함께 GRPO 스타일의 강화학습 목적 함수에 통합하여, 결과 수준과 프로세스 수준의 장점 사이의 균형을 맞춥니다. STP-Lean 및 DeepSeek-Prover-V1.5를 이용한 실험 결과, 택틱 수준의 감독이 대부분의 설정에서 결과 전용 베이스라인 (outcome-only baselines)보다 성능이 뛰어남을 보여주었으며, MiniF2F 및 ProofNet과 같은 벤치마크에서 성능 향상을 달성했습니다. 실증적인 이득을 넘어, 본 연구는 더 넓은 관점을 제시합니다. 즉, 심볼릭 증명 보조 도구는 평가 시점의 검증기일 뿐만 아니라, 학습 중에는 프로세스 수준의 보상 오라클 (reward oracles)로도 작용할 수 있습니다. 이는 언어 모델의 확장성과 형식적 추론을 위한 심볼릭 검증의 신뢰성을 결합한 강화학습 프레임워크를 향한 길을 열어줍니다.