Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization

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

AI 기반 자동 형식화 (Autoformalization) 의 한계와 '의미적 환각 (Semantic Hallucination)'

• 현재 상황: AI 를 활용한 수학 자동 형식화 기술이 급격히 발전하고 있으나, 기존 증명 보조 도구 (Proof Assistant) 의 타입 체커 (Type Checker) 는 논리적 정합성 (Proof term 의 구조적 정확성) 만을 보장할 뿐, 정의와 명제가 의도한 수학적 내용을 올바르게 반영하는지는 검증하지 못합니다.
• 핵심 문제 (의미적 환각): AI 가 생성한 형식화된 코드가 타입 체커를 통과하고 증명까지 완료되었더라도, 원래의 자연어 수학 명제와 의미적으로 일치하지 않는 경우가 발생합니다. 이를 저자들은 **'의미적 환각 (Semantic Hallucination)'**이라고 명명했습니다.
  • 예시: "3/2 = 1.5"를 형식화할 때 타입 어노테이션을 누락하면, Lean 이 이를 자연수 (Nat) 로 해석하여 "3/2 = 1"이라는 명제를 생성할 수 있습니다. 이는 논리적으로 증명 가능하지만 원래 의도한 수학 내용과는 다릅니다.
• 확장성 문제: 대규모 형식화 프로젝트에서 인간이 모든 명제와 정의의 의미적 정확성을 수동으로 검증하는 것은 비현실적입니다. 따라서 인간이 검증해야 할 후보 집합을 효율적으로 축소할 수 있는 방법이 필요합니다.

2. 제안 방법론 (Methodology)

저자들은 인간 - AI 협업 워크플로우를 제안하며, 이를 실현하기 위해 Lean Atlas와 Lean Compass를 개발했습니다.

A. 핵심 개념: 정렬된 Lean 코드 (Aligned Lean Code)

• 타입 체커의 논리적 정확성과 인간 과학자의 의미적 검증을 모두 통과한 형식화 코드를 **'정렬된 Lean 코드 (Aligned Lean Code)'**로 정의합니다. 이는 AI 생성 형식화의 품질 표준으로 제안됩니다.

B. Lean Atlas (도구)

• 목적: Lean 4 프로젝트의 의존성 그래프를 시각화하여 인간이 전체 구조를 파악하고 의미적 검증을 효율화하는 통합 증명 환경입니다.
• 아키텍처:
  • 백엔드 (Lean 4): Lean 환경의 모든 상수 (Constant) 를 탐색하여 의존성 그래프를 추출합니다.
  • 프론트엔드 (Web): Next.js 와 React Flow 를 기반으로 한 인터랙티브 웹 뷰어를 제공합니다.
• 의존성 분류: 그래프의 에지를 **타입 의존성 (Type Dependency)**과 **값 의존성 (Value Dependency)**으로 구분합니다.
  • 타입 의존성: 명제나 정의의 시그니처 (Type) 에 포함된 의존성 (의미적 검증 필수).
  • 값 의존성: 증명 term 이나 구현체 (Value) 에만 포함된 의존성.

C. Lean Compass (알고리즘)

• 기능: 사용자가 선택한 목표 정명 (Theorem) 집합에 대해, 의미적 정확성에 영향을 미칠 수 있는 프로젝트 고유 노드 (Project-specific nodes) 만을 자동으로 추출하여 검증 대상 범위를 축소합니다.
• 작동 원리 (Pruning Rule):
  1. 증명 의존성 제거: 정리의 증명 (Proof) 에서 파생된 값 의존성 (Value Dependency) 은 타입 체커가 이미 논리적 정합성을 보장하므로 **삭제 (Prune)**합니다.
  2. 정의 의존성 유지: 정의 (Definition) 의 구현체에서 파생된 값 의존성은 타입 시그니처에 없는 계산적 내용을 포함할 수 있으므로 유지합니다.
  3. 의존성 그래프 축소: 위 규칙에 따라 그래프를 다듬고, 목표 정리에서 도달 가능한 노드 (Reachable Nodes) 만을 '검증 원뿔 (Review Cone)'로 추출합니다.
• 출력: 인간이 의미적 검증을 수행해야 할 최소한의 노드 집합을 제공합니다.

3. 주요 기여 (Key Contributions)

1. 문제 정의 및 해결 접근법: AI 생성 증명에서의 '의미적 환각' 문제를 정의하고, 인간이 의미적 검증을 담당하는 'Human-in-the-loop' 접근법과 'Aligned Lean Code' 개념을 제시했습니다.
2. Lean Atlas 도구 개발: Lean 4 프로젝트의 의존성 그래프를 3 가지 축 (Source Kind × Dependency Site × Target Kind) 에 따라 8 가지 유형으로 분류하고, 이를 인터랙티브하게 시각화하는 도구를 구현했습니다.
3. Lean Compass 알고리즘: 목표 정리 집합에 대해 의미적 검증이 필요한 노드만 자동으로 추출하는 알고리즘을 제안하고 구현하여, 대규모 형식화에서의 인간 검증 부하를 획기적으로 줄였습니다.

4. 실험 결과 (Results)

저자들은 6 개의 다양한 Lean 4 프로젝트 (수학, 물리학, 암호학) 를 대상으로 도구를 평가했습니다.

• 평가 대상 프로젝트:
  • 증명 중심 (Proof-heavy): PrimeNumberTheoremAnd, Carleson, Brownian Motion.
  • 혼합형 (Mixed): FLT (페르마의 마지막 정리), PhysLib (이론 물리학).
  • 정의 중심 (Definition-heavy): XMSS (암호학).
• 노드 축소율 (Node Reduction Rate): Lean Compass 적용 후 검증 대상 노드가 줄어든 비율입니다.
  • 증명 중심 프로젝트: 매우 높은 축소율 달성.
    • PrimeNumberTheoremAnd: 94~99% (평균 99% 이상).
    • Carleson: 88~99% (평균 96.2%).
    • Brownian Motion: 89~99% (평균 94.4%).
    • 예시: Brownian Motion 의 주요 정리 IsBrownian_brownian 은 227 개 노드가 14 개로 축소되어 93.8% 감소했습니다.
  • 혼합형 프로젝트:
    • FLT (6 개 마일스톤 정리): 59.8% (상위 정리들은 90% 이상 축소되나, 하위 정의 의존성이 많은 부분은 축소율이 낮음).
    • PhysLib: 69.0% (물리 법칙 정의가 많은 부분은 축소율이 낮았으나, 증명 중심 정리는 96% 까지 축소).
  • 정의 중심 프로젝트:
    • XMSS: 27.3% (정의와 구현체의 값 의존성이 의미적 검증에 필수적이므로 축소율이 상대적으로 낮음).
• 결론: 축소율은 프로젝트의 크기나 이름이 아니라, 검증 원뿔 (Review Cone) 내의 '정리 대 정의 (Theorem vs Definition)' 비율에 의해 결정됩니다. 증명 의존성이 주를 이룰수록 축소 효과가 큽니다.

5. 의의 및 결론 (Significance)

• 과학적 형식화의 확장: 이 접근법은 순수 수학뿐만 아니라 **이론 물리학 (PhysLib)**과 **암호학 (XMSS)**과 같은 과학 및 공학 분야에서도 AI 생성 코드의 의미적 정확성을 검증하는 데 적용 가능함을 입증했습니다.
• 인간 - AI 협업의 새로운 표준: "Aligned Lean Code"를 통해 AI 가 생성한 코드의 논리적 정확성과 인간이 검증한 의미적 정확성을 결합한 새로운 품질 표준을 제시했습니다.
• 확장성: Lean Compass 를 통해 인간 검증자가 확인해야 할 노드 수를 최대 99% 까지 줄일 수 있어, 대규모 AI 생성 형식화 프로젝트의 실용성을 크게 높였습니다.
• 향후 과제: 실제 인간 검증 시간 단축 효과의 정량적 평가, AI 가 생성 시 신뢰도 (Confidence) 메타데이터를 자동 추정하는 기능 통합, 그리고 더 넓은 과학 분야로의 적용 확대가 필요합니다.

이 논문은 AI 가 생성한 형식적 증명의 신뢰성을 높이기 위해, 기계적 검증 (타입 체킹) 과 인간적 검증 (의미 분석) 을 효율적으로 결합하는 체계적인 프레임워크를 제시했다는 점에서 중요한 의의를 가집니다.