기술 요약: FormalRewardBench

문제 제기

최근 신경 정리 증명기 (neural theorem provers) 의 발전은 검증 가능한 보상을 활용한 강화 학습 (RLVR) 에 크게 의존하고 있습니다. 이 패러다임에서 증명 보조 도구 (Lean 4 등) 는 타입 체킹을 기반으로 이진적 정확성 신호 (통과/실패) 를 제공합니다. 이러한 신호는 확장성이 있고 보상 해킹에 면역이지만, 희소한 신용 할당 (sparse credit assignment) 문제를 겪습니다. 즉, 어려운 문제에서 부분적 진전을 보인 모델은 학습 신호를 받지 못합니다. 마지막 단계에서 실패한 증명도 완전히 잘못된 접근법과 동일한 영 (0) 보상을 받기 때문입니다.

이를 완화하기 위해 연구자들은 이진 검증을 넘어 증명 품질을 평가할 수 있는 학습된 보상 모델을 제안해 왔습니다. 그러나 이러한 보상 모델을 비교하는 것은 현재 비용이 많이 드는 강화 학습 (RL) 훈련 제거 실험 (ablations) 을 필요로 하므로 어렵습니다. furthermore, 기존 보상 모델 벤치마크 (RewardBench, ProcessBench 등) 는 비공식적 자연어 추론에 초점을 맞추고 있으며, 공식 정리 증명이 요구하는 구문적 정밀도, 타입 정확성, 그리고 논리적 건전성을 다루지 않습니다. 현재 훈련 실행 없이 공식 증명에서 보상 모델을 직접 평가할 수 있는 벤치마크는 존재하지 않습니다.

방법론

저자들은 Lean 4 에서 공식 정리 증명을 위한 보상 모델을 평가하기 위해 설계된 최초의 벤치마크인 FormalRewardBench를 소개합니다. 이 벤치마크는 각각 공식적으로 검증된 올바른 증명과 잘못된 변형이 포함된 **250 개의 선호도 쌍 (preference pairs)**으로 구성됩니다.

데이터셋 구축

이 데이터셋은 Lean 4 로 공식화된 488 개의 올림피아드 수준 수학 문제 모음인 MiniF2F에서 파생되었습니다. 저자들은 세 가지 기준을 충족하는 잘못된 증명을 생성하기 위해 통제된 오류 주입 파이프라인을 활용합니다:

1. 구문적 유효성: 잘못된 증명은 유효한 Lean 코드로 파싱되어야 합니다.
2. 의미적 그럴듯함: 오류는 정의되지 않은 변수와 같은 사소한 것이 아니라 현실적인 실패 모드를 반영해야 합니다.
3. 현실적인 오류 패턴: 실수는 대형 언어 모델 (LLM) 의 실제 실패를 반영해야 합니다.

오류 주입 전략

오류 변형을 생성하기 위해 다섯 가지 전문가 큐레이션 전략이 사용되며, 최첨단 LLM(Claude Opus 4.5) 에 대한 프롬프트를 통해 구현됩니다:

1. 최소 단일 지점 변형: 올바른 증명을 외과적으로 수정하여 (가설 교체, 단일 변수 또는 보조 정리 이름 변경 등) 구문적 유효성을 유지하면서 의미적 실패를 초래합니다.
2. 자연어 정당화: 결함이 있는 추론을 정당화하는 오해의 소지가 있는 자연어 주석을 잘못된 증명에 추가하여 " verbosity 편향 (verbosity bias)"을 테스트합니다.
3. Python 코드 주입: 공식 Lean 증명 단계를 실행 가능한 Python 코드로 대체하여 계산적으로 문제를 해결할 수는 있지만 공식 증명 요구 사항을 충족하지 못하게 합니다 (작업 준수 테스트).
4. 강제 LLM 실수: 이전 모델 출력에서 확인된 일반적인 공식 오류 (잘못된 전술 적용, 잘못된 가설 선택, 잘못된 보조 정리 인스턴스화 등) 를 포함하는 증명을 생성합니다.
5. 장황한 잘못된 증명: 근본적인 논리적 결함을 위장하는 정교한 구조와 중간 보조 정리로 불필요하게 긴 증명을 생성합니다.

평가 프로토콜

이 벤치마크는 두 가지 설정에서 모델을 평가합니다:

• 점별 (Pointwise): 모델이 각 증명을 독립적으로 점수 매깁니다. 올바른 증명의 점수가 잘못된 것보다 높을 경우 정확도를 측정합니다.
• 쌍별 (Pairwise): 모델이 두 증명을 비교하여 선호도를 출력합니다. 위치 편향을 완화하기 위해 모델이 올바른 순서 (올바른 것 먼저) 와 잘못된 순서 (올바른 것 나중에) 모두에서 일관되게 올바른 증명을 식별할 때만 정확도를 계산합니다.

주요 결과

저자들은 네 가지 범주의 모델을 평가했습니다: 최첨단 LLM, 저자 (Judge) LLM, 범용 LLM, 그리고 정리 증명 전문 모델.

1. 성능 계층 구조: 최첨단 LLM(예: Claude Opus 4.5)이 가장 높은 성능 (쌍별 정확도 59.8%) 을 달성했습니다. 저자 LLM(선호도 데이터로 훈련됨) 은 오픈 가중치 모델 중 전문 정리 증명기보다 훨씬 우수한 성능을 보였습니다 (일부 전문 모델의 12.8% 대비 52.8%).
2. 생성 - 평가 간극: 전문 정리 증명 모델 (예: DeepSeek-Prover-V2-7B, Gödel-Prover-V2-8B) 은 가장 낮은 성능을 보였습니다 (0.0% 에서 24.4% 사이). MiniF2F 에서 최첨단 pass@k 지표를 달성했음에도 불구하고, 이러한 모델들은 증명을 평가하는 데 어려움을 겪습니다. 저자들은 이를 오류 감지에 대한 훈련 부족 때문이라고 분석합니다. 이러한 모델들은 SFT 와 RLVR 을 통해 올바른 증명을 생성하도록 최적화되었지만 오류를 식별하거나 비판하는 방법을 배우지 못했습니다.
3. 오류 난이도 기울기:
   • 가장 쉬움: Python 코드 주입 (S3). 이는 증명 이해가 아닌 언어 식별에 의존하여 탐지합니다.
   • 가장 어려움: 장황한 잘못된 증명 (S5) 과 강제 실수 (S4). 최상의 모델조차 S5 에서 약 60%, S4 에서 약 50% 의 정확도만 달성했습니다.
   • 저자 모델의 한계: 저자 모델은 이분모 양상 (bimodal pattern) 을 보였습니다. Python 주입에서는 거의 완벽한 성능을 보이지만 장황한 증명에서는 거의 0 으로 추락했습니다. 이는 선호도 훈련이 깊은 공식 추론보다는 표면적 차별화를 발달시켰음을 시사합니다.
4. 위치 편향: 모든 카테고리에서 상당한 위치 편향이 관찰되었으며, 특히 전문 증명기 (예: DeepSeek-Prover-V2-7B 는 정확성과 관계없이 첫 번째 증명을 94.9% 의 빈도로 선호) 에서 두드러졌습니다.

중요성과 주장

이 논문은 세 가지 주요 기여를 주장합니다:

1. FormalRewardBench: 비용이 많이 드는 RL 훈련 제거 실험 없이 공식 정리 증명을 위한 보상 모델을 직접 비교할 수 있는 새로운 벤치마크.
2. 방법론: 다른 증명 보조 도구, 데이터 증강, 또는 커리큘럼 설계에 적용 가능한 현실적인 잘못된 공식 증명을 생성하기 위한 다섯 가지 오류 주입 전략의 재사용 가능한 집합.
3. 실증적 통찰: 정리 증명 분야의 특정 훈련보다 최첨단 및 저자 모델에서 발견된 일반 보상 모델링 능력이 증명 평가에 더 효과적으로 이전된다는 발견.

저자들은 효과적인 보상 모델을 개발하면 수학 발견과 검증을 가속화할 수 있지만, 현재 모델에는 상당한 한계가 있음을 강조합니다. 불완전한 보상 모델은 과도한 의존의 위험을 내포하므로, 공식 검증이 정확성의 궁극적인 심판자임을 지적합니다. 이 벤치마크는 공식 수학에 대한 보상 모델에 대한 추가 연구를 장려하기 위해 공개되었습니다.

이 논문은 대부분의 예시에서 자동 검증을 의존한다는 점, Lean 4 에만 초점을 맞춘다는 점, 그리고 프로세스 수준 또는 단계별 평가를 제외했다는 한계를 지적하며 마무리합니다. 향후 연구는 학습된 보상 모델과 공식 검증을 결합한 하이브리드 접근법과 Coq 및 Isabelle 과 같은 다른 증명 보조 도구로 벤치마크를 확장하는 데 초점을 맞출 것을 제안합니다.