기술 요약: OProver: 에이전트 형식 정리 증명용 통합 프레임워크

문제 제기

Lean 4 생태계 내에서 형식 정리 증명 분야의 최근 발전은 대규모 증명 생성과 검증자 인식 훈련을 활용하여 MiniF2F 및 PutnamBench 와 같은 벤치마크의 성능을 향상시켰습니다. 그러나 중요한 한계가 존재합니다: 에이전트 증명 능력(검색, 컴파일러 피드백, 반복적 수정)은 일반적으로 고정된 증명기에 적용되는 추론 시 휴리스틱으로 취급될 뿐, 훈련 과정에 통합된 학습된 정책으로 다루어지지 않습니다.

이는 훈련 - 추론 불일치를 초래합니다. 주로 최종 성공적인 증명에 기반하여 훈련된 모델들은 배포 시에만 컴파일러 피드백과 검색된 컨텍스트를 접하게 되며, 이는 모델이 최적화되지 않은 분포입니다. furthermore, 기존 형식 말뭉치는 최종 산물(명제와 검증된 증명) 에만 초점을 맞추어, 증명 수정 방법을 학습하는 데 필수적인 다중 라운드 상호작용 기록(실패 시도, 검색된 컨텍스트, 컴파일러 진단 정보) 을 생략합니다. 결과적으로 실제 증명 수정을 주도하는 감독 신호는 모델 훈련에서 대부분 활용되지 않고 있습니다.

방법론

본 논문은 검색, 컴파일러 피드백, 반복적 수정을 증명기의 정책에 직접 통합하는 OProver라는 통합 프레임워크를 제시하며, 이는 공진화 훈련 파이프라인을 통해 구현됩니다.

1. OProver 프레임워크

OProver 는 정리 증명을 유계 다중 라운드 정제 루프로 간주합니다. 각 라운드 $t$에서 정책 $\pi$는 압축된 상태 $X_t = (s, R_t, p_{t-1}, f_{t-1})$에 조건부로 작동하며, 여기서:

• $s$: 대상 정리 명제.
• $R_t$: 메모리 $M$에서 검색된 상위 $k$개의 컴파일러 검증 증명.
• $p_{t-1}$: 이전 증명 시도.
• $f_{t-1}$: Lean 4 검증자로부터의 원본 텍스트 컴파일러 피드백(진단 정보).

정책은 수정된 시도 $p_t$를 생성합니다. 검증이 실패하면 원본 피드백이 다음 라운드를 위해 정책으로 다시 전달됩니다. 핵심적으로, 정책은 가장 최근의 시도와 피드백에만 조건부로 작동하여 국소적 수정 신호를 유지하면서도 상태를 압축적으로 유지합니다.

2. OProofs: 통합 훈련 말뭉치

이 프레임워크를 지원하기 위해 저자들은 에이전트 증명을 위해 특별히 설계된 대규모 말뭉치인 OProofs를 구축했습니다. 최종 증명만 보존하는 이전 데이터셋과 달리, OProofs 는 직렬화된 궤적을 기록하며 다음을 포함합니다:

• 검색된 컨텍스트.
• 실패한 시도.
• 원본 컴파일러 피드백.
• 후속 수정.

OProofs 는 세 가지 소스에서 구축되었습니다: 공개 Lean 리소스, 대규모 증명 합성(자동 형식화 + 검증), 그리고 OProver 의 자체 에이전트 증명에서 얻은 추적 데이터입니다. 이는 177 만 개의 고유한 Lean 명제와 686 만 개의 컴파일러 검증 증명, 그리고 107 만 개의 에이전트 궤적으로 구성되어 있습니다.

3. 공진화 훈련 파이프라인

훈련 과정은 증명기와 말뭉치가 공진화하는 반복 루프(알고리즘 1) 를 따릅니다:

1. 지속적 사전 훈련 (CPT): Lean 코드, 수학, 긴 컨텍스트 추론 데이터의 혼합으로 베이스 모델을 훈련하여 OProver-Base를 생성합니다.
2. 반복적 사후 훈련:
   • 에이전트 롤아웃: 현재 정책이 메모리 $M_k$에서 검색하고 Lean 컴파일러로 검증하여 정리 풀에서 다중 라운드 증명을 수행합니다.
   • 데이터 수집: 새로 검증된 증명은 말뭉치에 추가되고 검색 메모리에 인덱싱됩니다. 실패한 시도와 성공적인 수정은 라운드 단위 예제 $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$로 분해됩니다.
   • 지도 미세 조정 (SFT): 수집된 수정 예제를 사용하여 모델을 업데이트합니다.
   • 강화 학습 (RL): Group Sequence Policy Optimization(GSPO) 을 해결되지 않은 어려운 사례에 적용하며, 검증 성공과 형식 정확도에 기반한 보상 신호를 사용합니다.
   • 재순환: 업데이트된 말뭉치와 메모리가 다음 반복으로 피드백되어, 정책이 자신의 개선된 증명에서 학습할 수 있도록 합니다.

주요 기여

1. 에이전트 증명을 위한 통합 프레임워크: OProver 는 검색, 피드백, 반복적 수정을 단일 학습된 정책으로 통합하여, 이러한 신호를 외부 휴리스틱이 아닌 핵심 전략의 일부로 사용하도록 모델을 훈련시킴으로써 훈련 - 추론 불일치를 제거합니다.
2. OProofs 말뭉치: 실패 시도와 원본 컴파일러 피드백을 포함한 다중 턴 상호작용 기록을 명시적으로 보존하는 대규모 말뭉치(177 만 개 명제, 686 만 개 증명) 를 구축하여, 기존 형식 데이터셋에서는 제공되지 않았던 감독 신호를 제공합니다.
3. 공진화 파이프라인: 증명기가 생성한 새로운 데이터(검증된 증명 및 수정 궤적) 가 즉시 훈련 말뭉치와 검색 메모리로 다시 통합되어 자기 개선 루프를 생성하는 훈련 방법론입니다.
4. 최첨단 성능: OProver 는 오픈 가중 전체 증명기 중에서 최상위권 결과를 달성하여, 에이전트 정제 전략이 훨씬 더 큰 모델들보다 우월할 수 있음을 입증했습니다.

실험 결과

OProver 는 MiniF2F, MathOlympiadBench, ProofNet, ProverBench, PutnamBench 등 다섯 가지 Lean 4 벤치마크에서 평가되었습니다.

• 성능: OProver-32B모델은 세 가지 벤치마크(MiniF2F: 93.3%, ProverBench: 58.2%, PutnamBench: 11.3%) 에서 최고의 Pass@32 점수를 달성했고, 나머지 두 가지(MathOlympiad: 22.8%, ProofNet: 33.2%) 에서는 두 번째로 좋은 성적을 거두었습니다.
• 효율성: OProver-32B(320 억 파라미터) 는 훨씬 적은 파라미터를 가졌음에도 대부분의 벤치마크에서 6710 억 DeepSeek-Prover-V2 와 5600 억 LongCat-Flash-Prover(TIR 포함) 를 능가했습니다. 80 억 변형조차 모든 벤치마크에서 320 억 Goedel-Prover-V2 를 능가했습니다.
• 추론 시 확장성: 성능은 계산 예산 증가(더 많은 샘플 또는 정제 라운드) 에 따라 일관되게 향상되었으나, 체감수익은 감소했습니다. 정제 깊이와 샘플링 너비 간의 최적 할당은 벤치마크 난이도에 따라 다양했습니다.
• 절대 실험: 다중 턴 컴파일러 피드백을 제거하면 가장 큰 성능 저하가 발생하여 반복적 정제가 성과 향상의 주된 동력임을 확인시켰습니다. 검색 증강을 제거해도 일관되게 더 작은 폭의 감소가 발생하여 검색 기반의 보완적 가치를 강조했습니다.

중요성과 주장

본 논문은 에이전트 형식 정리 증명이 별도의 추론 시 모듈로 조립되는 것이 아니라 통합된 정책으로 효과적으로 학습될 수 있음을 OProver 가 입증했다고 주장합니다. 증명 구성, 실패, 수정의 전체 궤적에 대해 훈련함으로써 모델은 컴파일러 피드백과 검색된 컨텍스트를 추론 과정의 고유한 부분으로 활용하는 방법을 학습합니다.

저자들은 성능 향상이 단순히 모델 규모 때문이 아니라 검색 증강 기반과 컴파일러 유도 반복 정제 간의 시너지에서 비롯된다고 강조합니다. OProver 정책과 OProofs 말뭉치의 공진화는 시스템이 자신의 성공 및 실패 시도에서 학습하여 증명 능력을 지속적으로 향상시킬 수 있게 하여, 형식 추론 시스템 훈련을 위한 새로운 패러다임을 확립합니다.