고등학교 경시문제를 잘 푸는 증명 인공지능(AI)가 대학원 해석학도 잘 풀까?

2026년 MA-ProofBench는 해석학 200문제를 학부·박사자격 수준으로 나눠 평가했고, 최고 일반 모델도 Pass@8 16%와 5%에 머물러 분야·난도별 검증의 필요성을 보였습니다.

연구 해설중급 · 약 9분원문: 학술지·학회 논문 · 2026

해설·교육용 구성: LTCT 편집부 · 게시 2026.09.13 · 최종 수정 2026.09.13

자동증명 벤치마크가 대수와 초등 정수론에 몰려 있다면 높은 점수는 ‘형식 수학 전체’의 능력을 뜻하지 않습니다. 연속성, 측도, 복소해석과 함수해석은 다른 라이브러리 지식과 긴 보조정리 계획을 요구합니다.

학술 자료의 내용

연구를 읽는 두 가지 질문

Pu 등은 MA-ProofBench를 수학 해석학 전용 형식 증명 벤치마크로 제안했습니다. 학부 수준 100문제와 박사자격시험 수준 100문제, 모두 6개 핵심 주제와 27개 하위 범주를 포함합니다. [1]

문제는 교과서와 공개 자격시험에서 모으고, 사람이 주도하며 언어모델을 보조로 쓴 형식화 뒤 독립 전문가가 원문 의미와 Lean 명제를 검토했습니다. 형식 문법이 맞는 것과 원래 수학 질문을 보존하는 것을 분리한 절차입니다. [1]

논문이 평가한 일반 추론 모델 중 최고는 Pass@8 기준 학부 수준 16%, 박사 수준 5%였습니다. 가장 강한 전용 정리증명기도 각각 6.86%, 0.44%였다고 보고합니다. Mathlib 항목 환각과 불완전 증명이 주요 실패 유형이었습니다. [1]

결과는 2026년 6월 11일 공개본의 특정 모델·프롬프트·시도 수·Mathlib 버전에 관한 것입니다. Pass@8은 최대 여덟 시도 중 하나가 성공하는지 보므로 1회 성공률과 다르고, 미래 모델의 현재 성능으로 읽을 수 없습니다. [1]

그림으로 생각하기

벤치마크 A가 초등 대수 100문제이고 B가 측도론·함수해석 100문제라면 둘 다 20문제를 풀어도 요구된 지식과 증명 길이가 다릅니다. 총점만으로 ‘동일한 수학 능력’이라고 할 수 없습니다.

Pass@8 성공은 여덟 후보 가운데 하나가 검증됐다는 뜻입니다. 실제 서비스가 한 번만 답하거나 계산 예산을 제한하면 체감 성능이 다릅니다. 문제 수준, 시도 수, 시간과 검증기를 함께 보고해야 합니다.

LTCT의 AI 벤치마크도 관계 읽기·추론·표현 전이의 층과 도메인을 교차표로 공개하고, 전체 평균 옆에 최저 범주와 실패 유형을 표시할 수 있습니다.

원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]

배운 내용을 수업에 적용하기

수학 AI의 평가표를 문제 분야와 요구되는 선행 개념별로 나눕니다. 학생은 경시문제에서의 성공과 해석학 문제에서의 성공이 같은 능력을 얼마나 다루는지 실제 문제의 조건을 비교합니다.

실패 기록에서 정의 사용, 보조정리 선택, 형식화 가운데 막힌 단계를 표시합니다. 교사는 한 분야의 총점을 모든 수학 수준의 성과로 확대하지 않고 평가 범위를 명시하게 합니다.

한 번 더 생각하기

생각을 비교할 해설 펼치기

Pass@8은 문제마다 최대 여덟 번 생성했을 때 하나 이상 성공한 비율이므로 단일 시도 조건과 계산 예산이 다릅니다.

한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.

이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준