Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

"Obfuscated Natural Number Game 를 통한 LLM 증명자의 아키텍처 추론 능력 평가"에 대한 상세한 기술 요약입니다.

1. 문제 제기

MiniF2F 와 PutnamBench 와 같은 형식 수학 벤치마크에서 대규모 언어 모델 (LLM) 의 성공에도 불구하고, 중요한 모호성이 남아 있습니다: 이러한 모델들은 진정한 논리적 추론 능력을 갖추고 있는 것일까요, 아니면 단순히 사전 학습 데이터에 대한 의미적 패턴 매칭을 수행하는 것일까요?

• 격차: 현재 벤치마크는 종종 Mathlib 과 같은 라이브러리 검색에 의존하며, 성공은 고차원 보조정리 (lemmas) 와 의미 식별자 (예: add, succ) 를 인식하는지에 달려 있습니다. 이는 외부 라이브러리나 친숙한 의미적 단서가 존재하지 않는 "이질적인" 수학 영역에서 증명을 종합하는 모델의 능력을 테스트하지 못합니다.
• 필요성: 자동화된 정리 발견을 달성하기 위해, AI 는 외부 라이브러리나 의미적 의미에 독립적으로 오직 국소적 공리, 정의, 그리고 구조적 논리만을 사용하여 형식적 증명을 종합할 수 있는 **아키텍처 추론 (Architectural Reasoning)**을 입증해야 합니다.

2. 방법론

저자들은 의미적 검색에서 구조적 추론을 분리하도록 설계된 영지식 (zero-knowledge) 벤치마크인 **Obfuscated Natural Number Game(O-NNG)**을 소개합니다.

A. 난독화 알고리즘

핵심 혁신은 Lean 4 의 Natural Number Game(NNG) 에서 의미적 단서를 체계적으로 제거하는 것입니다:

• 잡음 수준 ($\lambda$): $[0, 1]$ 범위로 정의됩니다.
  • $\lambda = 0$: 원래 NNG(의미 식별자 intact).
  • $\lambda = 1.0$: 식별자의 완전한 무작위화.
• 교란 메커니즘: 지수 관계식 $P = \lambda^{2.5}$가 문자 단위 교란의 확률을 결정합니다.
  • 대체: 유효한 Unicode/ASCII 후보로 문자를 교체합니다.
  • 삽입: 새로운 문자를 주입합니다 (확률 $0.4P$).
  • 삭제: 문자를 제거합니다 (확률 $0.3P$), 식별자가 비어있지 않도록 보장합니다.
• 목표: 이 과정은 식별자 (예: 공리, 정리, 전술) 가 무작위 문자열이 되는 "폐쇄 환경"으로 데이터셋을 변환하여, 모델이 페아노 공리의 논리적 구조에만 의존하도록 강제합니다.

B. 실험 설정

• 데이터셋: 8 개 모듈 (덧셈, 곱셈 등) 로 구성된 NNG 의 68 개 형식적 문제.
• 평가된 모델: API 를 통한 다섯 가지 최첨단 모델:
  • 추론 모델: DeepSeek-R1, GPT-5, DeepSeek-Prover-V2.
  • 일반 모델: GPT-4o, Claude-Sonnet-4.5.
• 파이프라인:
  1. 파싱: 엄격한 의존성 순서로 NNG 추출.
  2. 난독화: $\lambda$를 기반으로 문자 단위 교란 적용.
  3. 쿼리 생성: "이질적인" 공리, 대상 정리, 사용 가능한 전술을 포함하는 프롬프트 구성.
  4. 추론: 모델이 자연어 계획 ("Draft") 과 Lean 4 코드 ("Code") 가 포함된 JSON 을 출력.
  5. 검증: 구문 및 논리 오류를 확인하기 위해 Lean 4 컴파일러 (v4.27.0) 를 사용한 자동화 검증.
• 지표:
  • 정답률 (%): 성공적으로 증명된 정리의 비율.
  • 평균 시간 (초): 추론 지연 시간.

3. 주요 기여

1. 아키텍처 추론의 정의: 외부 라이브러리와 고차원 자동화 전술 (예: linarith) 을 배제하고 폐쇄된 이론 내에서 오직 국소적 정의와 공리만을 사용하여 증명을 종합하는 능력으로 공식화.
2. O-NNG 벤치마크: 의미 식별자가 제거되었을 때 성능 저하를 측정함으로써 "의미 - 추론 격차"를 정량화하는 새로운 영지식 평가 프레임워크.
3. "지연 세 (Latency Tax)"의 정량화: 이질적 영역을 탐색하는 것이 아키텍처와 무관하게 모든 모델에 보편적인 계산 비용 (증가된 추론 시간) 을 부과한다는 것을 확립.

4. 결과 및 분석

이 연구는 의미적 단서가 제거되었을 때 모델 행동의 급격한 분기를 드러냅니다:

• 보편적 지연 세:

  • 모든 모델은 $\lambda$가 증가함에 따라 통계적으로 유의미한 추론 시간 증가를 보였습니다.
  • 함의: 의미 식별자를 제거하면 모델들의 기본 능력과 무관하게 더 집중적인 내부 검색이나 논리적 재구성을 수행하도록 강제합니다.

• 견고성 (정확도) 의 분기:

  • 추론 모델 (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2): 모든 잡음 수준 ($\lambda \in [0, 1]$) 에서 안정적인 정확도를 유지했습니다. 성능 저하는 통계적으로 유의미하지 않았습니다.
    • 결론: 이러한 모델들은 구조적 논리에 의존하며 의미적 앵커 없이 페아노 공리를 탐색할 수 있습니다.
  • 일반 모델 (GPT-4o, Claude-Sonnet-4.5): $\lambda$가 증가함에 따라 성공률이 통계적으로 유의미하게 감소했습니다.
    • 결론: 이들의 표준 형식 작업 수행 능력은 순수 논리적 종합보다는 의미적 패턴 매칭과 명명 규칙에 대한 친숙함에 크게 의존합니다.

• 통계적 유의성: 일원 분산 분석 (One-Way ANOVA) 은 일반 모델의 성능 저하와 모든 모델의 지연 시간 증가가 통계적으로 유의미함 ($p < 0.05$) 을 확인했습니다.

5. 중요성 및 함의

• 진정한 추론의 벤치마킹: O-NNG 는 패턴 매칭을 통해 수학을 "아는" 모델과 구조적 논리를 통해 "추론"할 수 있는 모델을 구분하는 엄격한 지표를 제공합니다.
• 아키텍처 방향성: 자동화된 정리 발견 (AI4Math) 의 미래를 위해, 의미적 사전 지식의 부재에 견고한 추론 중심 아키텍처(DeepSeek-R1 및 GPT-5 와 같은) 가 범용 모델보다 우수하다는 결과가 시사됩니다.
• "추론의 언캐니 밸리": 데이터는 부분적 잡음이 완전한 난독화보다 더 해로울 수 있는 비선형 관계를 암시하며, 잔류 의미적 단서가 방해가 되는 휴리스틱으로 작용할 수 있음을 시사합니다.
• 미래 AI 에이전트: 이 발견은 불완전하거나 모호한 온톨로지를 가진 영역에서 작동할 수 있는 "지식 기반 의미 에이전트"의 개발을 옹호하며, 이는 새로운 수학 정리를 발견하기 위한 전제 조건입니다.

요약하자면, 이 논문은 현재 LLM 들이 패턴 매칭을 통해 알려진 문제를 해결할 수는 있지만, 완전히 낯설고 난독화된 논리적 환경에서 문제를 해결하는 데 필요한 아키텍처 추론을 갖춘 것은 특정 "추론" 아키텍처뿐임을 입증합니다.