💻 computer science

Lean-GAP: A Dataset of Formalized Graduate Algebra Problems

이 논문은 Dummit과 Foote의 교재에서 추출한 430개의 정형화된 대학원 수준 대수학 문제들로 구성된 Lean-GAP 데이터셋과, 이들의 생성을 위한 확장 가능한 파이프라인, 그리고 비정형 수학을 Lean 4 증명 보조기로 번역하는 과정에서 발생하는 과제와 병목 현상에 대한 분석을 소개한다.

원저자: Seewoo Lee, Byung-Hak Hwang, Hyojae Lim, Jihoon Hyun, Ilkyoo Choi, Yeachan Park, Jineon Baek, Hyukpyo Hong, Keewoo Lee, Jaeseong Heo, Hyungryul Baik, Chul-hee Lee, Kyu-Hwan Lee

게시일 2026-06-03

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Seewoo Lee, Byung-Hak Hwang, Hyojae Lim, Jihoon Hyun, Ilkyoo Choi, Yeachan Park, Jineon Baek, Hyukpyo Hong, Keewoo Lee, Jaeseong Heo, Hyungryul Baik, Chul-hee Lee, Kyu-Hwan Lee

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

개요: 두 언어 사이의 가교

당신이 "인간 수학"(비형식적 언어, 도표, 표준 표기법)으로 쓰인 방대한 고급 수학 교과서 도서관을 가지고 있다고 상상해 보세요. 이제 이 책들에 담긴 모든 문제를 "로봇 수학"(Lean 4라고 불리는 엄격한 컴퓨터 판독 가능 언어)으로 번역하고 싶다고 가정해 봅시다.

왜 그럴까요? 컴퓨터는 수학 문제를 푸는 데 매우 능숙해지고 있지만, 문제가 반드시 그들의 엄격한 언어로 작성되어야만 작동할 수 있기 때문입니다. 현재 우리는 큰 격차를 마주하고 있습니다. 즉, 엄청난 양의 '인간 수학'은 존재하지만, 표준 대학원 수준의 과정을 위한 '로봇 수학'은 매우 적다는 것입니다.

이 논문의 저자들은 이 격차를 메우는 다리를 건설했습니다. 그들은 유명한 교재(Abstract Algebra, Dummit 및 Foote 저)에 나오는 430개의 형식화된 대수학 문제들을 포함하는 LEAN-GAP이라는 데이터셋을 만들었습니다.

과정: 3단계 조립 라인

연구팀은 인간의 수학 문제를 로봇의 수학으로 바꾸는 "공장"을 구축했습니다. 그 과정은 다음과 같습니다.

스캐너 (PDF에서 LaTeX로):
먼저, 그들은 교과서의 스캔된 PDF(단순히 텍теxt의 이미지 형태)를 가져와 소프트웨어를 사용하여 디지털 텍스트 코드(LaTeX)로 변환했습니다. 이것은 마치 하이테크 스캐너를 사용하여 손으로 쓴 편지를 타이핑된 문서로 바꾸는 것과 같습니다.
번역가 (자동 형식화):
다음으로, 강력한 AI 모델(고급 챗봇 등)을 사용하여 그 타이핑된 텍스트를 Lean 4 코드로 번역했습니다. 이는 마치 번역가에게 일상적인 대화를 법률 계약서로 바꾸라고 요청하는 것과 같습니다. AI는 적절한 단어와 구조를 추측하려고 시도합니다.
품질 관리 (검증):
이 부분이 가장 중요하고 어려운 단계입니다. AI가 생성한 코드가 컴퓨터가 읽을 수 있다고 해서(컴파일이 된다고 해서), AI가 실제로 수학을 이해했다는 뜻은 아닙니다.

비유: AI가 문법적으로는 완벽하지만 틀린 내용을 말하는 문장을 썼다고 상상해 보세요 (예: "하늘은 파랗다" 대신 "하늘은 초록색이다"라고 말함). 컴퓨터는 그 문장을 받아들이겠지만, 의미는 틀린 것입니다.
이 때문에 저자들은 사람이 여기서 핵심적인 역할을 수행해야 한다는 것을 발견했습니다. 박사 학위를 가진 수학자들과 상급 학생들은 "로봇 수학"이 "인간 수학"과 정확히 동일한 의미를 갖는지 확인하기 위해 수많은 시간을 보냈습니다.

발견한 점: AI는 빠르지만, 인간은 필수적이다

연구팀은 어떤 AI 모델이 최고의 번역가인지 확인하기 위해 여러 가지 다른 AI 모델을 테스트했습니다. 주요 발견 사항은 다음과 같습니다.

"컴파일러"의 함정: 많은 AI 모델이 오류 없이 컴퓨터가 수용할 수 있는 코드를 작성할 수 있었습니다. 하지만 인간이 의미를 확인했을 때, AI가 핵심 세부 사항을 놓치거나, 논리를 뒤집거나, 존재하지 않는 정의를 지어내는 경우가 많았습니다.
"루프(Loop)"의 이점: 시도하고, 실패하고, 에러 메시지를 확인한 뒤 다시 시도할 수 있도록 허용된 하나의 AI 시스템(Codex)이 다른 모델들보다 훨씬 더 좋은 성능을 보였습니다. 이는 단순히 한 번 추측하는 것이 아니라, 정답을 얻을 때까지 수학 문제를 계속 연습하는 학생과 같습니다.
"인간 참여(Human-in-the-Loop)"의 현실: 가장 뛰어난 AI조차 혼자서는 일을 해낼 수 없었습니다. 이 프로젝트에서 가장 시간이 많이 걸린 부분은 코드를 작성하는 것이 아니라, 코드가 실제로 올려 맞는지 확인하기 위해 인간이 검토하는 작업이었습니다.

과제: 이론과 실제의 충돌

이 논문은 번역하기 매우 어려웠던 세 가지 특정 유형의 문제를 강조합니다.

기하학 문제: 일부 문제는 컴퍼스와 자를 이용한 도형 그리기를 포함합니다. 컴퓨터에게 인간의 직관과 일치하는 방식으로 "그림"이 무엇인지 가르치는 것은 매우 어렵습니다.
"답을 찾아라" 문제: 어떤 질문들은 가능한 모든 답을 나열하라고 요구합니다. AI는 가끔 문제를 해결하는 과정 대신 답을 그냥 사실로서 적어버리곤 합니다. 연구팀은 컴퓨터가 단순히 정답지를 읽는 것이 아니라 실제로 퍼즐을 풀 수 있도록 이 문제들을 재구성해야 했습니다.
누락된 사전 단어: 때때로 교과서에서 사용하는 특정 수학 개념이 아직 컴퓨터의 라이브러리(Mathlib)에 존재하지 않을 때가 있습니다. AI는 그 이름을 추측하려고 시도하지만, 컴퓨터는 그 이름이 무엇을 의미하는지 알지 못합니다. 인간은 처음부터 이러한 정의들을 직접 구축해야 했습니다.

결론: 팀워크

이 논문은 AI가 수학을 번역하는 능력이 향려지고 있지만, 아직 AI가 모든 일을 혼자서 다 할 수 있다고 믿고 전적으로 의존할 수는 없다고 결론짓습니다.

건물을 짓는 것에 비유해 보겠습니다:

AI는 벽돌을 매우 빠르게 쌓을 수 있는 로봇 팔과 같습니다.
인간은 벽이 똑바른지, 집이 안전한지 확인하는 건축가이자 검사관입니다.

저자들은 AI가 타이핑과 초기 번역이라는 힘든 일을 수행하지만, 미세한 오류를 잡아내기 위해 인간이 여전히 과정에 참여하는 시스템을 구축했습니다. 그들은 이 데이터셋(LEAN-GAP)을 공유함으로써 미래의 AI 시스템이 더 나은 "수학 학생"이 되도록 훈련하는 데 도움을 주고, 궁극적으로 AI가 까다로운 경시 대회 문제만 푸는 것이 아니라 표준 교과서로부터 학습할 수 있도록 돕기를 희망합니다.

기술 요약: LEAN-GAP: 정형화된 대학원 대수학 문제 데이터셋

문제 정의
자동 추론 및 대규모 언어 모델(LLM)의 상당한 발전에도 불구하고, 비형식적 수학 지식과 Lean 4와 같은 증명 보조기(proof assistant) 내의 형식적 대응물 사이에는 상당한 격차가 존재한다. 최근의 노력들이 경시 대회 스타일의 문제나 매우 전문화된 정리들을 성공적으로 정형화해 왔으나, 표준적인 대학원 수준의 자료를 다루는 대표적이고 구조화된 데이터셋은 부족한 실정이다. 이러한 기초 커리큘럼 데이터의 부재는 자동 추론 시스템의 발전을 저해하는데, 이는 해당 시스템들이 체계적인 개념 전개가 있는 표준 교과서 대신 "도전적인 문제들"에만 학습되는 경우가 많기 때문이다. 또한, 자동 정형화(autoformalization)가 진전되었음에도 불구하고, 생성된 형식적 문장이 의도된 의미를 충실히 포착하고 있는지 검증하는 것은 여전히 해결되지 않은 핵심적인 병목 현상으로 남아 있다.

방법론
저자들은 Dummit과 Foote의 교과서 Abstract Algebra에서 추출한 430개의 정형화된 연습문제로 구성된 LEAN-GAP(Lean-Graduate Algebra Problems) 데이터셋을 제시한다. 이 프로젝트는 확장 가능한 3단계 파이프라인을 채택한다:

PDF-to-LATEX 전처리: 스캔된 교과서 PDF 페이지를 이미지로 렌더링하고, 불필요한 요소를 제거하기 위해 크롭한 후, Mathpix Convert API를 통해 초기 LATEX 전사본을 생성한다.
LATEX-to-Lean 자동 정형화: 다양한 LLM을 사용하는 프롬프트 기반 접근 방식을 사용하여 LATEX 문장을 Lean 4 코드로 변환한다. 프롬프트는 일관된 명명 규칙(예: DF_{sec}_{subsec}_{exercise_num})과 Mathlib과의 호환성, 그리고 증명을 위한 sorry 플레이스홀더 포함을 강제한다. 저자들은 여섯 가지 시스템을 평가하였다: 다섯 가지 싱글샷 모델(GPT-5, Gemma4-31B, Goedel-Formalizer-V2-32B, Qwen3.6-35B-A3B, DeepSeek-R1-Distill-Qwen-32B)과 하나의 반복적 에이전트 루프(Codex).
비형식적-형식적 대응의 검증: 컴파일 성공이 의미론적 정확성을 보장하지 않는다는 점을 인식하여, 저자들은 엄격한 인간 참여형(human-in-the-loop) 검증 워크플フロー를 구현하였다.
- 기여자 단계: 기여자가 연습문제를 독립적인 정리 문장으로 다시 작성하고, 이를 Lean으로 정형화한 뒤 풀 리퀘스트(PR)를 제출한다.
- 자동 체크: GitHub CI가 고정된 Mathlib 리비전에 대해 Lean 코드가 정교화(elaborate)되는지 확인한다.
- 유지 관리자 검토: 독립적인 유지 관리자가 의미론적 검토를 수행하여, Lean 선언이 비형식적 문장의 수학적 내용을 제대로 포착했는지 확인한다.
- AI 보조 수정: Claude Opus 4.7 및 Aristotle과 같은 도구들을 "제2 독자"로 활용하여, 인간 검토자가 처음에 간과할 수 있는 양화사 반전(flipped quantifiers)이나 누락된 제약 조건(예: $n \ge 2$ )과 같은 미묘한 의미론적 오류를 탐지한다.

주요 기여

LEAN-GAP 데이터셋: 군론(group theory), 환론(ring theory), 체론(field theory), 갈로아 이론(Galois theory)을 다루며 주제와 난이도별로 구성된 430개의 정형화된 대학원 대수학 연습문제 코퍼스.
체계적인 정형화 파이프라인: 교과서 연습문제를 형식적 문장으로 변환하는 재현 가능한 방법론을 제시하며, 검증 단계에서 인간의 감독이 필수적임을 강조한다.
정형화 과제의 분석: 다음과 같은 반복되는 병목 현상을 포함한 상세한 분석을 제공한다:
- 기하학적 논증: 자와 컴퍼스를 이용한 작도 관련 연습문제는 Mathlib 내의 견고한 기하학적 인프라 부족으로 인해 정형화가 어렵다.
- 답안 포함 정형화: 해의 목록을 나열해야 하는 문제는 주어진 답을 검증하는 것과 답을 발견하는 것을 구분하는 데 어려움을 준다.
- 정의 누락: 아직 Mathlib에 없는 개념(예: 특정 프로베니우스 군)을 요구하는 연습문제는 교과서의 의도에 맞게 신중하게 구축되어야 하는 커스텀 정의를 필요로 한다.
- 미묘한 모호성: 비형식적 문장은 종종 암묵적인 제약 조건(예: $n \ge 2$ )을 포함하며, 이를 누락할 경우 Lean의 논리(예: 자연수 뺄셈 동작 때문)에서 해당 형식적 문장이 거짓이 될 수 있다.

결과
저자들은 1,966개의 전체 연습문제에 대해 서로 다른 자동 정형화 모델의 성능을 평가하였다:

정교화 성공률(Elaboration Success): Codex(반복적 에이전트 루프)는 95.5%의 가장 높은 성공률을 달enc하여, 싱글샷 모델들을 크게 앞질렀다. GPT-5는 44.1%의 연습문제를 완전히 정교화하며 싱글샷 모델 중 선두를 차지했다.
의미론적 충실도(Semantic Fidelity): 구문론적 성공(정교화)은 필요조건이지만 충분조건은 아니다. LLM 기반 의미론적 판정기(Claude Opus 4.7)가 문장의 충실도를 평가했다. GPT-5는 평균 3.45/5점을 기록했으며, 출력물의 45.1%가 "충실하다"고 판단되었다. 반면, DeepSeek-R1은 1.15/5점으로 현저히 낮았으며, 선언을 생성하지 못하거나 공허한 문장을 생성하는 경우가 많았다.
모델 상호 보완성: 모델들은 높은 불일치를 보였다. 모든 시스템이 해결한 문제는 단 7개였던 반이, 정확히 하나의 시스템만이 해결한 문제는 654개였다. 이는 모델들을 병렬로 실행하는 것의 가치를 강조한다.
인간 검증의 필요성: 검증 단계가 가장 노동 집약적인 것으로 드러났다. 높은 정교화율에도 불구하고, 많은 문장이 잘못된 군 이름이나 양화사 반전과 같은 의미론적 오류를 포함하고 있어 전문가의 개입이 필요했다.

의의
본 논문은 LEAN-GAP이 경쟁 대회 벤치마크를 넘어 표준 대학원 커리큘럼을 다룸으로써 AI 시스템을 위한 학습 데이터의 결정적 격차를 해결한다고 주장한다. 이 연구는 LLM이 수학 텍스트의 초기 번역을 자동화할 수는 있지만, 지속적인 의미론적 격차로 인해 표준 자료를 위한 엔드 투 엔드 자동 정형화 도구로서 아직 기능할 수 없음을 보여준다. 저자들은 미래의 정형화가 생산적인 인간-AI 협업에 달려 있다고 주장한다. 즉, AI는 미묘한 오류와 명시되지 않은 가설을 식별하는 "제2 독자" 역할을 수행하고, 인간 수학자는 의미론적 충실도를 위한 감독을 제공하는 것이다. 이 접근 방식은 표준 커리큘럼을 마스터할 수 있는 "AI 수학 학생" 개발을 위한 토대가 될 수 있는, 표준 수학 교육 자료의 정형화를 확장하기 위한 템플릿을 제공한다.