기술 요약: LEAP: 에이전트 프레임워크를 통한 LLM의 형식 수학 능력 극대화

1. 문제 정의

거대 언어 모델(LLM)은 "비형식적" 수학적 추론(자연어)에서는 강력한 능력을 보여주었으나, Lean과 같은 형식 언어(formal languages)를 이용한 기계적 검증 가능 증명을 생성하는 데에는 어려움을 겪고 있습니다. 형식 코퍼스에 맞춰 미세 조정된 특화 모델들이 유망한 성과를 보여주기도 했지만, 범용 파운데이션 모델들은 원샷(one-shot) 형식 정리 증명에서 종종 성능이 저하됩니다. 또한, 기존 벤치마크(예: MiniF2F, PutnamBench)는 포화 상태에 이르렀으며, 현재의 특화 시스템들은 폐쇄형 소스 구성 요소에 의존하거나 국제 수학 올림피아드(IMO)와 같이 고도로 비정형적이고 다단계적인 증명이 요구되는 수준으로 확장하는 데 실패하는 경우가 많습니다.

핵심 과제는 특화된 미세 조정에만 전적으로 의존하지 않고, 일반 LLM의 강력한 비형식적 추론 능력과 엄격한 기계 검증 요구 사항 사이의 간극을 메우는 것입니다.

2. 방법론: LEAP 프레임워크

저자들은 일반 목적의 파운데이션 모델이 자동 형식 정리 증명에서 최첨단 성능을 달랄 수 있도록 설계된 에이전트 프레임워크인 LEAP(LLM-in-Lean Environment Agentic Prover)를 소개합니다. LEAP는 특화된 미세 조정된 프로버 모델에 의존하는 대신, 일반 LLM의 상호 보완적인 기술인 비형식적 추론, 지시 이행, 도구 사용, 그리고 반복적인 자기 개선(self-refinement) 역량을 활용합니다.

2.1. 블루프린트 기반 계층적 분해

인간의 수학적 워크플로우와 Lean Blueprint 도구에서 영감을 얻은 LEAP는 복잡한 증명을 관리 가능한 단위로 분해합니다. 시스템은 AND-OR 유향 비순환 그래프(DAG) 상에서 작동합니다:

• OR 노드: 어떤 유효한 증명 전략에 의해서도 해결될 수 있는 열린 목표(open goals) 또는 보조 정리(lemma) 문장을 나타냅니다.
• AND 노드: 부모 목표가 모든 구성 하위 목표가 증명되어야만 증명된 것으로 간주되는 후보 분해 방식을 나타냅니다.

2.2. 워크플로우 및 반복적 개선

LEAP는 다단계 워크플로우를 따릅니다 (논문의 그림 1 참조):

1. 직접 형식화 시도: 에이전트는 먼저 직접적인 비형식적 증명을 생성하고, 이를 Lean으로 번역한 뒤, Lean 컴파일러로 검증하는 과정을 시도합니다.
2. 분해 (블루프린팅): 직접 증명이 실패할 경우, LEAP는 중간 단계의 보조 정리를 제안하는 비형식적 블루프린트를 작성합니다. 이 블루프린트는 **형식적 증명 스케치(formal proof sketch)**로 번역됩니다.
   • 스케치는 제안된 보조 정리들을 가정하여 현재의 목표를 증명합니다 (새로운 보조 정리에 대해서는 sorry 플레이스홀더만 사용).
   • 만약 스케치가 구문적으로 유효하고 타입이 일치한다면, 이는 AND 노드로 추가되며 제안된 보조 정리들은 자식 OR 노드가 됩니다.
3. 검증 가이드 탐색:
   • 컴파일러 피드백: Lean 컴파일러는 구문과 타입을 검증합니다.
   • LLM 리뷰어: 핵심적인 구성 요소로, LLM 리뷰어가 분해의 품질을 평가합니다. 이는 생산적이지 않은 분기(예: 원래 문제만큼 어렵거나 부모와 구문적으로 동일한 하위 목표)를 필터링하여 탐색 폭발을 방지합니다.
4. 계층적 메모이제이션 (Hierarchical Memoization): DAG 구조를 통해 서로 다른 브랜치 간에 중간 보조 정리를 저장하고 재사용할 수 있어, 중복된 유도를 방지하고 "선제적 보조 정리 계획(anticipatory lemma planning)"(당장 필요하지는 않지만 나중에 유용할 보조 정리를 제안하는 것)을 지원합니다.

3. 주요 기여

3.1. LEP 에이전트 프레임워크

본 논문은 구조화된 에이전트 워크플로우와 결합될 때, 오직 일반 목적의 LLM만을 사용하여 최첨단 형식 정리 증명을 달성할 수 있음을 입증합니다. 이는 특화된 미세 조정이 엄격한 형식 작업에 필수적이라는 기존의 가설에 도전하는 것입니다. 이 프레임워크는 고수준의 블루프린트 스케칭 후 저수준의 형식 생성 및 반복적인 컴파일러 피드백을 수행하는 인간과 유사한 워크플로우를 체계화합니다.

3.2. Lean-IMO-Bench 데이터셋

포화된 벤치마크를 넘어 진전을 평가하기 위해, 저자들은 IMO-Bench(Luong et al., 2025)의 문제 60개를 Lean으로 형식화한 새로운 데이터셋인 Lean-IMO-Bench를 도입합니다.

• 구조: "Basic"(IMO 이전부터 IMO-Medium까지) 세트와 "Advanced"(IMO-Hard까지) 세트로 나뉩니다.
• 특징: 문장은 짧지만 매우 비정형적이고 다단계적이며 구조적으로 복잡한 증명을 요구하는 문제들로 구성되어 있습니다.
• 검증: 정확성을 보장하기 위해 모든 60개 문제의 문장은 Lean 전문가들에 의해 수동으로 형식화되고 검증되었습니다.

3.3. 실증적 결과 및 분석

논문은 두 가지 주요 벤치마크에 대한 광범한 실증적 근거를 제공합니다:

• Putnam 2025: LEAP는 12개의 문제 중 100%(12/12)를 해결하여, 최첨단 폐쇄형 시스템(Aristotle, Numina)과 대등한 성능을 보였으며, 직접적인 베이스라인(일반 LLM 및 특화 모델의 원샷 설정에서의 해결률 0%)을 크게 앞질렀습니다.
• Lean-IMO-Bench: LEAP는 일반 목적 LLM의 원샷 형식 해결률을 10% 미만에서 **70%**로 끌어올렸습니다. 특히 특화된 ATP 모델(5%)과 금메달 수준의 시스템인 Aristotle(48%)을 능가했습니다. LEAP는 두 난이도 계층 모두에서 대수학(Algebra)과 정수론(Number Theory) 분야에서 100% 해결률을 달성했습니다.

3.4. 절제 연구 (Ablation Studies)

저자들은 LEAP 구성 요소의 기여도를 격리하기 위해 절제 연구를 수행했습니다:

• 반복적 vs 원샷: 일반 LLM(Gemini-1.5-Pro)은 반복적인 컴파일러 피드백을 통해 성능이 크게 향상(20%에서 36.6%로)된 반면, 특화 모델(Goedel-Prover-V2)은 큰 혜택을 받지 못해 일반적 추론 능력의 중요성을 강조했습니다.
• DAG vs Tree: 글로벌 DAG 메모이제이션을 제거하고 단순한 트리 구조를 사용했을 경우, Basic 세트에서의 성능이 83.3%에서 73.3%로 감소하여 보조 정리 재사용과 그래프 컨텍스트의 가치를 확인했습니다.
• LLM 리뷰어: LLM 기반의 분해 리뷰어를 제거하면 에이cent가 생산적이지 않은 순환적 분해(예: Putnam A5와 같은 복잡한 문제)로 인해 실패하게 되며, 이는 의미론적 탐색 필터링의 필요성을 입증합니다.

4. 의의 및 주장

본 논문은 일반 목적 LLM이 형식 수학에서 겪는 주요 병목 현상이 언어 이해 능력이 아니라, 증명 환경과의 구조적이고 반복적인 상호작용의 부재라고 주장합니다. 계층적 분해, 컴파일러 피드백, 의미론적 리뷰를 포함하는 에이전트 프레임워크로 일반 LLM을 보강함으로써, 시스템은 비형식적 추론과 형식적 검증 사이의 간극을 메울 수 있습니다.

저자들은 일반적인 파운데이션 모델이 적절한 에이전트 환경에 놓일 때, 거의 제로에 가까운 형식 수학 성능에서 매우 복잡하고 개방적인 연구 문제들을 해결하는 수준까지 발전할 수 있음을 보여줍니다. 이는 5,000줄 이상의 검증된 Lean 코드를 필요로 하는 복잡한 조합론적 과제인 **Knuth의 짝수 차수 Cayley 그래프의 Hamiltonian 분해(Hamiltonian decomposition of even-order Cayley graphs)**의 핵심 하위 문제를 LEAP가 자율적으로 형식화한 것을 통해 입증되었습니다.

이 연구는 패러다임의 전환을 시사합니다: 즉, 형식 코퍼스로 학습된 작은 특화 모델에만 의존하는 대신, 일반 파운데이션 모델의 광범적인 지식, 지시 이행 능력, 자기 수정 능력을 활용하여 형식적 정리 증명에서 경쟁력 있고 때로는 더 우수한 결과를 달성할 수 있다는 것입니다.