기술 요약: COMPOSE – 인용과 형식적 구조를 기반으로 한 미래 정리 구성

문제 정의

본 논문은 주어진 "앵커" 논문에 대해 타당한 미래 수학 주장 (정리 유사 진술) 을 예측하는 작업인 근거 기반 미래 수학 생성의 과제를 다룹니다. 저자들은 유효한 예측이 두 가지 동시 제약을 충족해야 한다고 주장합니다:

1. 과학적 궤적: 과학적 인용 그래프와 문헌 내 아이디어의 진화가 나타내는 연구 방향을 확장해야 합니다.
2. 형식적 근거: 기존 정의, 보조정리, 정의로부터 유효하게 유도될 수 있도록 형식 수학에 내재된 논리적 의존성을 존중해야 합니다.

기존 접근법은 일반적으로 이러한 소스 중 하나만을 모델링합니다. 과학적 텍스트만으로 훈련된 모델은 유창하지만 논리적으로 근거가 없는 주장을 생성할 수 있는 반면, 정리 증명 시스템은 형식적 구조에 대해 추론하지만 유망한 연구 방향을 식별할 과학적 맥락이 부족합니다. 본 논문은 과학 논문과 형식적 라이브러리 (Mathlib 등) 가 지식을 조직화하는 방식의 근본적인 차이로 인해 이러한 상호 보완적인 소스를 결합하는 것이 단순하지 않다고 주장합니다.

방법론: COMPOSE 프레임워크

저자들은 과학적 인용 맥락과 형식적 정리 구조 모두에 언어 모델을 조건부로 작용시키는 이중 그래프 프레임워크인 COMPOSE를 제안합니다. 이 접근법은 세 가지 주요 구성 요소로 이루어집니다:

1. 데이터 구축

저자들은 arXiv 수학 논문 (2000–2023) 과 Lean Mathlib 라이브러리에서 파생된 108,000 개의 쌍을 이루는 과학 - 형식 그래프 예제로 구성된 데이터셋을 구축했습니다.

• 과학 그래프 ($G_s$): 앵커 논문과 그 인용 맥락 (최대 2 홉) 으로 구축되었습니다. 여기에는 논문에 대한 초록 노드와 텍스트에서 추출된 정리 노드가 포함됩니다. 간선은 인용 링크와 논문 내부 의존성을 나타냅니다.
• 형식 그래프 ($G_f$): 추출된 비공식 정리를 Mathlib 의 해당 정리와 정렬하여 구성되었습니다. 이 정렬은 Mathlib 정리에 대한 인간이 작성한 비공식 설명 코퍼스인 FrenzyMath를 사용하여 비공식 - 비공식 검색을 수행함으로써 직접 자동 형식화의 노이즈를 피합니다. 형식 그래프는 LeanDojo 를 통해 추출된 의존성 간선을 사용하여 일치된 정리 루트에서 확장됩니다.
• 벤치마크: 2024 년 말과 2025 년의 실제 47,000 개의 미래 논문으로 구성된 시간적으로 홀드아웃된 테스트 세트로, 모델이 실제 출판된 결과를 예측하는 능력을 평가하는 데 사용됩니다.

2. 모델 아키텍처

COMPOSE 는 이중 인코더 아키텍처를 사용하고 그래프 조건부 디코더를 따릅니다:

• 이중 인코더: 두 개의 전용 그래프 신경망 (GNN) 이 $G_s$와 $G_f$를 별도로 처리합니다.
  • $G_s$ 노드는 E5 임베딩 (과학적 텍스트) 으로 초기화됩니다.
  • $G_f$ 노드는 DeepSeek-Math 임베딩 (형식적 서명) 으로 초기화됩니다.
  • 둘 다 게이트 잔여 연결을 가진 방향성 및 간선 유형별 메시지 전달을 사용합니다.
• 퓨전 모듈: 두 그래프의 표현은 공유 잠재 공간으로 투영되고 양방향 교차 주의 메커니즘을 통해 융합됩니다. 이를 통해 모델은 과학적 방향을 형식적 제약과 통합할 수 있습니다.
• 디코더: LoRA 로 적응된 사전 훈련된 수학 특화 LLM (DeepSeek-Math-7B 또는 Mistral-7B) 을 사용합니다. 교차 주의 레이어가 디코더에 삽입되어 융합된 그래프 임베딩에 생성을 조건부로 작용하게 하여, 토큰 생성 중 모델이 전체 그래프 구조에 주의를 기울일 수 있도록 합니다.

3. 2 단계 훈련

• 1 단계 (표현 학습): 디코더 없이 그래프 인코더와 퓨전 모듈을 다음 세 가지 목적 함수로 훈련합니다:
  • 링크 예측: 인코더가 그래프 구조를 포착하도록 보장합니다.
  • 대조적 정렬: 융합된 그래프 표현을 대상 논문의 초록과 주요 주장과 정렬합니다.
  • 교차 정렬: 비공식 정리 노드를 일치된 형식 대응물과 명시적으로 정렬합니다.
• 2 단계 (생성): 디코더를 추가하고 다음을 사용하여 미세 조정합니다:
  • 자기회귀 손실: 표준 다음 토큰 예측.
  • 그래프 마진 손실: 불일치하는 그래프 쌍에 대해 동일한 텍스트를 생성하는 경우 모델에 패널티를 부과하는 정규화 항으로, 모델이 특정 그래프 맥락에 의존하도록 강제합니다.

주요 결과

실험은 47K 미래 논문 벤치마크에서 수행되었으며, COMPOSE 를 GIANTS, FutureGen, GoAI 및 다양한 텍스트 전용 또는 프롬프트 전용 변형을 포함한 강력한 베이스라인과 비교했습니다.

• 검색 성능: COMPOSE 는 생성된 텍스트와 실제 미래 논문 사이의 코사인 유사도와 관련 없는 논문 사이의 차이로 정의된 가장 높은 Gap(0.240) 을 달성했습니다. H@10(50.8%) 및 H@100(80.8%) 에서 베이스라인을 크게 능가하여, 생성된 주장이 풀에서 올바른 미래 논문을 검색할 가능성이 훨씬 더 높음을 나타냅니다.
• 새로운 수학 주장 예측 (NMCP): COMPOSE 는 정밀도 (0.560) 와 일치도 (0.730) 에서 선두를 차지하여, 그 출력이 주제적 수준뿐만 아니라 형식적 및 비공식적 수준 모두에서 미래 정리와 정렬됨을 보여주었습니다.
• LLM 저자 평가: LLM 저자 (GPT-4.0) 가 내용, 깊이, 신규성, 정밀도, 구체성 측면에서 출력을 평가했습니다. COMPOSE 는 전체 점수 (3.36/5) 에서 가장 높은 점수를 달성했으며, 특히 기술적 깊이(3.52) 와 구체성(3.52) 에서 두드러졌습니다. 베이스라인이 종종 모호한 요약을 생성한 반면, COMPOSE 는 더 구체적이고 수학적으로 풍부한 출력을 생성했습니다.
• 절차 연구: 과학적 또는 형식적 그래프 인코더 중 하나를 제거하면 성능이 크게 저하되어 두 모달리티가 상호 보완적인 신호를 제공함을 확인했습니다. 형식적 그래프는 근거를 마련하는 데 결정적이었으며, 과학적 그래프는 올바른 연구 방향을 식별하는 데 필수적이었습니다.

중요성과 주장

본 논문은 미래 수학 생성이 과학적 맥락과 형식적 구조를 결합함으로써 혜택을 본다고 주장합니다.

• 근거 기반 생성: 저자들은 과학적 텍스트에만 의존하면 주제적 관련성은 있지만 논리적으로 근거가 없는 주장이 도출되는 반면, 형식적 구조에만 의존하면 새로운 방향을 예측하지 못한 채 알려진 정리로만 모델이 제한됨을 입증했습니다. COMPOSE 는 이러한 간극을 성공적으로 연결합니다.
• 데이터 기여: 108K 쌍을 이루는 데이터셋과 47K 미래 논문 벤치마크의 구축은 이 분야에서 시간적 벤치마크의 부재를 해결하는 근거 기반 수학 생성 평가를 위한 새로운 자원을 제공합니다.
• 방법론적 발전: 교차 주의 융합을 갖춘 이중 그래프 프레임워크는 생성 작업에 비공식 문헌과 형식 논리와 같은 이질적인 지식 소스를 통합하는 새로운 접근법을 제공합니다.

저자들은 방법론이 근사적인 비공식 - 형식 정렬에 의존한다는 한계 (Mathlib 커버리지가 희소한 영역에서 노이즈를 도입할 수 있음) 와 생성된 주장이 증명 도구에 의해 검증되지 않고 검색 및 LLM 기반 평가를 대리 신호로 사용한다는 점을 지적합니다. 그들은 향후 작업이 생성된 주장의 형식적 정확성을 직접 확인하기 위해 증명 인식 검증을 통합할 수 있음을 제안합니다.