기술 요약: Nazrin: Lean 4에서의 원자적 신경 증명 자동화 전술

문제 정의

Lean 4와 같은 시스템에서 인간이 작성한 증명을 기반으로 자동화된 에이전트를 훈련시키는 것은 다음과 같은 중대한 과제에 직면해 있습니다.

1. 무한한 행동 공간 (Unbounded Action Spaces): 인간의 증명은 임의의 파라미터를 가진 무수히 다양한 전술(예: 긴 인자 목록을 가진 simp, 임의의 증거를 가진 use)을 사용하며, 이는 노이즈가 많고 학습하기 어려운 탐색 공간을 생성합니다.
2. 표현 뷰와 탐색 뷰의 차이 (Presentation vs. Search Views): 인간이 작성한 증명은 종종 간결함과 가독성(표현 뷰)을 우선시하여, 실제 증명을 발견하는 데 필요한 점진적인 역방향 추론 단계(탐색 뷰)를 은폐합니다. 여기에는 "신비로운 도약"과 중간 단계의 생략이 포함됩니다.
3. 메타변수 결합 (Metavariable Coupling): Lean에서 목표(goals)들은 서로 의존할 수 있습니다(결합된 메타변수). 단순한 트리 탐색은 하나의 목표를 해결하는 것이 다른 목표를 즉각적으로 해결하거나 혹은 특정 경로를 불가능하게 만들 수 있다는 사실을 고려하지 못하며, 이는 단순한 트리가 아닌 유향 비순환 그래프(DAG) 상에서의 탐색을 복잡하게 만듭니다.
4. 하드웨어 제약 (Hardware Constraints): 기존의 신경 기반 정리 증명기들은 상당한 계산 자원을 요구하는 경우가 많아, 접근성과 훈련 데이터의 규모를 제한합니다.

방법론

본 논문은 그래프 신경망(GNN) 기반의 정리 증명 에이전트인 Nazrin(Neural Atomizer for Inhabitation Problems)을 소개합니다. 이 방법론은 세 가지 핵심 기둥에 의존합니다.

1. 원자적 전술 (Atomic Tactics)

저자들은 Lean의 모든 증명 가능한 문장을 증명할 수 있는 작고 유한한 "원자적 전술" 집합을 정의합니다. 이 전술들은 에이전트의 행동 공간을 유한하게 보장하도록 설계된 제한된 파라미터 공간을 가집니다.

• 완전성 (Completeness): 이 집합은 Lean의 모든 최상위 표현 생성자(예: 람다 추상을 위한 intro, 상수 적용을 위한 exact/apply, 귀납적 타입을 위한 cases)를 포괄합니다.
• 속성: 이 전술들은 불변적이며(백트래킹 없이 할당된 메타변수를 변경하지 않음), 완전하고, 진보적이며(항상 진전을 보임), 결정론적입니다.
• 교차 섹션의 최소화 (Minimization of Cross-Section): 이 집합은 "교차 섹션"(결합된 목표의 수)을 최소화하도록 선택되었으며, 이를 통해 가이드 생성의 난이도를 낮춥니다.

2. 전치 원자화 (Transposing Atomization)

에이전트를 훈련시키기 위해, 저자들은 기존의 인간 작성 증명(표현 뷰)을 원자적 전술의 시퀀스(탐색 뷰)로 변환하는 새로운 알고 アルゴリズム을 개발했습니다.

• 원자화 (Atomization): 이 알고리즘은 임의의 증명 항(proof terms)을 일련의 원자적 단계로 번역합니다. 이는 원자적 전술만을 사용하여 새로운 증명을 구축하도록 실제 증명 항을 가이드로 사용합니다.
• 전치 (Transposition): 알고리즘은 "탐색 뷰"에 맞게 전술의 실행 순서를 재정렬합니다. 이는 발견(예: $\epsilon$-$\delta$ 증명)에 사용되는 역방향 추론을 모사하여, 선행 목표(predecessor goals)보다 후행 목표(successor goals, 즉 선행 목표에 정보를 제공하는 목표)를 우선시합니다.
• 상태 수준 및 목표 수준 전치 (State-Level and Goal-Level Transposition): 시스템은 막다른 길을 피하기 위해 전술 디스패치 순서를 재정렬합니다. 예를 들어, 결합된 목표들이 아직 인스턴스화되지 않았더라도, 타겟이나 자유 변수의 일부에 작용하는 "세미그레이드(semigrade)" 전술들을 임의의 순서로 디스패치할 수 있도록 허용합니다.

3. ExprGraph 및 신경 아키텍처

에이전트는 Lean 표현을 ExprGraph로 표현하여 처리하는 그래프 신경망(GNN)을 사용합니다.

• 본질화 (Essentialization): 표현은 불필요한 기술적 구별(예: 특정 변수 이름, 메타데이터)이 제거된 그래프로 변환됩니다. 이 그래프는 근본적인 대칭성(예: $\alpha$-동치)을 보존하며, 하위 표현이 하위 그래프에 대응되도록 보장합니다.
• 신경 확률 자동자 (Neural Probabilistic Automaton, NPA): 표준 생성 모델 대신, Nazrin은 NPA를 사용합니다. GNN은 유한 상태 자동체의 전이 확률을 조건화합니다.
  • Kind State: 전술 유형(예: intro, apply)을 선택합니다.
  • Descendant States: 특화된 GNN 헤드가 인자(예: apply를 위한 상수를 선택하거나 자유 변수를 선택)를 생성합니다.
• 효율성: 모델은 매우 작으며(표준 라이브러리 기준 1.5M, Mathlib 기준 11M 파라미터), 소비자용 CPU 하드웨어에서도 실행 가능하며 분당 수천 개의 전술을 생성합니다.

주요 기여

1. 원자적 전술: 효율적인 강화 학습 및 지도 학습을 가능하게 하기 위해, 정리 증명 행동 공간을 관리 가능한 크기로 줄이는 유한하고 완전한 전술 집합을 제공합니다.
2. 전치 원자화 알고리즘: 기존의 형식화된 수학을 원자적, 탐색 뷰 증명으로 변환함으로써, 에이전트에게 단순히 '어떻게 제시하는가'가 아니라 '어떻게 증명을 찾는가'를 가르치는 대규모 훈련 데이터를 생성하는 방법을 제공합니다.
3. ExprGraph: 수학적 대칭성과 변수 참조를 활용하여 언어 모델의 어텐션 메커리즘을 명시적으로 모방하는, 축소된 그래프 기반의 Lean 표현 방식입니다.
4. Nazrin 증명기: 원자화된 데이터로 성공적으로 훈련되고 새로운 정리에 일반화될 수 있는 저자원 GNN 기반 에이전트입니다.
5. 평가 프레로부터: 정보 누출을 방정하기 위해, 한 라이브러리의 슬라이스에서 훈련하고 다음 슬라이스에서 테스트하는 방식으로 새로운 이론의 개발을 모사한 엄격한 평가 프레임워크를 구축했습니다.

결과

저자들은 Lean의 표준 라이브러리와 Mathlib에 대해 Nazrin을 평가했습니다:

• 원자화 성공률: 170,180개의 정리 중 약 58%가 성공적으로 원자화되었습니다.
• 일반화 성능:
  • Standard Library Slice 1에서 훈련되었을 때, Nazrin은 Slice 2에서 **57%**의 정확도를 달-성했습니다.
  • Mathlib Slice 3에서 훈련되었을 때, Nazrin은 Slice 4에서 **34%**의 완료율을 기록했습니다.
• 비교: Nazrin은 기존의 자동화 전술(Aesop 및 Grind)이 15초 시간 제한 내에 해결할 수 없었던 정리들을 증명하는 능력을 보여주었습니다.
• 성능: 시스템은 소비자급 하드웨어에서 효율적으로 작동하며, 이는 많은 LLM 기반 증명기들의 높은 자원 요구 사항과 대조됩니다.

의의 및 주장

본 논문은 Nazrin이 인간이 작성한 증명의 구조와 자동화된 탐색의 요구 사항 사이의 근본적인 불일치를 해결한다고 주장합니다. 원자적 전술을 통해 유한한 행동 공간을 강제하고 전치 원자화를 통해 훈련 데이터를 생성함으로써, 저자들은 다음을 입증했습니다:

• 머신러닝 에이전트는 복잡하고 임의적인 파라미터를 처음부터 생성할 필요 없이 점진적으로 증명을 발견하도록 훈련될 수 있습니다.
• 그래프 기반 표현은 수학적 증명의 구조적 대칭성을 포착하는 데 효과적입니다.
• 고성능 정리 증명은 적절한 하드웨어에서도 충분히 가능하며, 이는 기술의 접근성을 높입니다.

저자들은 시스템이 유망하지만, 현재 모든 정리를 커버하지는 못하며(높은 교차 섹션을 가진 증명에서 원자화 실패), 아키텍처가 아직 완전히 튜닝되지 않았음을 언급했습니다. 향-후 연구는 원자화 커버리지 개선, 교차 섹션 감소, 그리고 다중 파라미터 조건화 및 비기호적 데이터(숫자/문자열)를 더 견고하게 처리하기 위한 신경 아키텍처 정교화에 집중될 수 있다고 제안합니다.