TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

이 논문은 기존 수학 라이브러리 (MathLib) 에 의존하는 자동 정리 증명 시스템이 표준 라이브러리를 사용하지 않고 기본 개념부터 구축된 테오도르 타오의 분석학 기반 벤치마크 'TaoBench'에서 성능이 약 26% 급감한다는 사실을 규명하여, 현재 모델들의 주요 한계가 작업 난이도가 아닌 정의 프레임워크 간 일반화 부재에 있음을 보여줍니다.

핵심

이 논문은 "인공지능 수학 천재들은 정말로 수학을 잘할까, 아니면 그냥 특정 교재만 외운 것일까?" 라는 아주 날카로운 질문에서 시작합니다.

논문 제목인 TAOBENCH를 통해 저자들은 인공지능 (LLM) 이 수학 문제를 풀 때, 우리가 흔히 쓰는 '표준 교과서 (MathLib)'만 보고 훈련받았을 뿐, 실제 연구 현장처럼 새로운 방식으로 수학을 정의하면 얼마나 무너지는지 실험했습니다.

이 복잡한 내용을 세상에서 가장 쉬운 비유로 설명해 드릴게요.

---

🍔 비유: "햄버거 가게와 오마카세 요리사"

1. 상황 설정: 두 가지 메뉴

• MathLib (표준 프레임워크): 전 세계 모든 햄버거 가게에서 쓰는 표준 레시피입니다. "패티는 150g, 소스는 케첩 2 스푼"처럼 정해진 규칙이 있습니다. 현재 AI 수학 모델들은 이 레시피만 보고 훈련받았습니다.
• Tao's Analysis (새로운 프레임워크): 세계적인 요리사 (테런스 타오) 가 만든 새로운 오마카세 메뉴입니다. 여기서 패티는 '고기'가 아니라 '두부'로 만들고, 소스는 '케첩' 대신 '간장'을 씁니다. 수학적으로 의미는 똑같지만, **재료와 조리법 (정의)**이 완전히 다릅니다.

2. 실험 내용: AI 의 실력 테스트

저자들은 AI 에게 두 가지 미션을 주었습니다.

1. 미션 A (MathLib): "표준 햄버거 레시피로 햄버거를 만들어줘."
2. 미션 B (TaoBench): "테런스 타오의 새로운 레시피 (두부 패티, 간장 소스) 로 똑같은 맛의 햄버거를 만들어줘."

3. 놀라운 결과: "레시피만 바꿨는데 AI 가 당황했다!"

• 미션 A (표준): AI 는 아주 잘했습니다. 70% 이상 성공했습니다.
• 미션 B (새로운): AI 는 약 26% 나 떨어졌습니다. (성공률이 70% 에서 44% 로 뚝 떨어짐)

왜 그럴까요?
AI 는 "햄버거를 만드는 법"을 배운 게 아니라, **"표준 레시피를 암기하는 법"**을 배웠기 때문입니다. 재료가 조금만 바뀌어도 (패티가 두부가 되면), AI 는 "아, 이건 내가 배운 햄버거가 아니야!"라고 생각하며 당황해서 실패합니다.

---

🔍 핵심 발견: "문제의 난이도가 아니라, '정의'의 차이"

논문의 가장 중요한 결론은 이것입니다.

"AI 가 못 푼 이유는 수학 문제가 너무 어려워서가 아니라, 수학을 설명하는 '방식 (정의)'이 익숙하지 않아서다."

• 상황: 같은 '삼각형' 문제를 풀더라도, 한 교재는 "세 변의 길이를 합한 것"으로 정의하고, 다른 교재는 "세 각의 합"으로 정의할 수 있습니다. 수학적으로 같은 뜻이지만, AI 가 훈련받은 방식과 다르면 AI 는 길을 잃습니다.
• 비유: 마치 "집"을 설명할 때, 한 사람은 "벽과 지붕이 있는 공간"이라고 하고, 다른 사람은 "네모난 상자"라고 했을 때, AI 가 "벽"이라는 단어를 못 알아듣고 "상자"라는 단어로만 생각하다 보니 집을 짓는 법을 잊어버린 것과 같습니다.

---

🛠️ 연구팀이 한 일: "공정한 시험지 만들기"

이 연구를 위해 저자들은 매우 정교한 장비를 만들었습니다.

1. 자동 추출기 (Agentic Pipeline): 테런스 타오의 교재에서 문제를 뽑아낼 때, AI 가 혼자서 헷갈리지 않도록 필요한 모든 정의와 규칙을 딱딱 잘라내어 하나의 파일로 만들었습니다. (AI 가 "아, 이거 정의가 뭐였지?" 하고 헤매지 않게요.)
2. 쌍둥이 문제 (Paired Problems): 같은 문제를 두 가지 버전으로 만들었습니다.
   • TAOBENCH: 타오의 새로운 레시피 버전.
   • TAOBENCHMATHLIB: 표준 햄버거 레시피 버전.
   • 이렇게 하면 "문제가 어려워서 못 푼 건지, 레시피가 달라서 못 푼 건지" 정확히 구별할 수 있습니다.

---

💡 이 연구가 우리에게 주는 교훈

지금까지 AI 수학 모델들은 "표준 교재"에서만 시험을 봐서 성적이 좋았습니다. 하지만 실제 수학 연구나 새로운 발견은 표준 교재에 없는 새로운 정의를 만들어가는 과정입니다.

• 현재의 문제: AI 는 "익숙한 환경"에서는 천재처럼 보이지만, "새로운 환경"에서는 초보자가 됩니다.
• 미래의 방향: 우리는 AI 가 단순히 레시피를 외우는 게 아니라, **어떤 재료 (정의) 가 주어지더라도 그 맛 (수학적 의미) 을 찾아낼 수 있는 진정한 '요리사'**로 만들어야 합니다.

한 줄 요약:

"지금의 AI 수학 천재들은 '표준 교재'라는 특정 언어만 할 줄 아는 통역사일 뿐, 새로운 언어 (새로운 수학 정의) 가 주어지면 당황하는 초보생일 수 있습니다. 우리는 AI 가 어떤 언어에서도 수학을 이해할 수 있도록 훈련시켜야 합니다."

기술 요약

1. 연구 배경 및 문제 정의 (Problem)

• 현재의 한계: 자동 정리 증명 (ATP) 을 위한 대규모 언어 모델 (LLM) 은 주로 MathLib(Lean 4 의 표준 수학 라이브러리) 에서 형식화된 문제들로 훈련 및 평가됩니다. 이로 인해 모델들은 MathLib 의 정의 체계 (definitional framework) 에 과도하게 편향되어 있습니다.
• 실제 연구 환경과의 괴리: 실제 수학 연구, 특히 탐구적 (exploratory) 인 연구나 프로토타이핑 과정에서는 표준 라이브러리를 사용하지 않고, 문제 해결을 위해 맞춤형 (bespoke) 정의와 구성을从零 (scratch) 으로 구축하는 경우가 많습니다.
• 핵심 질문: 현재 최첨단 ATP 모델들이 MathLib 과 다른 새로운 정의 체계 (예: Terence Tao 의 분석학 교재 형식화) 로 전환되었을 때, 그 성능이 얼마나 일반화 (generalize) 될 수 있는가?
• 가정: 기존 벤치마크는 모델의 수학적 추론 능력을 평가하는 것이 아니라, 특정 라이브러리 (MathLib) 에 대한 친숙도를 평가하고 있을 가능성이 높음.

2. 방법론 (Methodology)

2.1. TAOBENCH 벤치마크 구축

• 데이터 소스: Terence Tao 의 Analysis I 교재를 Lean 4 로 형식화한 코드베이스 (150 개의 연습문제) 를 기반으로 합니다.
• 특징:
  • Zero-shot 정의: MathLib 의 표준 정의를 재사용하지 않고, 집합, 자연수, 실수 등 핵심 개념을 처음부터 구축 (from-scratch) 합니다.
  • 맞춤형 정의: 집합을 α → Prop (MathLib 방식) 대신 커스텀 인덕티브 타입이나 구조체로 정의하는 등 MathLib 과는 완전히 다른 정의 체계를 사용합니다.
• 자동화 파이프라인 (Agentic Pipeline):
  • 각 문제별로 컴파일 가능한 자체 독립 환경 (self-contained local environment) 을 자동으로 추출합니다.
  • JiXia 도구: 정적 분석을 통해 문제의 의존성 (참조, 정의, 정리) 을 재귀적으로 추출합니다.
  • 파일 조회 및 컴파일 에이전트: 추출된 의존성을 바탕으로 Lean 소스 코드를 복사하고, 컴파일 오류를 수정하여 최종적으로 독립적으로 실행 가능한 Lean 파일을 생성합니다. 이는 문맥 길이 제한과 컴파일 실패를 방지하기 위함입니다.

2.2. TAOBENCHMATHLIB (대조군) 구축

• 목적: 문제의 난이도 변화가 아닌 정의 체계의 차이만 isolate 하기 위해 설계되었습니다.
• 변환 프로세스:
  1. Rewriting: GPT-5.1 을 활용하여 Tao 의 정의 체계를 MathLib 의 표준 정의 (예: Set, Tendsto 등) 로 변환합니다. 웹 검색을 통해 MathLib 의 정확한 사용법을 참조합니다.
  2. Equivalence Checking: JiXia 도구를 사용하여 원본 (Tao) 과 변환본 (MathLib) 의 증명 목표 상태 (proof state) 를 추출하고, 두 식이 수학적으로 동등한지 LLM 에게 검증시킵니다.
  3. Expert Verification: 수학 및 Lean 전문가가 150 개 문제의 변환 정확도와 동등성을 수동으로 검증하고 수정합니다.

2.3. 실험 설정

• 평가 모델: DeepSeek-Prover-V2, Goedel-Prover-V2, Kimina-Prover 등 최신 ATP 모델과 GPT-5.1, Gemini 3 Pro 등 프런티어 기초 모델.
• 지표: Pass@128 (128 번의 시도 중 성공한 비율).

3. 주요 결과 (Key Results)

• 성능 저하 (Performance Gap):

  • 모든 평가된 ATP 모델은 MathLib 버전 (TAOBENCHMATHLIB) 에서 높은 성능 (대부분 65%~70% 이상) 을 보였습니다.
  • 반면, Tao 의 정의 체계 버전 (TAOBENCH) 에서 성능이 평균 약 26% 포인트 급격히 하락했습니다. (예: Goedel-Prover-V2-32B 는 MathLib 에서 72.67% → Tao 에서 49.33%)
  • 이는 모델이 MathLib 정의 체계에 특화되어 있어, 수학적으로 동일한 문제라도 정의가 다르면 해결하지 못함을 의미합니다.

• 문맥 길이 (Context Length) 의 영향:

  • 문제 해결에 필요한 로컬 정의 (local definitions) 의 수가 증가할수록 Tao 버전의 성능은 급격히 떨어집니다.
  • 정의가 10 개 이상 포함될 경우, 평균 성공률은 67% 에서 6.37% 까지 추락했습니다.
  • 반면 MathLib 버전은 정의 수가 늘어나도 성능 저하가 완만했습니다. 이는 모델이 훈련 데이터 (MathLib) 와 다른 새로운 정의를 문맥에서 효과적으로 통합하고 추론하는 데 어려움을 겪고 있음을 보여줍니다.

• 프런티어 모델 vs 전용 ATP 모델:

  • 수학 증명에 특화되지 않은 프런티어 모델 (GPT-5.1 등) 은 MathLib 버전에서는 ATP 모델보다 성능이 낮았으나, Tao 버전에서는 오히려 더 나은 성능을 보이거나 유사한 수준을 유지했습니다.
  • 이는 프런티어 모델이 문맥 내 정보 (in-context information) 를 활용하는 능력이 뛰어나기 때문이며, ATP 모델의 약점이 "수학적 추론 능력 부족"이 아니라 "새로운 정의 체계에 대한 일반화 실패"임을 시사합니다.

• 케이스 스터디:

  • Nat.backwards_induction: Tao 버전에서는 수학적 귀납법과 순서 정리를 처음부터 재구성해야 하므로 실패율이 높았으나, MathLib 버전에서는 표준 정리를 활용해 성공했습니다.
  • Convergesto.squeeze: Tao 버전의 명시적 $\epsilon-\delta$ 정의는 모델이 잘 처리했으나, MathLib 의 필터 (filter) 기반 추상화 (Tendsto) 는 오히려 모델이 추론을 어렵게 여겼습니다. 이는 모델이 특정 정의 체계에 과도하게 의존하고 있음을 보여줍니다.

4. 주요 기여 (Key Contributions)

1. TAOBENCH 제안: MathLib 을 벗어난 새로운 정의 체계로의 일반화 능력을 측정하는 최초의 Lean 벤치마크를 제시했습니다.
2. TAOBENCHMATHLIB 제공: 동일한 문제를 MathLib 정의 체계로 변환한 쌍 (paired) 데이터를 제공하여, 문제 난이도와 정의 체계의 영향을 분리하여 평가할 수 있는 기반을 마련했습니다.
3. 자동화 파이프라인 개발: 대규모 형식화 프로젝트 (교재) 에서 각 문제별로 컴파일 가능한 독립 환경과 수학적으로 동등한 MathLib 버전을 자동으로 생성하는 에이전트 파이프라인을 구축했습니다. 이는 향후 고품질 훈련 데이터 생성에 활용 가능합니다.

5. 의의 및 결론 (Significance)

• 현실적 장벽의 노출: 현재 공개된 최첨단 ATP 모델들은 MathLib 과 같은 특정 정의 체계에 "과적합 (overfitting)"되어 있어, 실제 수학 연구에서 흔히 발생하는 새로운 정의 체계나 프로토타이핑 환경에서는 신뢰할 수 있게 작동하지 못합니다.
• 벤치마크의 한계 지적: 기존 벤치마크는 모델의 진정한 수학적 능력을 평가하기보다, 특정 라이브러리에 대한 암기나 적응 능력을 평가하고 있을 가능성이 높습니다.
• 미래 방향: 실제 연구 수학 (Research Mathematics) 에 ATP 를 적용하기 위해서는 모델이 익숙하지 않은 정의 체계에서도 유연하게 추론할 수 있도록 훈련 데이터와 평가 기준을 다변화해야 합니다. TAOBENCH 는 이러한 방향성을 제시하는 구체적인 테스트베드 역할을 합니다.

요약하자면, 이 논문은 "자동 정리 증명 LLM 들은 MathLib 이라는 특정 정의 체계 밖에서는 수학적 능력을 발휘하지 못한다" 는 사실을 실증적으로 증명하며, 향후 모델 개발이 단순한 문제 해결 능력 향상을 넘어 정의 체계의 일반화 (generalization across definitional frameworks) 에 초점을 맞춰야 함을 강조합니다.