LAMP: MCP와 증명 수리 (Proof Repair)를 활용한 Lean 기반 에이전트 프레임워크

대규모 언어 모델 (LLM)은 수학적 추론 능력이 점점 향상되고 있지만, 이들이 생성하는 증명은 종종 신뢰할 수 없으며 검증하기 어렵습니다. Lean 4와 같은 대화형 정리 증명기 (Interactive theorem provers)는 커널 검증된 (kernel-checked) 증명만을 수용함으로써 이 문제를 해결하지만, 그 범위는 사용 가능한 형식화된 지식에 의해 제한됩니다. 다양한 수학 분야를 다루는 Lean 4 정리의 형식화 저장소인 Mathlib이 존재함에도 불구하고, 특정 전문 분야는 여전히 충분히 다뤄지지 않고 있습니다. 특히 단어 조합론 (Combinatorics on Words, CoW) 분야가 그러합니다. CoW는 수열을 연구하며 주기성 (periodicity), 경계 (borders), 공액 (conjugacy), 형태 (morphisms)와 같은 특성을 탐구합니다. 그 결과, Mathlib 중심의 데이터로 학습된 전문 증명기들은 CoW 분야에서 작동하기 위한 보조 정리 (lemmas)가 부족한 실정입니다.

우리는 두 가지 기여를 제시합니다. 첫째, 8개의 모듈과 93개의 핵심 정의 및 기초 보조 정리 선언을 포함하는 CoW의 Lean 4 형식화 (formalization)를 도입합니다. 둘째, 증명기를 미세 조정 (fine-tuning)하는 대신, 추론 시점에 온톨로지 (ontology)를 통해 명시적이고 구조화된 도메인 지식을 제공함으로써 커널 검증된 Lean 4 증명을 합성하는 멀티 에이전트 프레임워크인 LAMP를 제시합니다. LAMP는 모델 컨텍스트 프로토콜 (Model Context Protocol, MCP) 기반의 도메인 특화 CoW 온톨로지 접근 권한을 가진 플래너 (Planner), 빌더 (Builder), 검증기 (Verifier)를 조정합니다. 8개 모듈과 3가지 난이도 수준을 아우르는 90개의 CoW 정리 세트에서, LAMP는 정리의 96.7%에 대해 검증된 증명을 합성하였으며, 이는 스캐폴딩이 없는 베이스라인 (unscaffolded baseline)과 기존의 전문 증명기들을 모두 크게 상회하는 수치입니다. 절제 연구 (ablation) 결과, 백본 모델 (backbone model)을 고정하더라도 LAMP의 도구 기반 아키텍처를 제거하거나 플래너/빌더 분리를 제거할 경우 각각 약 12% 포인트의 성능 저하가 발생함을 보여주었습니다.