기술 요약: 자동 정리 증명용 자연어 기반 그래프 테스트 시간 컴퓨팅 확장

문제 제기

대규모 언어 모델 (LLM) 이 다단계 논리적 추론에서 능력을 입증했음에도 불구하고, 자동 정리 증명은 여전히 난제입니다. 구체적인 장애물로는 핵심 수학 개념의 정확한 식별, 그들 간의 상호 관계 이해, 그리고 자연어 또는 형식 시스템 내에서 증명을 올바르게 형식화하는 것이 포함됩니다. 기존 접근법은 종종 집중적인 파인튜닝, 전문가 반복, 또는 대량의 형식 데이터 (예: Lean) 를 통한 학습에 의존하는데, 이는 자원 집약적일 뿐만 아니라 모델이 더 광범위한 비형식적 수학 지식을 활용하는 능력을 제한할 수 있습니다. 또한, 순수한 형식적 접근법은 자연스러운 추론의 유연성 처리에 어려움을 겪을 수 있으며, 순수한 자연어 접근법은 형식 검증 시스템으로 전환할 때 모호성에 직면합니다.

방법론: KG-Prover

저자들은 일반 목적 LLM 에 ProofWiki 와 같은 권위 있는 수학 텍스트에서 채굴된 지식 그래프 (KG) 를 보강하여 증명을 구성하고 형식화하는 새로운 프레임워크인 KG-Prover를 소개합니다. 이 시스템은 기본 LLM 의 추가적인 파인튜닝 없이 작동하며, 대신 테스트 시간 컴퓨팅 확장과 검색 증강 생성 (RAG) 에 의존합니다.

핵심 구성 요소

1. 지식 그래프 구축:

   • 소스: 그래프는 ProofWiki 를 구문 분석하여 "정의 (Definition)", "공리 (Axiom)", "증명 (Proof)"과 같은 네임스페이스에서 노드를 추출함으로써 구축됩니다.
   • 구조: 각 노드는 독립적인 수학적 진술 (예: 정리 명제 또는 정의) 을 나타냅니다. 간선은 텍스트 내에서 발견된 하이퍼링크를 나타내며, 의존성과 개념적 관계를 포착합니다.
   • 규모: 결과 그래프는 60,000 개 이상의 노드와 300,000 개 이상의 간선을 포함합니다.
   • 임베딩: 노드는 의미 검색을 용이하게 하기 위해 사전 계산된 임베딩 벡터 (text-embedding-3-large 사용) 로 보강됩니다.

2. 추론 파이프라인:

   • 검색 및 탐색: 명제 $P$가 주어지면 시스템은 그 임베딩을 계산하고 가장 유사한 상위-$k$개 노드를 검색합니다. 초기 증명 시도가 실패하면 시스템은 방문한 노드의 상위-$k$개 이웃을 선택하며 그래프를 깊이 $d$까지 탐색하여 컨텍스트를 반복적으로 확장합니다.
   • 비형식적 증명 생성: LLM 은 검색된 컨텍스트를 사용하여 비형식적 자연어 증명을 생성합니다. 이는 모델의 등장적 추론 능력과 KG 에 존재하는 광범위한 비형식적 증명 코퍼스를 활용합니다.
   • 자동 형식화: 별도의 모델 (DeepSeek-Prover-V1.5) 이 비형식적 증명을 Lean 4 코드로 번역합니다.
   • 검증 및 정제: 생성된 Lean 코드는 Lean 4 정리 증명기를 사용하여 검증됩니다. 검증이 실패하면 오류 메시지가 정제를 위해 자동 형식화기로 피드백됩니다. 여전히 증명이 실패하면 시스템은 그래프 탐색 깊이를 증가시키거나 검색 전략을 채택할 수 있습니다.

3. 확장 전략 (테스트 시간 컴퓨팅):

   • Best-of-N: 시스템은 $n$개의 독립적인 비형식적 증명을 생성하고, 이를 자동 형식화한 후, 정답성과 명확성을 기준으로 전용 "심판" 모델이 점수를 매겨 최고 점수 후보를 선택합니다.
   • 빔 검색 (Beam Search): 증명 후보들은 너비 $w$의 빔으로 구성됩니다. 각 단계에서 검증기 피드백을 기반으로 후보들이 확장되고 점수가 매겨지며, 상위-$k$개는 다음 반복을 위해 유지됩니다. 이는 다양한 증명 경로의 탐색과 검증 기반 정제 사이의 균형을 맞춥니다.

주요 기여

• KG-Prover 프레임워크: 비형식적 증명 생성과 반복적인 지식 그래프 기반 탐색 및 LLM-as-a-judge 메커니즘을 통합하여 전문화된 학습이나 전문가 반복의 필요성을 제거하는 시스템.
• 대규모 수학 KG: ProofWiki 에서 60,000 개 이상의 노드와 300,000 개 이상의 간선을 가진 지식 그래프를 구축하여 수학 개념 간의 복잡한 관계를 모델링함.
• 반복적 정제 시스템: 휴리스틱 평가 및 빔 검색 메커니즘을 통해 베이스라인 대비 최대 26.4%, 비확장 KG-Prover 구성 대비 21.8% 의 성능 향상을 달성함.
• 테스트 시간 확장 입증: 그래프 탐색 깊이 조절과 검색 전략 (Best-of-N, 빔 검색) 도입이 기본 모델을 재학습하지 않고도 성능을 크게 향상시킨다는 증거.

실험 결과

이 프레임워크는 miniF2F-test, ProofNet, MUSTARDSAUCE라는 세 가지 벤치마크에서 평가되었습니다.

• 성능 향상:

  • KG-Prover 는 모든 데이터셋에서 베이스라인 시스템과 표준 검색 증강 생성 (RAG) 을 일관되게 능가했습니다.
  • Llama 3.1 8B, GPT-4o, o1-mini 등 여러 모델에서 베이스라인 대비 **2% 에서 11%**까지의 개선이 있었습니다.
  • miniF2F-test에서 일반 목적 LLM 은 KG-Prover 와 결합 시 최대 **21%**까지 향상되었습니다.
  • o4-mini를 사용한 KG-Prover 구성은 miniF2F-test 에서 **50%**의 통과율을 달성했습니다.
  • 가장 높은 확장 구성에서 베이스라인 대비 개선 폭은 **26.4%**에 달했습니다.

• 확장 효과:

  • 탐색 깊이: 정확도는 탐색 깊이 ($r$) 가 증가함에 따라 향상되었으며, 특히 Llama 3.1 8B 와 같은 작은 파라미터 모델에서 두드러졌습니다. 처음 몇 단계의 깊이 증가가 가장 큰 향상을 가져왔습니다.
  • 검색 전략: KG 와 빔 검색 및 Best-of-N 샘플링을 결합하면 정확도가 더욱 향상되어 ProofNet 에서 10.75%, MUSTARDSAUCE 에서 **50.40%**를 달성했습니다.
  • 파인튜닝 모델: Lean 을 위해 이미 파인튜닝된 모델 (예: TheoremLlama, DeepSeek-Prover-V1.5) 에 적용되더라도 KG-Prover 는 추가적인 성능 향상을 제공했습니다 (예: miniF2F 에서 파인튜닝된 베이스라인 대비 +1.85%).

중요성 및 주장

본 논문은 KG-Prover가 추가적인 파인튜닝이나 집중적인 전문가 반복 없이 자동 정리 증명을 위한 유망하고 확장 가능한 접근법을 제공한다고 주장합니다. 일반 목적 LLM 의 내재된 자연어 추론 능력을 활용하고 구조화된 그래프 검색 정보를 통해 이를 보강함으로써, 이 프레임워크는 비형식적 추론과 형식적 검증 사이의 간격을 효과적으로 연결합니다.

저자들은 이 방법이 추론 중에 관련 개념을 주입함으로써 기존 기초 모델이 전문화된 파인튜닝 시스템과 동등하거나 더 높은 성능을 달성할 수 있게 한다고 강조합니다. 이 연구는 복잡한 추론 작업을 위한 모델 파라미터 확장의 대안으로 테스트 시간 컴퓨팅 확장—그래프 탐색 깊이 조절과 검색 전략 채택—의 잠재력을 부각시킵니다. 비록 이 접근법은 비형식적에서 형식적 번역 단계에서 도전을 제기하지만, 그래프 검색을 지원하는 2 에이전트 시스템 (생성 + 자동 형식화) 은 이러한 문제를 성공적으로 완화하여 해석 가능한 추론 흔적과 증명 생성을 위한 새로운 전략을 제공합니다.