Kimina-Prover: 대규모 형식 추론 모델에 테스트 타임 RL 검색 적용

Numina & Kimi 팀

Figure 1:
miniF2F-테스트 데이터셋에서 명제 증명 모델의 성능 비교.

우리는 Kimina-Prover-72B, Qwen2.5-72B [2] 기반의 Kimi k1.5[1] RL 파이프라인으로 훈련된 최첨단 명제 증명 모델을 출시한다고 기쁘게 발표합니다. 함께, 우리는 또한 두 가지蒸馏 변형을 출시합니다: Kimina-Prover-Distill-8B와 1.7B(Qwen3-8B 및 Qwen3-1.7B[3] 각각에 기반함).

우리의 핵심 혁신은 다음과 같습니다:

테스트 타임 강화학습 검색 (Test-Time RL Search): 모델이 여러 명제 (lemma) 를 순차적으로 발견하고 결합하여 복잡한 증명 구조를 구축할 수 있도록 하는 훈련 가능한 에이전트 증명 프레임워크. 이는 새로운 명제 활성화 패턴 (lemma-enabled pattern) 을 기반으로 합니다.

오류 수정 능력 (Error-Fixing Capability): Kimina-Prover 는 Lean 의 오류 메시지를 읽고 해석하며 표적화된 수정안을 제안할 수 있으며, 처음부터 증명을 재생성하는 것보다 훨씬 높은 샘플 효율성을 보여줍니다.

이러한 발전은 Kimina-Prover 가 어려운 수학 문제를 해결하고 이전 방법들을 능가하도록 합니다. Figure 1 에 따르면, 널리 사용되는 miniF2F 벤치마크에서 Kimina-Prover 는 92.2% 의 최첨단 통과율을 달성했습니다.

우리는 Lean 4 언어의 자동 명제 증명 (ATP) 에 집중하여 형식 수학 증명의 구축을 자동화하는 것을 목표로 합니다. 신경 기반 명제 증명 (neural theorem proving) 의 최근 발전은 AI 시스템이 이 과정을 보조하거나 자동화하는 능력을 크게 향상시켰습니다. 주목할 만한 성과로는 Google DeepMind 의 AlphaProof[4] 가 있으며, 이는 국제 수학 올림피아드 수준 문제에서 강력한 성능을 입증했습니다. 또한 강화학습을 통합한 오픈소스 시스템인 DeepSeek-Prover-V2[5] 는 최첨단 결과를 달성했습니다. 또한 DSP+ [6] 과 같은 신경-기호 에이전트 접근 방식은 모듈러 프레임워크에서 오프더샤프 모델을 활용함으로써 대규모 훈련 없이도 경쟁력 있는 성능이 가능함을 보여줍니다.

우리의 이전 작업인 Kimina-Prover Preview[7] 는 Lean 의 형식 명제 증명을 위한 대형 언어 모델을 소개하여 miniF2F 벤치마크에 대한 새로운 성능 기준을 설정했습니다. 대규모 강화학습 파이프라인으로 훈련된 이 모델은 추론 기반 탐색 패러다임을 채택했으며, 더 큰 모델이 더 강력한 형식 추론자로 봉사할 수 있음을 입증했습니다. 이 구조화된 추론 패턴은 효율적인 증명 검색과 인간과 유사한 문제 해결 전략을 모방하는 것을 가능하게 했습니다.

이 초기 성공 이후, 우리는 추가 강화학습 반복을 통해 모델을 계속 개선해 왔습니다. 그러나 단일 단계 추론 (single-step reasoning) 은 긴 다단계 증명이 필요한 복잡한 문제를 해결하기에는 부족합니다. 이 한계를 해결하기 위해, 모델이 여러 중간 명제 (lemma) 를 자율적으로 발견하고 결합하며 재사용할 수 있도록 하는 테스트 타임 강화학습 (TTRL) 검색 프레임워크를 소개합니다. 이 프레임워크는 어려운 문제를 재사용 가능한 하위 구성 요소로 분해함으로써 더 깊은 장기적 추론 (long-horizon reasoning) 을 지원합니다.

TTRL 검색의 핵심 재료는 명제 활성화 패턴 (lemma-enabled pattern) 으로, 이는 모델이 증명 구축 과정의 일부로 중간 명제를 식별하고 적용할 수 있게 합니다. 이 구조화된 중간 결과의 재사용은 단일 단계 생성을 넘어 모델의 문제 해결 능력을 크게 확장시킵니다.

Robustness을 더욱 강화하기 위해 우리는 Lean의 오류 메시지를 해석하고 표적 수정을 제안하는 오류 수정 메커니즘도 통합했습니다. 이는 모델이 반복적인 피드백을 통해 출력을 정교화하여 증명 신뢰도와 전체 샘플 효율성을 개선할 수 있게 합니다.

Model	pass@1	pass@32	pass@1024
Kimina-Prover-1.7B	46.7	73.4	—
...
Table 1:

miniF2F 테스트 데이터셋에서 등가 샘플링 예산 하에 증명 모델의 성능 비교. Kimina-Prover-72B는 모든 평가 설정에서 최상위 성능을 달성했습니다.

제안된 기법의 조합이 형식적 정밀 증명 성능에 상당한 개선점을 가져온다는 점입니다. miniF2F 벤치마크에서, Kimina-Prover 는 pass@32 로 84.0% 의 통과율을, 단일 라운드의 오류 수정 추가와 함께 86.4%, pass@1024 로는 87.7% 의 통과율을 기록했습니다. 전체 Test-Time Reinforcement Learning (TTRL) 검색 프레임워크를 적용하면 최종 통과율은 92.2% 로, 추정된 통과 상한선은 약 42,000 입니다. 그러나 현재 샘플링의 상당 부분이 도움이 되지 않거나 중복적인 명제를 증명하는 데 사용되므로, 향후 버전에서는 이 통과 예산을 크게 최적화할 수 있습니다.

특히, 이러한 결과는 증명 시스템의 스케일링 행동 변화가 있음을 시사합니다. 이전 버전은 샘플링 예산 증가에 대해 로그 스케일에서 약 선형 개선점을 보였으나, 현재 시스템은 pass@1024 이후 감소하는 수익을 보입니다. 이는 추가적인 이득이 샘플링 증가보다 더 의존적이지 않으며, TTRL 로 도입된 것과 같은 더 정교한 검색 전략이 필요함을 시사합니다.

명제 활성화 패턴 (lemma-enabled pattern) 은 모델에 입력에 제공된 유용한 명제를 식별하고 활용하는 능력을 부여하도록 설계되었습니다. 이 기능을 지원하기 위해, 강화 학습 (RL) 훈련 중에는 문제 컨텍스트 앞에 1 개에서 3 개의 형식적 명제의 무작위 하위집합이 추가되어, 증명자가 최종 증명을 구성하는 데 도움이 될 수 있는 잠재적으로 유용한 중간 결과를 노출시킵니다. 이러한 명제들은 2 단계 파이프라인을 통해 준비됩니다: (1) 일반 목적 LLM 이 자연어에서 후보 명제를 생성합니다; (2) 이를 우리의 Kimina-Autoformalizer-7b 를 사용하여 형식적 문장으로 번역합니다.

초기 관찰은 모델이 제공된 명제를 통합하는 경향이 낮음을 보였습니다. 이를 해결하기 위해, 우리는 RL 프레임워크 내에서 선호도 기반 보상 형성 전략을 도입했습니다. 여러 경로로 증명 가능한 정리에 대해, 제공된 명제를 성공적으로 활용하여 증명된 해답에 더 높은 보상을 부여하고, 그렇지 않은 경우 벌점을 부과했습니다. 이 접근법은 효과적이며, 훈련 후 명제 활용율을 30–40% 로 안정화시켰습니다. 중요한 것은 이 방법이 명제 사용을 장려하는 것뿐만 아니라 선택성을 촉진한다는 점입니다: 모델은 유용할 때 전략적으로 명제를 적용하고, 관련 없는 경우를 무시하여 더 효율적이고 인간 같은 추론 행동을 보였습니다.

Figure 2:

Test-Time Reinforcement Learning (TTRL) 검색 프레임워크 다이어그램. 이는 RL 훈련, 하위명제 생성, 부정 필터링으로 구성된 3 개의 주요 구성 요소로 이루어집니다. 하위명제는 생성되고 형식화된 후, 동적 점수와 가지치기를 포함하여 훈련 루프에 통합됩니다. 부정 필터는 논리적 일관성을 보장하기 위해 유효하지 않은 명제를 제거합니다.

lemma-enabled pattern은 모델이 증명을 구성할 때 사전 생성된 lemmas(명제)를 중간 단계로 통합하도록 허용했습니다. 그러나 무작위로 샘플링하고 lemmas 를 삽입하는 것은 고도로 구조화되고 깊게 중첩된 추론을 요구하는 복잡한 문제를 해결하기에는 부족함이 있었습니다. 이 한계를 극복하기 위해, 우리는 Test-Time Reinforcement Learning Search (TTRL) 프레임워크를 개발했습니다. TTRL 은 학습 가능한 에이전트 접근 방식으로, 후보 lemmas 를 체계적으로 조직하고 필터링하며 조합하여 완전한 증명을 구축합니다. 이 프레임워크는 과정을 무작위 탐색에서 더 전략적이고 목표 지향적인 검색으로 전환시킵니다.

Figure 2 에 따르면, 우리는 각 문제의 **search scope (검색 범위)**를 해당 문제와 관련된 후보 lemmas 와 함께 정의합니다. TTRL Search 는 각 search scope 내에서 **lemma utilization score(lemma 활용 점수)**를 추적하여 최종 증명에 각 lemma 이 얼마나 자주 그리고 효과적으로 기여하는지 측정합니다. 각 RL training iteration(강화학습 훈련 반복) 의 시작 시, 각 문제 (즉, search scope) 에 대해 우리는 lemmas 를 다른 조합으로 붙여 K = 10개의 입력 변형을 구성합니다. 탐험과 활용을 균형 있게 하기 위해, **60%**의 입력은 가장 높은 활용 점수를 가진 top-ranking lemmas(최고 순위 lemmas)를 사용하여 구축되며, 모델이 가장 유망한 증명 경로를 집중시킵니다. 나머지 **40%**는 이러한 top lemmas 를 포함하고 1 개에서 4 개의 무작위로 선택된 추가 lemmas 를 포함하여 새로운 및 잠재적으로 유용한 lemma 조합의 탐험을 장려합니다.

품질 보장을 위해, **filtering mechanism(필터링 메커니즘)**은 일관되게 의미 있게 기여하지 못하는 lemmas 를 잘라냅니다: 50 번의 insertion attempts(삽입 시도) 후 활용 점수가 τ=0.10 보다 낮지 않은 모든 lemmas 는 검색 풀에서 제거됩니다.

TTRL 의 핵심 기능은 **recursive search mechanism(재귀적 검색 메커니즘)**입니다. search scope 는 원래 정리에만 제한되지 않고, 각 lemma 에 대해서도 유지되며, 프레임워크가 문제를 더 작은 subproblems(부분 문제) 으로 재귀적으로 분해할 수 있게 합니다. 병렬로 **sublemma generation process (부분 명제 생성 과정)**이 계속 실행되며, 정리나 lemmas 가 N = 128 번의 시도 후 증명을 찾지 못하면 새로운 후보 sublemmas 가 생성됩니다. 이 재귀적 전략은 추론 깊이의 test-time scaling(테스트 시간 확장) 을 가능하게 하여 모델의 효과적인 문제 해결 능력을 크게 확장합니다.

논리적 타당성을 유지하기 위해, 우리는 오직 formalized lemmas (형식화된 명제) 가 잘못되면 단순하거나 무효한 증명을 유도할 수 있는 실패 모드를 해결합니다. 이러한 경우, 모델은 일관성 없는 부분을 이용하여 겉보기에는 유효하지만 불완전한 해를 구성할 수 있습니다. 이를 방지하기 위해, 우리는 **negation proving process (부정 증명 과정)**을 도입했습니다: 새로 생성된 lemmas 에 대해 논리적 부정 (logical negation) 을 증명하는 시도를 합니다. 부정 문장이 증명 가능하면, 이는 원래 lemmas 가 논리적으로 모순적임을 의미하며 즉시 제거됩니다. 이 단계는 전체 증명 구축 과정의 신뢰성과 타당성을 보장합니다.

최근 고급 정리 증명 모델의 중요한 한계는 증명 보조 프로그램 (proof assistant) 의 피드백을 기반으로 증정을 수정할 수 있는 능력의 부재입니다. 이는 인간 사용자가 정기적으로 활용하는 기능입니다. 이 격차를 해소하기 위해, 우리는 **error-fixing capabilities(오류 수정 능력)**을 Kimina-Prover 에 통합하기 위한 전용 프레임워크를 개발했습니다.

오류 수정을 위한 SFT 데이터 생성. 일반 목적의 대규모 언어 모델은 Lean 의 오류 메시지를 해석하고 유효한 수정안을 제안할 때 낮은 성공률을 보입니다. 이를 극복하기 위해, 우리는 오류 수정에 특화된 지도 기반 미세 조정 (Supervised Fine-Tuning, SFT) 데이터를 구축했습니다. 이 데이터셋은 (오류 있는 증명, Lean 피드백, 올바른 증명) 형식의 삼중항으로 구성됩니다. 감독 신호를 풍부하게 하기 위해, 우리는 Claude 3.7 sonnet[8] 를 사용하여 제공된 피드백을 활용하여 오류 있는 증명을 어떻게 올바른 것으로 변환할 것인지 단계별 추론 체인을 생성하도록 프롬프트를 구성했습니다. 그 결과, 초기 및 수정된 증명뿐만 아니라 중간 추론도 포함된 고품질의 데이터셋이 만들어졌으며, 이는 더 효과적인 학습을 가능하게 합니다.

배치 기반 실패 재플레이 전략. 오류 수정을 강화 학습 (RL) 루프에 직접 통합하는 것은 SFT 모델의 오류 수정 성공률이 낮음 (~1%) 으로 인해 초기에는 비효과적임. 이로 인해 희소한 보상과 불안정한 훈련이 발생했습니다. 이를 해결하기 위해, 우리는 배치 기반 실패 재플레이 (Batched Failure Replay) 전략을 설계했습니다. RL 반복 중 오류를 즉시 수정하려는 것이 아니라, N 번 반복의 모든 실패한 증명 시도를 수집합니다. 다음인 N+1 번 반복에서 훈련 배치는 이전 실패 (예: 500 샘플) 와 프롬프트 세트의 표준 문제 (예: 또 다른 500 샘플) 의 고정 크기 합집합으로 구성됩니다. 이는 각 훈련 단계마다 오류 수정 작업에 일관되고 높은 부하의 노출을 보장하며, 모델이 안정적이고 데이터 효율적인 방식으로 효과적인 오류 처리 행동을 점진적으로 학습할 수 있게 합니다.

16+16 시도 및 수정	32×1 브루트 포스	32+32 시도 및 수정
kimina-prover	35.6	28.8

표 2:
오류 수정 전략과 브루트 포스 전략의 성능 비교. 가장 낮은 승률의 선택된 MiniF2F-Test 문제 59 개에 대해 수행되었습니다. 동일한 샘플 예산에서 오류 수정 전략 (16+16) 은 브루트 포스 베이스라인 (32×1) 을 능가하며, 향상된 샘플 효율성을 입증합니다.

이러한 훈련 방식은 모델의 실패 회복 능력에 측정 가능한 개선점을 가져왔습니다. 모델은 기본 문법 오류를 수정하는 것에서 시작하여 복잡한 논리적 실수를 해결하고, 초기 시도가 실패할 때 대안 증명 전략을 발견하는 단계로 발전했습니다. 특히 이 기능은 샘플 효율성을 향상시켰습니다. 표 2 에 따르면, 고정된 계산 예산 하에 다른 전략들을 비교했습니다. 16+16 시도 및 수정 전략 (각각 16 번의 초기 증명 시도를 수행하고 그 후 1 번의 오류 수정 시도를 수행) 은 35.6% 의 성공률을 달성하여, 32 번의 독립적인 시도로 28.8% 를 달성한 32×1 브루트 포스 베이스라인을 능가했습니다. 샘플 예산을 오류 수정과 함께 32+32 로 증가시키면 성공률은 44.1% 가 됩니다. 이러한 결과는 모델이 자신의 오류를 수정할 수 있게 하는 것이 반복적인 시행착오보다 계산 자원의 더 효율적인 사용을 의미함을 보여줍니다.

우리의 핵심 TTRL 검색 및 오류 수정 외에도, 모델의 학습 과정과 문제 해결 능력을 향상시키기 위해 몇 가지 다른 새로운 기술을 개발했습니다.