큰 정리를 작은 목표로 나누면 AI 증명은 더 강해질까? DeepSeek-Prover-V2는 비형식 풀이를 하위 목표로 재귀 분해해 형식 추론의 학습 자료와 보상 구조를 만든다. 원자료의 발표일과 읽은 버전을 구분하고 연구 질문·방법·결과·한계와 LTCT 적용 제안을 차례로 살펴봅니다.
연구를 읽는 두 가지 질문
연구 질문
대형 언어모델이 복잡한 Lean 정리를 하위 목표로 나눈 추론 흔적을 학습하면 형식 증명 성능이 향상되는가? [1]
자료와 방법
Ren 등은 DeepSeek-V3가 자연어 문제와 Lean 목표를 작은 하위 목표로 재귀 분해하게 하고, 각 하위 목표의 형식 증명을 결합해 cold-start 자료를 만들었다. 이후 증명 검사기의 성공 신호를 사용한 강화학습으로 모델을 훈련했다. 2025년 7월 18일 v2 공개본에서 MiniF2F-test, PutnamBench와 325문항 ProverBench를 평가하며 추론 예산과 표본 수 조건을 함께 보고한다. [1]
핵심 결과
671B 모델은 MiniF2F-test에서 88.9%를 기록했고 PutnamBench 658문항 중 49문항을 풀었다. ProverBench에는 AIME 2024·2025 문제 15개가 포함됐는데 형식 증명 모델은 6개를 풀었고, 비형식 DeepSeek-V3 다수결은 8개를 풀어 자연어 풀이와 Lean 증명 사이 간극도 드러냈다. 하위 목표 분해는 긴 증명 탐색을 구조화하지만, 결과는 특정 벤치마크·도구·추론 예산에서 얻은 사전출판 성능이다. [1]
결과의 범위
arXiv v2 사전출판본으로 동료심사 확정판이 아니며 모델·벤치마크 수치는 이후 버전에서 바뀔 수 있다. 높은 pass 조건과 대규모 계산을 쓰는 벤치마크 성능은 한 번의 생성, 새로운 라이브러리, 사람에게 이해하기 쉬운 증명 품질을 보장하지 않는다. 연구에서 직접 확인된 내용과 LTCT가 제안하는 수업·평가 아이디어를 분리해 읽어야 합니다. 통계적 차이와 교육적 중요성은 같은 말이 아니며, 측정하지 않은 장기 행동이나 다른 집단까지 같은 결과가 난다고 확장하지 않습니다. [1]
구체적으로 생각해 보기
목표 G를 한 번에 생성하는 대신 보조정리 A와 B로 나누고 A→B→G의 의존 관계를 만든다. A와 B가 각각 검사기를 통과해도 연결에 필요한 가정이 빠지면 전체 증명은 실패한다. 따라서 하위 목표 성공률과 최종 컴파일 성공을 구분해야 한다.
LTCT 도식은 큰 목표가 두 하위 목표로 갈라졌다가 검증된 의존선으로 합류하는 구조다. 합류점과 화살표 끝은 노드 경계에 맞췄고 실제 논문 도표는 복제하지 않았다.
답을 고른 뒤 사용한 전제, 비교 기준, 남는 불확실성을 적습니다. 이 예시는 원 연구의 추가 결과가 아니라 LTCT가 만든 교육용 사례이며, 본문의 수치와 도식의 관계를 서로 대조했습니다.
어디까지 말할 수 있을까요?
- arXiv v2 사전출판본으로 동료심사 확정판이 아니며 모델·벤치마크 수치는 이후 버전에서 바뀔 수 있다.
- 높은 pass 조건과 대규모 계산을 쓰는 벤치마크 성능은 한 번의 생성, 새로운 라이브러리, 사람에게 이해하기 쉬운 증명 품질을 보장하지 않는다.
- 공개본에서 확인한 범위를 넘어 저자나 참가자의 속성을 추측하지 않았고 최초 발표일과 개정·권호 출판일을 구분했습니다.
원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]
교육 현장과 연결해 보면
긴 증명을 시작하기 전에 필요한 작은 목표들을 적고 의존 관계를 연결합니다. 학생은 먼저 해결할 수 있는 목표와 다른 결과를 기다려야 하는 목표를 나누어 봅니다.
AI가 제안한 분해안에서는 각 하위 목표가 원래 정리에 필요한지, 모두 해결하면 최종 결론에 닿는지 확인합니다. 교사는 하위 증명의 타당성과 전체 계획의 완결성을 별도로 피드백합니다.
하위 목표가 모두 맞으면 전체 증명도 반드시 맞을까?
생각을 비교할 해설 펼치기
각 하위 목표가 올바른 가정 아래 증명되고 연결 단계가 검사될 때만 그렇다. 독립 성공을 나열하는 것과 전체 의존 구조를 닫는 것은 다르다.
원문과 출처 정보
한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.
딥시크 증명기 버전 2: 하위 목표 분해 강화학습을 통한 형식 수학 추론 향상 (DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition)
Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, Chong Ruan (2025). arXiv:2504.21801v2.
- 자료 성격
- 공개 AI 사전출판 연구
- 읽은 버전
- 2025-04-30 v1, 2025-07-18 v2 공개본
- 확인 범위
- v2 공개 본문 전체의 자료 생성, 하위 목표 분해, 강화학습, MiniF2F·PutnamBench·ProverBench 결과
- 원문 확인일
이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준
같은 연구 흐름에서 이어 읽기
같은 원문, 저자·연구 흐름, 공통 개념 태그를 기준으로 연결한 관련 해설입니다.