DeepSeek-Prover-V1.5는 Lean 4 검증 피드백을 강화학습과 트리 탐색에 이용해 형식증명 성능을 평가했습니다. 이 글은 공개 원문에서 확인한 연구 질문·방법·결과를 협회의 적용 아이디어와 나누어 읽습니다.
연구를 읽는 두 가지 질문
연구 질문과 확인한 자료
Huajian Xin et al.의 원자료를 공개 전문으로 확인했습니다. Lean 4 형식언어에 특화한 모델을 지도 미세조정한 뒤 증명 보조기의 검증 결과로 강화학습하고, 내부 보상으로 다양한 경로를 찾는 RMaxTS를 결합해 miniF2F와 ProofNet에서 평가했습니다. [1]
방법과 핵심 결과
논문은 두 유도 프롬프트를 결합한 설정에서 miniF2F-test 63.5%, 대학 수준 ProofNet 25.3%의 통과율을 보고했습니다. 전체 증명을 한 번 생성하는 방식보다 검증 가능한 중간 상태를 따라 여러 경로를 탐색하는 장점을 보였습니다. 수치와 범주는 원문이 보고한 범위에서만 사용했습니다. [1]
해석의 범위와 한계
수치는 2024년 공개 모델·특정 샘플링 예산과 벤치마크 설정에 한정됩니다. Lean이 통과시킨 증명의 형식적 정확성과 자연어 설명의 교육적 품질은 다른 문제이며 데이터 중복 가능성도 계속 점검해야 합니다. 발표일과 확인한 버전을 구분하고 저자 국적은 추정하지 않았습니다. [1]
개념을 직접 점검하는 예시
한 정리에서 실패한 증명 경로와 검증된 중간 상태를 가지처럼 나누고, 보조기 피드백이 어느 가지를 닫는지 표시합니다.
그림은 후보 증명 → Lean 피드백 → 탐색 갱신 순서로 읽고 마지막 합류점에서 조건·범위·반례를 함께 확인합니다. 원 논문의 표나 그림을 복사하지 않고 LTCT가 개념 관계만 새로 그렸습니다.
어디까지 말할 수 있을까요?
- 수치는 2024년 공개 모델·특정 샘플링 예산과 벤치마크 설정에 한정됩니다. Lean이 통과시킨 증명의 형식적 정확성과 자연어 설명의 교육적 품질은 다른 문제이며 데이터 중복 가능성도 계속 점검해야 합니다.
- 이 연구만으로 LTCT 교육·시험의 효과를 확인할 수 없습니다. 적용안은 별도 비교 조건과 측정 계획이 필요한 제안입니다.
원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]
교육 현장과 연결해 보면
오류가 있는 짧은 증명과 증명 보조기의 피드백을 제시합니다. 학생은 오류가 난 줄의 목표와 사용할 수 있는 전제를 읽고, 다음에 시도할 규칙을 이유와 함께 제안합니다.
수정 전후의 증명 상태를 보존하고 닫힌 목표와 남은 목표를 표시합니다. 교사는 새 문장을 많이 만든 정도보다 피드백을 이용해 어느 장애를 해결했는지 살펴봅니다.
통과율 63.5%면 한 번 질문할 때 63.5% 확률로 맞는다는 뜻인가요?
생각을 비교할 해설 펼치기
반드시 아닙니다. 여러 샘플·프롬프트와 탐색 예산을 합친 벤치마크 통과율이므로 실제 단일 요청 조건과 구분해야 합니다.
원문과 출처 정보
한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.
딥시크 증명기 버전 1.5: 증명 보조기 피드백을 활용한 강화학습과 몬테카를로 트리 탐색 (DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search)
Huajian Xin et al. (2025). ICLR 2025.
- 자료 성격
- ICLR 국제학회 공개 논문
- 읽은 버전
- arXiv v1 2024-08-15 및 ICLR 2025 공개본 · 2026-09-12 전문 확인
- 확인 범위
- 공개 원문 전문에서 연구 질문, 방법, 표본·비교 조건, 핵심 결과와 해석 한계를 확인. arXiv v1 2024-08-15 및 ICLR 2025 공개본 · 2026-09-12 전문 확인
- 원문 확인일
- 영구 식별
- DOI 미기재 · 아래 보존판 주소로 안내
이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준
같은 연구 흐름에서 이어 읽기
같은 원문, 저자·연구 흐름, 공통 개념 태그를 기준으로 연결한 관련 해설입니다.