100단계 증명에서 매 단계 99% 정확하면 전체도 거의 성공할까요? 오류가 한 번만 나도 증명이 멈춘다면 단순 계산은 약 36.6%까지 떨어집니다. 실제 자동증명에서도 개별 보조정리는 잘 풀면서 전체 전략을 이어 붙이지 못하는 문제가 나타납니다.
연구를 읽는 두 가지 질문
연구 질문과 확인 버전
2025년 8월 21일 공개된 v1은 이론컴퓨터과학 문제를 매개변수화해 규모가 커질수록 자동증명기가 어떻게 무너지는지 묻습니다. 이 글은 arXiv HTML과 PDF의 v1만 확인했으며 후속 개정이나 모델 서비스 변화는 별도입니다. [Zhang et al., arXiv:2508.15878 v1]
방법
연구진은 Busy Beaver 계산과 Mixed Boolean Arithmetic(MBA) 단순화에서 자연어 설명과 Lean 4 정리를 짝지어 자동으로 난이도를 확장하는 과제를 만들었습니다. 작은 단위 보조정리와 전체 정리를 모두 평가하고, 여러 번 생성했을 때 하나라도 통과하는 Pass@16 등을 보고했습니다. 형식 커널이 최종 코드를 검사합니다. [Lean Meets Theoretical Computer Science]
핵심 결과
DeepSeek-Prover-V2-671B의 Pass@16은 Busy Beaver에서 57.5%, MBA에서 12%로 과제군 차이가 컸습니다. OpenAI o4-mini는 개별 단계에서 98.88%에 이르는 성공을 보였지만 전체 증명에서는 여전히 실패가 누적됐습니다. 높은 로컬 성공률이 장기 의존성과 전역 증명 계획을 보장하지 않는다는 정량적 사례입니다. [Zhang et al. (2025), evaluation]
학술적 의미와 한계
고정 문제 목록의 정답률만 보면 기억이나 템플릿 적합성을 분리하기 어렵습니다. 매개변수화한 문제는 길이와 구조를 체계적으로 바꾸어 확장성을 시험합니다. 다만 두 문제군과 Lean 라이브러리에 집중한 사전논문이므로 수학 전 영역이나 다른 증명기에 일반화할 수 없고, 개별 단계 정의도 벤치마크 설계에 상대적입니다. [arXiv v1 results and discussion]
검수할 때 확인할 점
성능표에는 문제 단위 전체 성공률, 보조정리 성공률, 시도 횟수와 계산비용을 같은 행에 놓는 것이 좋습니다. Pass@16은 한 번의 답변 품질이 아니라 여러 후보 중 하나가 통과할 가능성이므로 Pass@1과 직접 바꾸어 읽으면 안 됩니다. 단계별 문제를 원래 전체 증명에서 분리했을 때 전제가 추가되거나 목표가 쉬워졌는지도 확인해야 합니다. 장기 증명 능력은 의존 그래프를 유지한 상태에서 커널이 전체 파일을 검사했을 때 평가해야 합니다. 또한 제목의 질문에 답할 때 연구가 직접 관찰한 결과, 저자가 제안한 해석, LTCT가 제시한 교육 적용을 서로 다른 색으로 표시해야 합니다. 표본과 과제 밖의 주장에는 ‘추가 검증 필요’ 꼬리표를 붙이고, 본문 수치와 도식의 방향이 일치하는지 마지막으로 대조합니다. [LTCT 비판적 읽기 제안]
열 단계 중 한 단계가 비면
LTCT 예시입니다. 1~10번 보조정리 가운데 1~6번과 8~10번을 모두 증명해도 7번이 8번의 전제라면 최종 정리는 닫히지 않습니다.
각 단계 정답률 평균과 전체 증명 성공률을 함께 보고해야 합니다. 실패 지점 뒤의 단계가 개별적으로 맞다는 사실은 전체 의존 사슬을 복구하지 않습니다.
어디까지 말할 수 있을까요?
- 확인본은 2025-08-21 arXiv v1 사전논문이며 동료심사·후속 개정 상태와 구분해야 합니다.
- Pass@16은 16번의 생성 기회를 주는 지표라 단일 시도 성능이나 비용과 같지 않습니다.
원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]
교육 현장과 연결해 보면
AI 평가에서는 보조정리 단위 정확도, 의존관계 보존, 전체 커널 통과를 별도 지표로 기록할 수 있습니다.
논리 수업은 증명 그래프에서 병목 보조정리를 찾고 ‘부분 점수’와 ‘완결성’을 분리해 설명하게 할 수 있습니다.
개별 단계 정확도가 98.88%라면 전체 증명도 98.88% 성공한다고 볼 수 있을까요?
생각을 비교할 해설 펼치기
아닙니다. 단계 오류가 누적되고 앞 단계의 실패가 뒤 의존관계를 끊습니다. 증명 길이와 오류 상관, 전역 계획을 포함한 전체 커널 통과율을 따로 봐야 합니다.
원문과 출처 정보
한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.
린과 이론컴퓨터과학의 만남: 형식-비형식 쌍 자동정리증명 과제의 확장 가능한 합성 (Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs)
Terry Jingchen Zhang; Wenyuan Jiang; Rongchuan Liu; Yisong Wang; Junran Yang; Ning Wang; Nicole Ni; Yinya Huang; Mrinmaya Sachan (2025). arXiv.
- 자료 성격
- public preprint
- 읽은 버전
- arXiv:2508.15878 v1, 2025-08-21
- 확인 범위
- v1 HTML 전문과 PDF의 생성 방법, 두 과제군, 모델별 표, 한계 확인
- 원문 확인일
이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준