기술 요약: MATHLIBLEMMA

1. 문제 제기

공식 수학 생태계, 특히 Lean 과 그 라이브러리인 Mathlib 은 LaTeX 나 Maple 과 같은 일상적인 도구로 자리 잡는 것을 방해하는'마지막 한 마일'장벽에 직면해 있습니다. 대규모 언어 모델 (LLM) 이 자동 정리 증명 분야에서 진전을 이루었지만, 지속적인 병목 현상이 남아있습니다. 그것은'구전 보조정리 (folklore lemmas)'의 부재입니다. 이러한 보조정리는 실무 수학자들이 routinely 사용하며 자명하다고 여기는 중간 사실들 (종종 교과서나 실습을 통해 암묵적으로 습득됨) 이지만, 재사용 가능한 형태로 공식 라이브러리에 명시적으로 존재하지는 않습니다.

이러한 보조정리가 누락되면, 사소하지만 필수적인 단계에서 공식화가 멈추게 되며, LLM 기반 증명기는 이를 호출하는 대신 처음부터 결과를 재구성하도록 강요받습니다. 이는 검색 공간을 확장하고 컨텍스트 토큰을 소모하며, 환각과 실패 가능성을 높입니다. 현재의 평가는 종종 고정된 올림피아드 수준의 문제 세트 (예: MiniF2F) 에 초점을 맞추는데, 이는 성능 포화 상태에 도달하여 밀집되고 재사용 가능한 라이브러리 확장에 대한 구조적 필요성을 해결하지 못합니다.

2. 방법론: MATHLIBLEMMA 파이프라인

저자들은 이러한 누락된 구전 보조정리를 능동적으로 채굴, 공식화, 증명하도록 설계된 모듈형 LLM 기반 파이프라인인 MATHLIBLEMMA를 소개합니다. 이 시스템은 의미적 환각, 구문 오류, 증명 검색 실패와 같은 실패 모드를 직교 구성 요소로 분해하기 위해 네 가지 명확한 단계를 통해 작동합니다.

1. 발견 모듈 (맥락 인식 생성):

   • 입력: 기존 Mathlib 소스 파일 (시드).
   • 과정: LLM 은 시드 맥락을 기반으로 구조적 공백과 주제 간 상호작용에 초점을 맞춰 plausible 한 누락된 보조정리를 브레인스토밍하도록 프롬프트됩니다.
   • 출력: 증명 시도를 하지 않은 채 sorry 플레이스홀더가 포함된 Lean 코드의 원시 후보 진술.

2. 심사관 모듈 (의미 필터링):

   • 과정: LLM 이 심사관 역할을 하여 Lean 구문의 잘 형성 여부를 명시적으로 무시하고 원시 후보의 수학적 정확성을 평가합니다.
   • 목표: 비용이 많이 드는 커널 검사나 증명 검색 전에 수학적으로 거짓이거나 nonsensical 인 진술을 필터링합니다.
   • 출력: 이진 판정 (옳음/틀림); "옳음"후보만 진행됩니다.

3. 공식화 모듈 (커널 기반 수리):

   • 과정: 시스템은 의미적으로 필터링된 진술을 타입 체크하기 위해 Lean 서버 (Kimina Lean 서버) 와 상호작용합니다.
   • 루프: 오류가 발생하면 LLM 이 컴파일러 진단에 기반하여 구문, 네임스페이스, 암시적 인수를 반복적으로 수리합니다. 진술이 오류 수준의 진단 없이 컴파일되거나 최대 시도 횟수에 도달하면 루프가 종료됩니다.
   • 출력: 타입 체크된 Lean 진술 (여전히 sorry 포함).

4. 증명기 모듈 (증명 검색 및 검증):

   • 과정: 증명기 LLM 이 타입 체크된 진술에 대한 완전한 증명을 생성하려고 시도합니다.
   • 검증: 성공적인 시도는 두 가지 검사를 통과해야 합니다.
     1. Lean 커널 검사: 파일이 오류 없이 확장되어야 합니다.
     2. 증명 우회 스크린: 생성된 코드에서 주석을 제거하고 불완전한 플레이스홀더 (sorry, admit, sorryAx) 가 없으며 모델이 도입한 새로운 가정 (axiom, constant, opaque) 을 추가하는 최상위 선언이 없는지 확인합니다.
   • 루프: 실패한 증명은 최대 2 회 수리 라운드를 수행하는 생성 - 검증 - 수리 루프를 트리거합니다.

3. 주요 기여

A. MATHLIBLEMMA 벤치마크

이 파이프라인은 세 가지 영역에 걸친 4,028 개의 비자명한 타입 체크된 Lean 진술로 구성된 벤치마크 세트를 생성했습니다.

• 기초: 실해석학, 이산 구조, 기본 확률론.
• 응용: 고급 확률론 (마팅게일), 정보 이론, 볼록 해석학.
• 추상: 범주론, 대수적 위상수학, 미분기하학.

이전 벤치마크와 달리, 이들은 사전에 존재하는 정답 증명이 없는 새로 발견된 추측들입니다. 저자들은 모델이 해결하지 못한 잔여물에 대해 시드 계층화 표본에 대한 인간 증명 가능성 감사를 수행했는데, **78%**가 수학적으로 타당하고 전문가에 의해 증명 가능하다는 것을 발견했습니다. 이는 많은 실패가 거짓 진술 때문이 아니라 현재 증명기의 한계 때문임을 나타냅니다.

B. 검증된 구전 라이브러리

이 파이프라인은 증명 우회 스크린을 통과한 1,506 개의 Lean 확인 증명 저장소를 생성했습니다. 이는 커뮤니티를 위한 재사용 가능한 자산 역할을 합니다.

• 상향식 유효성 검증: 6 개의 큐레이션된 보조정리를 Mathlib 에 제출하는 소규모 파일럿 노력이 있었습니다. 세 개가 병합되어 선택된 출력물이 전문가 라이브러리 표준을 충족할 수 있다는 외부 증거를 제공했습니다. 병합된 예시에는 Grönwall 경계에 대한 단조성 보조정리, 측도론의 커널 호환성 보조정리, 확률론의 중심 모멘트에 대한 거의 모든 곳에서의 합동 보조정리가 포함됩니다.

C. 최첨단 모델 평가

이 벤치마크는 외부 검색이 없는 폐쇄형 제약 하에서 다양한 모델 (GPT-5.1, DeepSeek-R1 변형, Goedel-Prover, Kimina-Prover, Qwen3) 을 평가하는 데 사용되었습니다.

• 결과: 모든 모델의 합집합이 보조정리의 **37.39%**를 증명했으며, 가장 뛰어난 개별 모델 (Goedel-Prover) 은 **19.39%**를 증명했습니다.
• 전문가 대 일반인: Goedel-Prover 는 기초 영역 (27.42%) 에서 뛰어났지만 추상 영역 (8.24%) 에서는 어려움을 겪은 반면, GPT-Reasoning 은 영역 전반에 걸쳐 더 일관된 성능을 보였습니다.
• 다양성: 최상위 단일 모델과 합집합 성능 간의 상당한 격차는 향후 시스템이 다양한 아키텍처의 앙상블을 우선시해야 함을 시사합니다.

4. 중요성 및 주장

이 논문은 MATHLIBLEMMA 가 LLM 의 역할을 공식 라이브러리의 수동적 소비자가 아닌 확장에 대한 능동적 기여자로 전환시킨다고 주장합니다.

• 마지막 한 마일 격차 해소: 수학의'연결 조직'을 능동적으로 채굴함으로써 증명 보조기기의 사용성을 제한하는 누락된 구전 보조정리라는 구조적 장벽을 해결합니다.
• 구체적 방법론: 이 프레임워크는 Mathlib 으로의 증명 성공적 상향식 제출과 인간 감사를 거친 잔여물의 높은 유효성률로 검증된 자동 라이브러리 확장을 위한 구체적 방법론을 제공합니다.
• 벤치마킹 전환: 평가 초점을 고립된 어려운 퍼즐 (올림피아드 문제) 해결에서 인간 수학자가 당연시하는 방대한 양의 일상적 배경 사실을 공식화하는 기초 작업으로 이동시킵니다.

저자들은 새로움 필터링을 위한 구문적 고유성에 대한 의존성 (의미적 중복을 놓칠 가능성), 수리 루프 내 의미 일관성 검사의 부재, 그리고 Mathlib 에 최종 통합되기 전 이름, 배치, 일반성에 대한 인간 큐레이션의 필요성 등 한계를 인정합니다. 그들은 이 작업을 완전한 자율적 솔루션이 아닌 공식 수학 라이브러리의 AI 지원 확장을 향한 한 걸음으로 위치시킵니다.