🖼️ 인포그래픽

🖼️ 4컷 인포그래픽

💡 한 줄 요약

김이나-프로버는 중간 보조정리를 재귀적으로 생성·선별·결합하는 테스트 시점 강화학습 탐색과 린 오류 기반 교정 기능을 통해 미니에프투에프에서 92.2%의 최고 통과율을 기록한 형식 정리 증명 모델이다.

📌 핵심 요약

• 김이나-프로버-72B는 큐웬2.5-72B를 기반으로 키미 k1.5 강화학습 파이프라인을 적용한 린 4 정리 증명 모델이며, 8B와 1.7B 증류 모델도 함께 공개됐다.
• 핵심 혁신은 여러 중간 보조정리를 재귀적으로 발견하고 조합하는 테스트 시점 강화학습 탐색과, 린의 오류 메시지를 해석해 기존 증명을 부분적으로 수정하는 오류 교정 능력이다.
• 보조정리 활용 패턴은 문제 문맥에 1~3개의 보조정리를 제공하고, 이를 유용하게 사용한 증명 궤적에 더 높은 보상을 부여해 활용률을 안정적으로 30~40%까지 높였다.
• 탐색 과정은 보조정리 활용 점수에 따라 유망한 후보를 집중적으로 재사용하면서 무작위 후보도 섞고, 기여도가 낮은 보조정리는 제거하며, 증명에 실패한 정리에는 새로운 하위 보조정리를 생성한다.
• 김이나-프로버-72B는 미니에프투에프에서 패스@1 63.9%, 패스@32 84.0%, 패스@1024 87.7%를 달성했고, 전체 테스트 시점 강화학습 탐색을 적용했을 때 최종 92.2%에 도달했다.

🧩 주요 포인트

1. 김이나-프로버-72B는 큐웬2.5-72B를 기반으로 키미 k1.5 강화학습 파이프라인을 적용한 린 4 정리 증명 모델이며, 8B와 1.7B 증류 모델도 함께 공개됐다.
2. 핵심 혁신은 여러 중간 보조정리를 재귀적으로 발견하고 조합하는 테스트 시점 강화학습 탐색과, 린의 오류 메시지를 해석해 기존 증명을 부분적으로 수정하는 오류 교정 능력이다.
3. 보조정리 활용 패턴은 문제 문맥에 1~3개의 보조정리를 제공하고, 이를 유용하게 사용한 증명 궤적에 더 높은 보상을 부여해 활용률을 안정적으로 30~40%까지 높였다.
4. 탐색 과정은 보조정리 활용 점수에 따라 유망한 후보를 집중적으로 재사용하면서 무작위 후보도 섞고, 기여도가 낮은 보조정리는 제거하며, 증명에 실패한 정리에는 새로운 하위 보조정리를 생성한다.
5. 김이나-프로버-72B는 미니에프투에프에서 패스@1 63.9%, 패스@32 84.0%, 패스@1024 87.7%를 달성했고, 전체 테스트 시점 강화학습 탐색을 적용했을 때 최종 92.2%에 도달했다.

🧠 상세 정리

1. 모델 공개와 핵심 성과

연구팀은 린 4 형식 정리 증명을 위한 김이나-프로버-72B를 공개했다. 이 모델은 큐웬2.5-72B를 기반으로 하며, 키미 k1.5 강화학습 파이프라인을 이용해 훈련됐다. 큐웬3-8B와 큐웬3-1.7B를 각각 기반으로 한 김이나-프로버-디스틸-8B 및 1.7B 증류 모델도 함께 제공된다. 연구가 강조하는 두 가지 핵심 혁신은 여러 보조정리를 재귀적으로 발견하고 결합하는 테스트 시점 강화학습 탐색과, 린의 오류 메시지를 읽어 표적 수정안을 만드는 오류 교정 기능이다. 이러한 기법을 모두 적용한 72B 모델은 미니에프투에프 시험 세트에서 최종 92.2%의 통과율을 기록하며 기존 방법을 넘어섰다고 보고됐다.

2. 자동 정리 증명의 배경과 기존 접근의 한계

연구의 목표는 린 4 언어에서 형식 수학 증명의 구성을 자동화하는 것이다. 논문은 국제수학올림피아드 수준의 문제에서 성과를 보인 알파프루프, 강화학습을 적용한 딥시크-프로버-V2, 대규모 훈련 없이 모듈식 구성으로 경쟁력을 보인 신경기호적 에이전트 방식인 디에스피 플러스를 주요 선행 사례로 제시한다. 이전 김이나-프로버 프리뷰는 대규모 강화학습과 추론 중심 탐색을 통해 미니에프투에프의 새로운 기준을 세웠고, 큰 모델이 더 강한 형식 추론기로 기능할 수 있음을 보였다. 그러나 한 번의 생성이나 단일 단계 추론만으로는 길고 복합적인 증명을 해결하기 어려웠다. 이에 연구팀은 복잡한 문제를 재사용 가능한 하위 구성요소로 분해하고, 여러 중간 보조정리를 결합하는 장기 탐색 구조를 도입했다.

3. 벤치마크 결과와 탐색 확장의 의미

동일한 표본 추출 예산에서 김이나-프로버-72B는 패스@1 63.9%, 패스@32 84.0%, 패스@1024 87.7%를 기록해 표에 제시된 모든 평가 설정에서 가장 높은 성능을 보였다. 패스@32 결과에 한 차례 오류 교정을 추가하면 통과율은 86.4%로 상승했다. 전체 테스트 시점 강화학습 탐색을 적용한 최종 통과율은 92.2%이며, 이에 사용된 추정 통과 예산 상한은 약 4만 2천으로 제시됐다. 다만 현재 표본 추출의 상당 부분이 도움이 되지 않거나 중복된 보조정리를 증명하는 데 소비되므로 예산을 크게 최적화할 여지가 있다고 연구팀은 설명한다. 또한 패스@1024 이후에는 표본 수 증가의 효과가 둔화되어, 추가 성능 향상에는 단순한 표본 확대보다 정교한 탐색 전략이 더 중요하다는 변화가 관찰됐다.

4. 보조정리 활용 패턴의 훈련 방식

보조정리 활용 패턴은 입력에 주어진 중간 보조정리 가운데 유용한 것을 식별하고 최종 증명에 적용하도록 모델을 훈련하는 방식이다. 강화학습 과정에서는 무작위로 선택한 1~3개의 형식 보조정리를 문제 문맥 앞에 붙여, 모델이 중간 결과를 활용할 기회를 제공한다. 후보 보조정리는 먼저 범용 대규모 언어 모델이 자연어로 생성하고, 이후 김이나-오토포멀라이저-7B가 형식 명제로 변환하는 두 단계 절차로 준비된다. 초기에는 모델이 제공된 보조정리를 거의 사용하지 않았기 때문에, 같은 정리를 여러 경로로 증명할 수 있을 때 보조정리를 활용한 궤적에는 더 높은 보상을 주고 활용하지 않은 궤적에는 불이익을 주는 선호 기반 보상 조정이 도입됐다. 그 결과 보조정리 활용률은 훈련 후 안정적으로 30~40%에 도달했으며, 모델은 관련 보조정리는 선택적으로 사용하고 무관한 것은 무시하는 행동도 학습했다.

5. 테스트 시점 강화학습 탐색의 구성

무작위로 보조정리를 삽입하는 방식만으로는 깊게 중첩되고 구조화된 추론이 필요한 문제를 충분히 해결할 수 없었다. 테스트 시점 강화학습 탐색은 이 한계를 넘기 위해 많은 후보 보조정리를 체계적으로 조직하고 선별하며 조합하는 훈련 가능한 에이전트형 프레임워크로 설계됐다. 각 문제와 그에 연결된 후보 보조정리 집합은 하나의 탐색 범위를 이루며, 각 보조정리가 최종 증명에 얼마나 자주 효과적으로 기여하는지를 나타내는 활용 점수가 관리된다. 매 강화학습 반복의 시작에는 문제마다 서로 다른 보조정리 조합을 앞에 붙인 열 개의 입력 변형을 만든다. 이 가운데 60%는 활용 점수가 높은 상위 보조정리 중심으로 구성하고, 나머지 40%는 상위 후보와 함께 1~4개의 무작위 보조정리를 추가해 새로운 조합을 탐색한다.

6. 후보 가지치기와 재귀적 하위 문제 생성

탐색 과정에는 지속적으로 기여하지 못하는 보조정리를 제거하는 품질 관리 절차가 포함된다. 특정 보조정리가 50번 삽입된 뒤에도 활용 점수 0.10 이상을 달성하지 못하면 탐색 후보군에서 제외된다. 동시에 탐색 범위는 원래 정리에만 머무르지 않고 각 보조정리에도 별도로 유지되므로, 어려운 문제를 더 작은 하위 문제로 재귀적으로 분해할 수 있다. 정리 또는 보조정리가 128번의 시도 이후에도 증명되지 않으면 병렬 하위 보조정리 생성 과정이 새로운 후보를 만든다. 이 구조는 단순히 같은 문제에 더 많은 답을 생성하는 대신, 증명 실패 지점을 중심으로 추론 깊이를 확장하고 중간 결과를 다시 조합하는 테스트 시점 확장을 가능하게 한다.

7. 부정 증명을 통한 논리적 건전성 보호

자동 생성된 보조정리를 사용하는 과정에서는 자연어 후보가 형식 명제로 잘못 변환될 위험이 있다. 잘못 형식화된 명제가 논리적 모순을 일으키면 모델은 그 모순을 이용해 겉으로는 유효해 보이지만 실제로는 건전하지 않은 증명을 구성할 수 있다. 연구팀은 이를 막기 위해 새로 생성된 보조정리마다 그 명제의 논리적 부정을 증명해 보는 부정 증명 절차를 도입했다. 부정된 명제가 증명되면 원래 보조정리가 논리적으로 일관되지 않는다는 신호로 보고 즉시 후보군에서 폐기한다. 따라서 보조정리 생성과 재귀 탐색이 확대되더라도, 모순된 중간 명제가 최종 증명 경로에 남아 잘못된 성공을 만드는 가능성을 필터링하도록 설계됐다.

8. 린 오류 피드백을 활용한 증명 교정

기존의 고성능 정리 증명 모델은 인간 사용자가 일상적으로 활용하는 증명 보조기의 오류 피드백을 바탕으로 결과를 수정하는 능력이 부족했다. 김이나-프로버는 잘못된 증명, 린의 피드백, 올바른 증명으로 구성된 삼중항 형태의 전문 지도 미세조정 자료를 구축해 이 문제에 대응했다. 범용 대규모 언어 모델은 린 오류를 해석하고 유효한 수정안을 제시하는 성공률이 낮았기 때문에, 연구팀은 클로드 3.7 소넷으로 오류 피드백에 따라 잘못된 증명을 올바른 증명으로 바꾸는 단계별 추론 과정도 합성했다. 이렇게 만든 자료는 최초 증명과 수정 결과뿐 아니라 그 사이의 교정 논리까지 학습 신호로 제공한다. 다만 이 지도 미세조정 모델의 초기 오류 수정 성공률은 약 1%에 그쳤고, 이를 강화학습에 직접 통합하면 보상이 희소해지고 훈련이 불안정해져 연구팀은 배치 실패 재생 전략을 설계했다고 설명한다.

🧾 핵심 주장 / 시사점

• 성능 곡선이 패스@1024 이후 둔화된다는 결과는 형식 증명 성능을 높이기 위해 단순 표본 수 확대보다 보조정리의 우선순위화·재사용·재귀 분해가 중요해졌음을 보여준다.
• 보조정리 사용에 무조건 보상하지 않고 실제로 유용한 경우에 선택적으로 활용하도록 훈련한 결과, 30~40%의 안정적인 활용률과 무관한 후보를 무시하는 행동이 함께 나타났다.
• 오류 교정은 증명을 처음부터 다시 생성하는 대신 린의 구체적인 피드백을 이용해 기존 증명을 수정하는 접근이지만, 초기 성공률이 약 1%여서 희소 보상과 훈련 안정성을 별도로 해결해야 했다.

✅ 액션 아이템

• Kimina-Prover-72B의 Qwen2.5-72B 기반 Lean4 모델을 k1.5 강화학습 파이프라인으로 고정하고 공개된 8B·1.7B 증류본도 동일 축에서 성능을 추적한다.
• 보조정리 탐색 흐름을 점수 기반 재사용, 무작위 후보 혼합, 저기여 보조정리 제거, 실패 정리의 하위 보조정리 생성으로 분해해 실험 동작을 정밀하게 기록한다.
• 미니F2F 성능을 패스@1 63.9, 패스@32 84.0, 패스@1024 87.7, 테스트 시점 RL 적용 후 92.2로 분해해 정량 판정 기준과 모델 간 비교 규칙을 둔다.

❓ 열린 질문

• 보조정리 활용률 30~40%를 실제로 유지시키는 보상 설계의 검증은 어떤 실험 조건에서 반복 가능한가?
• 린 오류 메시지 해석 기반 부분 수정이 잘못된 추론 경로를 유도하지 않도록 하는 경계 규칙은 무엇으로 정할 것인가?
• 패스@1에서 패스@1024, 그리고 최종 92.2로 개선되는 과정은 신뢰도 향상으로 해석 가능한가, 아니면 탐색 범위 확장 효과에 편향된 것인가?