기술 요약: Lean을 통한 프로세스 검증 강화 학습 (Process-Verified Reinforcement Learning)

문제 정의

자동 정리 증명(Automated Theorem Proving, ATP)은 수학적 정리에 대한 형식적 증명을 생성하는 것을 목표로 합니다. 대규모 언어 모델(LLM)이 추론 작업에서 진보를 이루었으나, 이들은 일반적으로 강화 학습(RL) 과정에서 자연어(NL) 또는 이진 결과 보상(정답/오답)에 의존합니다. 이는 다음과 같은 격차를 발생시킵니다:

1. 희소한 피드백(Sparse Feedback): 표준 RL 접근 방식은 종종 최종적인 이진 신호(증명 통과/실패)만을 사용하므로, 크레딧 할당(credit assignment)이 희소하며 긴 추론 체인을 가이드하는 데 어려움을 겪습니다.
2. 비구조적 vs 구조적(Unstructured vs. Structured): 유형 이론적(type-theoretic)으로 모든 추론 단계를 미세하게 검증하는 심볼릭 증명 보조 도구(예: Lean, Coq, Isabelle)와 달리, LLM은 스칼라 보상을 가진 토큰 시퀀스에 대해 훈련됩니다.
3. 프로세스 보상 모델(Process Reward Models, PRMs): 최근 연구들은 단계별 보상을 제공하기 위해 PRM을 사용하지만, 이는 대규모 주석 데이터셋을 필요로 하거나 자연어 기반의 CoT 감독에 의 Rely하는 경우가 많아, 심볼릭 검증의 엄격한 건전성(soundness)이 부족합니다.

핵심적으로 해결하고자 하는 과제는 외부의 노이즈 섞인 PRM이나 인간의 주석에 의존하지 않고, 어떻게 심볼릭 증명 보조 도구(Lean)의 풍부하고 구조화된 피드백을 LLM 훈련에 활용할 것인가 하는 점입니다.

방법론

본 논문은 Lean의 심볼릭 피드백을 그룹 상대 정책 최적화(Group Relative Policy Optimization, GRPO) 목적 함수에 직접 통합하는 프로세스 검증 강화 학습(Process-Verified Reinforcement Learning) 프레임워크를 제안합니다. 이 방법은 세 가지 주요 구성 요소로 이루어집니다.

1. 심볼릭 프로세스 오라클 (Symbolic Process Oracle)

저자들은 Lean을 단순히 최종 검증기로 취급하는 대신, 훈련 중에 프로세스 오라클로서 활용합니다.

• 파싱(Parsing): 생성된 증명은 추상 구문 트리(AST)를 기반으로 일련의 택틱(tactics, $T_1, \dots, T_N$)으로 파싱됩니다.
• 검증(Verification): Lean의 정교화(elaboration) 과정은 두 가지 유형의 신호를 제공합니다:
  • 결과 신호(Outcome Signal): 전체 증명의 유효성을 나타내는 전역 이진 점수 $g(Y) \in \{0, 1\}$.
  • 프로세스 신호(Process Signal): 각 택틱에 대한 미세한 피드백으로, 국소적으로 타당한 단계와 첫 번째 오류가 발생한 특정 위치를 식별합니다.

2. 크레딧 할당 전략 (Credit Assignment Strategy)

심볼릭 피드백과 토큰 수준 RL 사이의 간극을 메우기 위해 저자들은 특정 할당 규칙을 도입합니다.

• 첫 번째 오류 전파(First-Error Propagation): 만약 택틱 $T_j$가 실패하면, 이후의 모든 택틱($k \ge j$인 $T_k$)은 오류가 있는 것으로 간주합니다. 이는 증명의 인과적 성질을 반영합니다: 유효하지 않은 접두사는 이후의 모든 추론 체인을 무효화합니다.
• 택틱 수준 점수($\phi$):
  • 증명이 통과되면($g(Y)=1$), 모든 택틱은 양수 점수(1)를 받습니다.
  • 증명이 실패하면($g(Y)=0$):
    • 첫 번째 오류 이전의 택틱들은 부분 점수($d_1$)를 받습니다.
    • 첫 번째 오류가 발생한 택틱과 그 이후의 모든 택틱은 페널티 점수($d_2$)를 받습니다.
• 토큰 수준 매핑(Token-Level Mapping): 택틱 수준의 어드밴티지(advantage)는 각 택틱의 첫 번째 토큰(예: 키워드 intro, apply)에만 할당됩니다. 이는 증명 전략이 결정되는 의미론적 결정 지점과 일치합니다.

3. RL 목적 함수 (GRPO 통합)

이 프레임워크는 결과 어드밴티지와 프로세스 어드밴티지를 단일 GRPO 목적 함수로 결합합니다:

• 결과 어드밴티지($A_{outcome}$): 그룹 평균에 대한 전역 통과/실패 상태를 기준으로 계산됩니다.
• 프로세스 어드밴티지($A_{process}$): 문제의 난이도를 고려하기 위해 그룹의 평균 결과 보상으로 정규화된 택틱 수준 점수를 기반으로 계산됩니다.
• 결합된 어드밴티지(Combined Advantage): 응답 $i$ 내의 택틱 $j$의 첫 번째 토큰인 토큰 $t$에 대하여:
  $$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$$
  비(非) 첫 번째 토큰의 경우, 결과 어드밴티지만 적용됩니다. 이 공식은 별도의 가치 모델(value model)이나 보조 PRM 없이도 검증기의 그라운드 트루스(ground truth)에만 의존하도록 설계되었습니다.

주요 기여

1. 심볼릭 피드백의 공식화: 저자들은 Lean의 택틱 수준 피드백을 스칼라 훈련 신호로 공식화하여, 자연어 가이드 없이도 미세한 토큰 수준의 크레딧 할당을 가능하게 했습니다.
2. 심볼릭 검증기 가이드 RL: 결과 및 택틱 수준 보상을 모두 Lean에서 직접 도출하여 RL 프레임워크에 통합함으로써, 조밀하고 검증 가능한 크레딧 할당을 제공합니다.
3. 안정적인 벤치마크 성능 향상: 이 접근 방식은 MiniF2F 및 ProofNet 벤치마크에서 일관된 성능 향상을 보여주며, 외부 PRM이나 NL 표기법 없이도 결과 전용(outcome-only) RL 및 바닐라 베이스라인을 능가합니다.

실험 결과

실험은 STP-Lean 및 DeepSeek-Prover-V1.5 (7B 모델)를 사용하여 MiniF2F-Test 및 ProofNet-Test 벤치마크에서 수행되었습니다.

• 성능 향상:
  • STP-Lean: 제안된 방법은 MiniF2F pass@64를 +2.5% (56.7%에서 59.2%로), ProofNet pass@32를 +1.4% 개선했습니다.
  • DeepSeek-Prover-V1.5: 모든 설정에서 일관되지만 미미한 수준의 개선이 관찰되었습니다.
• 베이스라인과의 비교:
  • 본 방법은 불안정성을 보이고 일부 구성에서 ProofNet 성능 개선에 실패한 "Outcome-only" GRPO보다 우수한 성능을 보였습니다.
  • 거대한 추론 시간 탐색 예산 없이도 단일 샷 생성(single-shot generation) 방식을 통해 강력한 트리 탐색 베이스라인들(예: InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS)과 경쟁력 있는 결과를 달성했습니다.
• 절제 연구(Ablation Studies):
  • 토큰 할당: 크레딧을 택틱의 첫 번째 토큰에 할당하는 것이 모든 토큰에 분배하거나 마지막 토큰에 할당하는 것보다 가장 안정적인 결과를 냈습니다.
  • 첫 번째 오류 전파: 이 규칙을 제거하면 성능이 크게 저하되었으며, 이는 오류 이후의 단계들을 무효한 것으로 처리해야 함을 확인시켜 줍니다.
  • 타임아웃: 15초의 검증 타임아웃이 복잡한 증명을 버리지 않으면서도 간결한 증명을 유도하는 최적의 균형을 제공했습니다.

의의 및 주장

본 논문은 심볼릭 증명 보조 도구가 단순한 평가 도구가 아니라, 훈련 중 능동적인 프로세스 수준의 보상 오라클로 간주되어야 한다고 주장합니다. 형식적 추론 시스템에 내재된 "풍부하고 미세한 구조적 피드백"을 활용함으로써, 저자들은 LLM의 확장성과 심볼릭 검증의 신뢰성을 결합하는 RL 프레임워크의 경로를 제시합니다.

연구의 핵심 요점은 다음과 같습니다:

• 조밀하고 검증 가능한 신호: 증명기의 자체 오류 로그와 정교화 트리를 사용하면, 희소한 이진 결과나 학습된 PRM보다 우수한, 건전하고 조밀한 보상 신호를 제공할 수 있습니다.
• 안정성: 전역 결과 보상과 로컬 택틱 보상의 결 조합은 택틱 전용 훈련에서 나타나는 조기 수렴 문제와 결과 전용 훈련의 희소성 문제를 방지하여 훈련을 안정화합니다.
• 효율성: 이 접근 방식은 트리 탐색의 계산 오버헤드나 별도의 PRM 훈련을 위한 데이터 요구 사항 없이도 최첨단 혹은 경쟁력 있는 성능을 달ace합니다.

저자들은 학습된 어드밴티지 추정기 대신 고정된 보상 점수($d_1, d_2$)에 의존한다는 점과, 현재는 CoT가 없는 순수 Lean 증명에 집중하고 있어 긴 형태의 자연어 추론을 위한 보상 설계의 과제가 남아 있다는 점을 언급하며 한계점에 대해 겸허한 태도를 유지하고 있습니다.