보통 시험에서는 학습을 끝낸 뒤 문제를 풉니다. AlphaProof는 특히 어려운 문제를 만나면 주변 변형 문제를 대량으로 만들고, 그 문제군에서 다시 강화학습해 탐색 전략을 조정합니다. 풀이 중 학습과 검증기가 결합된 셈입니다.
연구를 읽는 두 가지 질문
2025년 온라인 공개된 Nature 논문입니다
Hubert 등은 2025년 11월 12일 공개된 논문에서 AlphaProof의 구조와 평가를 상세히 보고했습니다. 2026년 Nature 651권에 수록됐으며, Lean의 상태·전술·보상으로 증명 탐색을 순차 의사결정 문제로 정의했습니다. [1]
대규모 형식 문제로 자기 경험을 만들었습니다
3B 매개변수 증명망을 코드·수학 텍스트 약 3천억 토큰으로 사전학습하고 Mathlib 사람 증명 약 30만 상태-전술 쌍으로 미세조정했습니다. 자연어 문제 약 100만 개를 약 8천만 형식 문제로 확장해 증명·반증 시도의 검증된 결과로 강화학습했습니다. [1]
시험시점 학습은 한 문제 주변에 계산을 집중합니다
일반 트리 탐색으로 풀기 어려운 목표에는 변형 생성기가 단순화·일반화 등 관련 문제를 만들고, 그 전용 교육과정에서 다시 강화학습합니다. 논문은 검색 12 TPU시간 이후 이 단계가 formal-IMO와 Putnam 시험에서 각각 추가 15%포인트가량의 해결률을 제공했다고 보고합니다. [1]
IMO 성과에는 시간과 범위 조건이 붙습니다
2024 IMO에서 비기하 5문제 중 3문제를 풀고 AlphaGeometry 2와 합쳐 은메달 수준 점수를 얻었지만, 인간보다 훨씬 긴 다일 계산을 사용했습니다. 형식화 충실성, 기하의 별도 시스템, 비공개 계산 자원 때문에 ‘모든 수학을 이해한다’는 결론은 허용되지 않습니다. [1]
하나의 목표 주변에 연습문제 만들기
목표가 ‘모든 n에서 식 F(n)이 성립함’이라면 n의 작은 값, 조건을 강화한 보조정리, 일부 항을 제거한 단순형을 주변 변형으로 만들 수 있습니다. 검증기는 각 전술이 새 상태를 만드는지 즉시 판정합니다.
변형을 많이 풀었다고 원 목표가 자동으로 증명되지는 않습니다. 변형에서 배운 정책이 원 목표의 유망한 보조정리와 전술을 찾도록 탐색을 안내하고, 최종 증명항은 Lean 커널이 다시 검사합니다.
LTCT AI 평가에는 정답률과 함께 사용 계산량, 형식화 충실성, 검증 성공, 문제별 추가 학습 여부를 표시해야 합니다. 같은 정답 수라도 자원 조건이 다르면 직접 비교할 수 없습니다.
어디까지 말할 수 있을까요?
- 공개 논문은 시스템 전체를 설명하지만 학습 데이터·분산 계산 인프라의 모든 세부를 외부가 동일하게 재현하기 어렵습니다.
- IMO 성과는 제한된 형식화 문제와 막대한 다일 계산 조건이며 일반 자연어 추론·교육 효과로 확장되지 않습니다.
원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]
교육 현장과 연결해 보면
어려운 증명 한 문제를 바로 여러 번 푸는 기록과 주변 변형 문제를 먼저 연습한 기록을 비교합니다. 학생은 평가 도중 추가된 학습 자료와 사용한 시간·시도 수를 표로 정리합니다.
교사는 시작 상태에서의 성과와 문제별 추가 학습 뒤의 성과를 나누어 설명하게 합니다. 검증기가 확인한 증명과 아직 확인하지 못한 설명도 구분하여 비교 조건을 밝힙니다.
Lean 커널이 최종 증명을 검사했다는 사실과 자연어 문제가 올바르게 형식화됐다는 사실은 왜 다른가요?
생각을 비교할 해설 펼치기
커널은 주어진 형식 명제의 증명항만 검사합니다. 그 명제가 원래 자연어 문제의 뜻을 충실히 옮겼는지는 별도의 의미 검수입니다.
원문과 출처 정보
한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.
강화학습을 이용한 올림피아드 수준 형식 수학 추론 (Olympiad-level Formal Mathematical Reasoning with Reinforcement Learning)
Thomas Hubert et al. (2026). Nature 651, 607–613.
- 자료 성격
- 공개 학술자료
- 읽은 버전
- 2025-11-12 온라인 공개, 2026 Nature 651권 출판
- 확인 범위
- 공개 본문 전체: Lean 환경, 자료·훈련, 검색과 시험시점 강화학습, 벤치마크, 계산량과 방법
- 원문 확인일
이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준