기술 요약: MathAtlas: 야생 환경에서의 자동 형식화를 위한 벤치마크

문제 제기

현재의 자동 형식화 벤치마크는 주로 선결 과제가 제한적이고 Mathlib 과 같은 라이브러리에 이미 형식화된 경우가 많은 올림피아드나 학부 수준의 수학 등 더 단순한 도메인에 초점을 맞추고 있습니다. 그러나 대학원 수준 및 연구 수학은 아직 충분히 탐구되지 않았습니다. 이러한 고급 도메인에서 자동 형식화는 다음과 같은 이유로 훨씬 더 복잡합니다:

1. 선결 과제의 깊이: 고급 수학은 광범위한 선결 이론에 의존하며, 그 중 상당수는 아직 형식화되지 않았습니다. 효과적인 시스템은 대상 진술을 형식화할 뿐만 아니라 필요한 종속 이론을 검색하거나 생성해야 합니다.
2. 정의 격차: 기존 벤치마크는 수학적 정의의 형식화를 대부분 무시합니다. 명제 진술만 처리할 수 있는 시스템은 기존 형식 이론에 의해 제한받으며, 정의가 존재하지 않는 개념이 포함된 명제를 형식화할 수 없습니다.
3. 실제 데이터의 부재: 대학원 수준 수학의 "야생 환경 (in the wild)"적 복잡성, 즉 풍부한 문맥적 종속성과 개체 간 관계를 포착하는 대규모 실제 벤치마크는 부족합니다.

방법론

데이터셋 구축: MathAtlas

저자들은 대학원 수준 수학에 대한 최초의 대규모 자동 형식화 벤치마크인 MathAtlas를 소개합니다.

• 원천 자료: 이 데이터셋은 실해석학, 미분 기하학, 범주론, 양자 군 등 87 개의 서로 다른 분야를 다루는 103 권의 대학원 수준 수학 교과서에서 추출되었습니다.
• 규모 및 구성: MathAtlas 는 약 52,052 개의 개체로 구성되어 있으며, 다음과 같습니다:
  • 약 18,000 개의 명제
  • 약 10,000 개의 연습문제
  • 약 10,000 개의 정의
  • 약 10,000 개의 증명
  • 약 5,000 개의 예시
• 종속성 그래프: 데이터셋을 수학적 종속성 그래프로 풍부하게 만든 것이 주요 특징이며, 이 그래프에는 약 178,000 개의 관계가 포함되어 있습니다. 이 그래프는 개체를 다음에 연결합니다:
  • 객체 참조: 외부 정의를 필요로 하는 named 수학적 개념 (예: "데데킨트 환").
  • 개체 참조: 텍스트 내의 다른 특정 명제나 정의에 대한 참조.
  • 로컬 변수 참조: 명시적인 로컬 도입 없이 사용되는 기호.
  • 종속성 깊이: 개체 종속성 트리의 최대 높이 (평균 깊이 30, 최대 80 까지) 로, 분야에 따라 크게 달라집니다 (예: 리 대수는 집합론보다 더 깊은 트리를 가짐).

구축 파이프라인:

1. 변환: Nougat 를 사용하여 PDF 를 수학적 마크다운 (MMD) 으로 변환합니다.
2. 추출: 퓨샷 프롬프트를 사용한 LLM(gpt-oss-120b) 이 정의, 명제 등의 개체와 해당 식별자를 추출합니다.
3. 참조 추출: 두 번째 모델이 추출된 텍스트 내의 객체, 개체, 로컬 변수 참조를 식별합니다.
4. 관계 추출: 시스템이 참조를 대상 개체와 매칭하여 (Mathlib 기반을 위해 LeanSearch 사용, 내부 매칭을 위해 LLM 사용) 종속성 그래프를 구성합니다.
5. 품질 관리: 무작위 샘플에 대한 인간 평가 결과, 개체 추출의 유효성은 90.4%, 관계 추출의 F1 점수는 94.8% 로 나타났습니다.

평가 지표

본 논문은 형식화가 두 가지 조건을 만족해야 하는 **정확성 (Correctness)**이라는 복합 지표를 사용하여 자동 형식화 성능을 평가합니다:

1. 컴파일: 생성된 Lean 4 코드가 성공적으로 컴파일되어야 합니다.
2. 의미적 충실도: 형식화된 진술은 비형식적 원천과 의미적으로 동등해야 합니다.
   • 충실도를 측정하기 위해 저자들은 MathAtlas 의 200 개 개체 (진술 및 정의) 로 구성된 이진 분류 벤치마크인 MA-Align을 도입했으며, 이를 "정렬됨" 또는 "비정렬됨"으로 주석 달았습니다.
   • 기존 "LLM-as-judge" 시스템 (예: CriticLean) 을 평가한 결과, 이전 벤치마크 (ConsistencyCheck, CriticLeanBench) 에서는 잘 수행되었으나 MA-Align 에서는 정확도가 크게 떨어지는 것을 발견했습니다. 이는 대학원 수준 정의 평가의 격차를 강조합니다.

실험 설정

저자들은 MathAtlas 에서 다양한 베이스라인을 테스트했습니다:

• 프롬프트 모델: gpt-oss-20b 및 gpt-oss-120b 를 사용한 제로샷 및 퓨샷 프롬프팅.
• 파인튜닝 모델: Herald, Kimina, ATLAS-L, Goedel, ReForm.
• 애블레이션 연구: 로컬 컨텍스트 (이전 500 토큰), 엔지니어링된 프롬프트, 특정 훈련 예시의 영향을 테스트.
• MA-Hard 하위 집합: 현재 시스템의 한계를 테스트하기 위해 가장 깊은 종속성 트리 (평균 깊이 >50) 를 가진 약 700 개의 개체로 구성된 특정 하위 집합.

주요 결과

전반적 성능

MathAtlas 는 극도로 까다로운 벤치마크임이 입증되었습니다. 강력한 베이스라인도 낮은 정확도만 달성합니다:

• 진술 (명제, 예시, 연습문제): 최상의 베이스라인 (ReForm 8B) 은 **9.8%**의 정확도만 달성합니다.
• 정의: 최상의 베이스라인 (퓨샷 프롬프팅을 적용한 gpt-oss-120b) 은 **16.7%**의 정확도를 달성합니다.
• 격차: 컴파일률과 정확도 사이에 큰 격차가 있습니다 (예: Kimina 7B 는 진술의 27.3% 를 컴파일하지만 충실한 것은 2.3% 에 불과함). 이는 구문적 성공이 의미적 정확성을 보장하지 않음을 나타냅니다.

종속성 깊이와 난이도

종속성 깊이가 증가함에 따라 성능이 크게 저하됩니다:

• MA-Hard(가장 깊은 종속성 트리를 가진 700 개 개체) 에서 최상의 모델은 **2.6%**의 정확도만 달성합니다.
• 통계적 분석 (콜모고로프 - 스미르노프 검정) 은 얕은 종속성 트리와 깊은 종속성 트리 간의 정확도 분포에 유의미한 차이가 있음을 확인했습니다 ($p < 0.001$).

문맥 및 기반

• 로컬 컨텍스트: 프롬프트에 로컬 컨텍스트 (이전 500 토큰) 를 추가하는 것은 프롬프트 모델의 성능을 감소시켰습니다 (정의에서 20.3% 에서 17.4% 로 하락). 이는 현재 모델이 장거리 문맥을 효과적으로 통합하는 데 어려움을 겪고 있음을 시사합니다.
• Mathlib 기반: 기존 형식화 (Mathlib) 에 기반을 둘 수 있는 개체는 기반이 없는 정의 (16.8%) 에 비해 올바르게 형식화될 가능성이 훨씬 높았습니다 (27.9%). 이는 LLM 이 훈련 데이터에서 형식화된 이론에 대한 사전 노출로부터 혜택을 받음을 시사합니다.

중요성과 기여

본 논문은 해당 분야에 다음과 같은 중요성을 주장합니다:

1. 최초의 대학원 수준 벤치마크: MathAtlas 는 올림피아드 및 학부 데이터셋의 제약을 넘어선 최초의 대규모 "야생 환경" 대학원 수준 수학 벤치마크입니다.
2. 종속성 인식 평가: 풍부한 종속성 그래프와 개체 간 관계를 포함하는 최초의 벤치마크로, 선결 이론과 정의 생성을 처리해야 하는 시스템을 평가할 수 있게 합니다.
3. 정의 격차 부각: 결과는 현재 최첨단 모델이 정의와 깊은 종속성 체인에서 크게 어려움을 겪고 있음을 보여주며, 고급 수학으로 자동 형식화를 확장하는 데 있어 중요한 병목 현상을 드러냅니다.
4. 충실도 지표의 한계: MA-Align 의 도입과 후속 실험은 기존 의미적 충실도 지표 (CriticLean 등) 가 대학원 수준 정의에 잘 일반화되지 않음을 보여주며, 새로운 평가 접근법이 필요함을 시사합니다.
5. 커뮤니티 리소스: 저자들은 종속성 인식 자동 형식화 및 고급 수학적 개념의 형식화에 대한 향후 연구를 촉진하기 위해 MathAtlas, MA-Align, 실험 코드를 공개합니다.

저자들은 현재 시스템이 가능성을 보이지만, 기존 능력과 대학원 수준 수학의 요구 사항 사이의 격차, 특히 선결 이론의 생성과 정의의 형식화와 관련하여 여전히 막대하다고 결론지었습니다.