Kimina-Prover: 정형 정리 증명을 위한 테스트 타임 RL 탐색

개요

Kimina-Prover-72B는 Lean 4 언어를 위해 설계된 최첨단 자동 정리 증명(ATP) 모델로, miniF2F-test 벤치마크에서 92.2%의 통과율을 달성했습니다. 테스트 타임 강화 학습(TTRL) 탐색과 새로운 오류 수정 메커니즘을 통합함으로써, 이 시스템은 단일 단계 추론을 넘어 복잡한 수학적 문제를 관리 가능한 하위 보조 정리(sub-lemma)로 자율적으로 분해합니다.

테스트 타임 강화 학습(TTRL) 탐색

TTRL 탐색 프레임워크는 정리 증명을 무작위 탐색에서 목표 지향적인 에이전트 프로세스로 전환합니다. 이 프레임워크는 모델이 중간 보조 정리를 식별하고 이를 증명 구성에 통합하도록 훈련되는 "보조 정리 활성화 패턴(lemma-enabled pattern)"을 활용합니다.

TTRL 프레임워크의 주요 구성 요소는 다음과 같습니다:

• 동적 보조 정리 점수 산정: 시스템은 탐색 범위 내에서 보조 정리의 유용성을 추적하며, 성공적인 증명에 자주 기여하는 보조 정리에 우선순위를 부여하고 최소 활용 임계값(τ=0.10)을 충족하지 못하는 보조 정리는 제거합니다.
• 재귀적 분해: 정리나 보조 정리가 128번의 시도 후에도 증명되지 않으면, 시스템은 하위 보조 정리 생성 프로세스를 트리거합니다. 이를 통해 모델은 어려운 문제를 재귀적으로 더 작고 증명 가능한 구성 요소로 분해할 수 있습니다.
• 논리적 건전성: 모델이 일관성 없는 내용을 악용하여 사소한 증명을 생성하는 것을 방지하기 위해, 시스템은 "부정 증명 프로세스"를 사용합니다. 생성된 보조 정리의 논리적 부정이 증명 가능하다면, 원래의 보조 정리는 일관성이 없는 것으로 간주되어 폐기됩니다.

오류 수정 및 샘플 효율성

Kimina-Prover는 증명을 처음부터 다시 시작하는 대신 Lean의 오류 메시지를 해석하여 반복적인 수정을 수행함으로써 샘플 효율성을 향상시킵니다. 연구팀은 Claude 3.7 Sonnet에 의해 합성된 단계별 추론 체인으로 보강된 (잘못된 증명, Lean 피드백, 올바른 증명) 삼중항으로 구성된 특수 지도 미세 조정(SFT) 데이터셋을 개발했습니다.

이를 강화 학습 루프에 통합하기 위해 연구팀은 "배치 실패 재생(Batched Failure Replay)" 전략을 구현했습니다. 이전의 실패 사례와 표준 문제의 고정 크기 결합에 대해 훈련함으로써, 모델은 복잡한 논리적 실수와 구문 오류를 해결하는 방법을 학습하며, 동일한 계산 예산 하에서 무차별 대입 샘플링 전략보다 지속적으로 우수한 성능을 보입니다.

모델 변형 및 성능

주력 모델인 72B 파라미터 모델 외에도 다양한 배포 요구 사항을 지원하기 위해 증류된 변형 모델이 포함되어 있습니다:

• Kimina-Prover-72B: Qwen2.5-72B 기반, miniF2F-test에서 92.2% 달성.
• Kimina-Prover-Distill-8B: Qwen3-8B 기반.
• Kimina-Prover-1.7B: Qwen3-1.7B 기반.

성능 데이터에 따르면 초기 모델은 샘플링 예산에 따라 선형적으로 확장되었지만, 현재 시스템은 pass@1024를 넘어서면 효율이 감소하는 경향을 보입니다. 이는 추가적인 성능 향상이 단순한 샘플링 양보다는 TTRL이 제공하는 정교한 탐색 전략에 더 크게 의존함을 시사합니다.