기술 요약: 형식적 공리계에서의 자기 지도적 정리 발견 (Self-Supervised Theorem Discovery)

문제 정의

최근의 AI 시스템, 특히 대규모 언어 모델(LLM)은 수학적 추론에서 상당한 진전을 보여주었으나, 이들은 주로 수학적 텍스트, 코드, 기존 정리 라이브러리와 같은 인간이 제공한 사전 지식(priors)에 크게 의존하고 있습니다. 핵심적인 미결 과제는 다음과 같습니다: 에이전트가 인간의 사전 지식, 기존 정리 라이브러리, 또는 훈련용 문제 세트에 대한 접근 없이, 오직 형식적 공리계의 원시 규칙들로부터 시작하여 유용한 정리를 자율적으로 발견할 수 있는가?

현재의 방법론들은 추론을 부트스트래핑하기 위해 인간이 구축한 지식에 의존하는 경우가 많습니다. 공리적 영역 내의 자기 개선 에이전트들조차도 발견된 정리의 유용성을 평가하기 위해 외부 판별자(external judges)에 의존하곤 합니다. 본 논문은 에이전트가 단순히 정리를 발견하는 것을 넘어, 오직 공리와 추론 규칙만을 사용하여 자신의 증명 탐색 및 외부 추론 시스템의 성능을 개선할 수 있는 "유용한" 정리를 식별하고 활용할 수 있는지 조사합니다.

방법론

1. 형식적 설정: 스택 머신으로서의 힐베르트 체계 (Hilbert System)

저자들은 문제를 명제 논리를 위한 힐베르트 공리계 내에서 구현하였습니다. 이 체계는 의도적으로 최소화되었으며, 다음으로 구성됩니다:

• 세 가지 공리:
  • $Ax1: A \to (B \to A)$ (약화, Weakening)
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (분배, Distribution)
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ (대우, Contraposition)
• 한 가지 추론 규칙: 모두스 포넨스(Modus Ponens, MP), 즉 $X$와 $X \to Y$로부터 $Y$를 도출함.

학습을 용이하게 하기 위해, 저자들은 정리 증명을 결정론적이고 목표 조건부인 스택 머신 의사결정 과정 $(S, A, s_0, P)$로 정식화했습니다:

• 상태 ($S$): 공식(formula)들의 유한한 스택.
• 행동 ($A$): $Ax1, Ax2, Ax3$의 인스턴스를 스택에 푸시(push)하거나, 모두스 포넨스(MP)를 적용함.
• 메커니즘: MP 행동은 힌들리-밀너(Hindley–Milner) 유니피케이션을 사용합니다. 만약 스택의 최상단 요소가 $X \to Y$와 유니파이(unify)되고, 그 아래 요소가 $X$와 유니파이된다면, 두 요소는 팝(pop)되고 $Y$가 푸시됩니다.
• 성공: 스택에 타겟 목표와 일치하는 단 하나의 공식이 포함되면 증명이 성공한 것으로 간듭니다.

2. 자기 지도적 정리 발견 알고리즘

핵 core 기여는 증명 탐색과 유용한 정리 추출을 교대로 수행하며, 향후 탐색을 위한 보조 정리(lemma) 역할을 할 정리 라이브러리를 구축하는 알고리즘입니다.

A. 목표 조건부 정책 학습 (Goal-Conditioned Policy Learning)

에이전트는 현재 스택 $S$와 타겟 목표 $g$가 주어졌을 때 다음 행동을 예측하는 정책 $\pi_\theta(A|S, g)$를 학습합니다.

• 하indsight 학습 (Hindsight Learning): 탐색 에피소드 동안, 스택에 단일 공식 $f_t$가 포함된 모든 상태는 원래의 목표와 상관없이 "도달한 정리(reached theorem)"로 취급됩니다.
• 훈련 신호: $f_t$로 이어진 행동 접두사(action prefix)는 $f_t$에 대한 증명으로 간주됩니다. 이러한 접두사들은 교차 엔트로피 손실을 통해 정책을 업데이트하기 위해 훈련 세트 $D_{train}$에 추가됩니다.
• 목표 버퍼 ($G$): 버퍼는 발견된 정리들을 유지합니다. 에이전트는 이후의 탐색 에피소드를 위해 $G$에서 정리를 균등하게 샘플링하며, 이는 효과적으로 스스로의 커리큘럼을 부트스트래핑하는 역할을 합니다.

B. 유용한 정리 추출

라이브러리가 사소하거나 중복된 정리들로 비대해지는 것을 방방지하기 위해, 알고리즘은 다음 두 가지 기준에 따라 발견된 정리를 필터링합니다:

1. 일반성 (Generality): 정리는 다른 후보들의 단순한 특수화(specialization)인 경우를 제거하기 위해 필터링됩니다. 시스템은 공식 치환(formula substitution)에 의해 정의된 부분 순서(partial order) 하에서 "최소" 요소들(즉, 가장 일반적인 형태들)만을 유지합니다.
2. 재증명 가능성 (Reprovability): 시스템은 현재 정책이 특정 정리를 재증명할 수 있는 확률을 추정합니다. 베이지안 사후 평균(Beta(1,1) 사전 분포)을 사용하여, 정리는 발견되었으나 재증명하기 어려운(difficult to reprove) 정리를 우선시합니다. 이러한 "재증명하기 어려운" 정리들은 가치 있는데, 왜냐하면 이를 보조 정리로 추가함으로써 어려운 증명 경로를 압축할 수 있기 때문입니다.

C. 다세대 라이브러리 확장 (Multi-Generation Library Expansion)

프로세스는 다음과 같은 세대 단위로 작동합니다:

1. 정책 학습: 현재 행동 공간(초기에는 공리와 MP만 포함)에서 정책을 학습합니다.
2. 추출: 일반성과 재증명 가능성을 기준으로 목표 버퍼 $G$에서 유용한 정리를 식별합니다.
3. 행동 공간 확장: 추출된 정리를 새로운 라이브러리 행동(예: $Thm_1, Thm_2$)으로 추가합니다. 이 행동이 선택되면 해당 정리를 스택에 푸시하여 검증된 보조 정리로서 기능하게 합니다.
4. 반복: 이 과정을 반복하여, 에이전트가 이전에 발견한 정리를 사용하여 더 복잡한 새로운 정리를 찾도록 합니다.

주요 기여

1. 정식화: 명제 정리 증명을 인간의 정리 코퍼스에 의존하지 않고, 힐베르트 공리와 추론 규칙에 직접 기반한 스택 머신 의사결정 과정으로 정식화했습니다.
2. 알고리즘: 원시 규칙으로부터 스스로 정리 라이브러리를 키워나가는 자기 지도적 정리 발견 알고리즘을 제안했습니다. 이 알고리즘은 추출된 정리를 후속 증명 탐색을 위한 보조 정리로 재사용합니다.
3. 자율적 발견: 에이전트는 수만 개의 정리를 발견하고, 인간의 사전 지식을 사용하지 않고도 인간이 작성한 벤치마크 문제들에 대한 증명을 찾아냅니다.
4. 전이 가능성: 추출된 정리는 프롬프트 보조 정리(prompt lemmas)로 제공될 때, 외부 LLM의 증명 성능을 유의미하게 향 향상시키는 효과적인 외부 지식 역할을 합니다.

실험 결과

1. 정리 발견 및 커버리지

• 성장: 발견된 정리의 수가 6세대에 걸쳐 증가하며, 에이전트가 자율적으로 지식 기반을 확장할 수 있음을 입증했습니다.
• 벤치마크 성능: 에이전트는 클라인(Kleene)의 교과서에서 파생된 인간 작성 벤치마크 세트의 **30%**에 대해 힐베르트 체계 증명을 성공적으로 찾아냈습니다.
• 비교: (가장 강력한 베이스라인인) GPT-5-high가 도움 없이 이 벤치마크에서 약 23%의 정확도를 달encing하는 것에 비해, 에이전트가 30%의 증명을 찾아낸 것은 이 발견된 정리가 인간의 수학적 관점에서도 의미 있는 비자명한(non-trivial) 증명임을 시사합니다.

2. LLM 추론에 미치는 영향

• 프롬프트 보조 정리 (Prompt Lemmas): 추출된 정리를 GPT-4o 및 GPT-5 변체들에 프롬프트 보조 정리로 제공했을 때, 벤치마크 문제에 대한 증명 성공률이 유의미하게 향상되었습니다.
• 질적 분석:
  • 발견된 정리 중 일부는 잘 알려진 원리(예: 폭발 원리, $\neg A \to (A \to B)$)에 대응하며, 이는 쉽게 해석 가능합니다.
  • 또 다른 정리들(예: 복잡한 함의 리프팅, implication lifting)은 인간에게 즉각적으로 명확하지는 않지만, LLM 증명에서 효과적인 지원 지식으로 기능합니다.
  • 이는 에이전트가 인간이 명시적으로 제공하지 않은 유용한 보조 정리를 표면화할 수 있으며, 이 지식이 서로 다른 추론 구조(에이전트에서 LLM으로) 간에 전이 가능하다는 것을 나타냅니다.

의의 및 주장

본 논문은 인간이 제공한 정리 라이브러리에 의존하지 않고도 증명 탐색을 통해 유용한 정리가 출현할 수 있음을 보여주는 증거를 제공한다고 주장합니다.

• 자기 진화형 AI: 이 연구는 수학을 위한 자기 진화형 AI 시스템을 향한 경로를 제시합니다. 이 시스템은 모든 발견이 공리로부터 엄격히 검증되는 동시에, 증명 탐색을 통해 자율적으로 형식적 지식을 확장할 수 있습니다.
• 형식적 검증 가능성: 환각(hallucination)을 일으켜 그럴듯하지만 틀린 문장을 생성할 수 있는 LLM과 달리, 이 에이전트의 발견물은 힐베르트 체계의 공리와 추론 규칙에 엄격하게 근거합니다.
• 겸손한 태도: 저자들은 일반적인 추론 능력에서 최첨단 LLM을 능가했다고 주장하지 않습니다. 대신, 제한된 형식적 환경 내에서 에이전트가 어떻게 스스로의 지식을 발견하고 활용하여 고급 LLM조차 해결하기 어려운 문제를 풀 수 있는지, 그리고 이 자가 발견된 지식이 외부 시스템을 어떻게 강화할 수 있는지를 입증했습니다.

본 연구는 단일 공리계(힐베르트 명제 논리)로 제한되어 있으나, 저자들은 이 프레임워크가 1차 논리(first-order logic)나 집합론과 같은 더 풍부한 체계로 일반화될 수 있다고 보고 있으며, 이는 향후 연구 방향으로 남아 있습니다.