LLM 증명자: 가짜 자연수 게임 (Obfuscated Natural Number Game) 을 통한 구조적 추론 능력 평가

대형 언어 모델 (Large Language Models, LLMs) 은 MiniF2F 와 같은 형식 수학 벤치마크에서 주목할 만한 성과를 이뤘지만, 이러한 결과가 진정한 논리적 추론을 비롯했는지 아니면 사전 학습 데이터에 대한 의미적 패턴 매칭 (semantic pattern matching) 을 비롯했는지는 아직 명확하지 않습니다. 본 논문은 미래 자동화된 정리 발견 AI 를 위한 필수 능력인 구조적 추론 (Architectural Reasoning) 을 식별합니다. 구조적 추론이란 외부 수학 도메인이 아닌, 외계 수학 도메인 (alien math domain) 내에서 국소 공리 및 정의만을 사용하여 형식 증명을 종합할 수 있는 능력을 의미합니다. 우리는 이를 평가하기 위해 가짜 자연수 게임 (Obfuscated Natural Number Game) 을 사용합니다. 이 벤치마크는 Lean 4 의 Natural Number Game 에서 식별자 (identifiers) 를 재명칭하여 제로 지식 (zero-knowledge), 폐쇄 환경 (closed environment) 을 만듭니다. 우리는 최첨단 모델들을 평가하여 가짜화 (obfuscation) 가 추론 시간을 증가시키는 보편적 지연세 (universal latency tax) 를 발견했습니다. 또한, 일반 모델 (Claude-Sonnet-4.5, GPT-4o) 은 성능 저하를 겪지만, 추론 모델 (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2) 은 의미적 단서 (semantic cues) 의 부재에도 불구하고 동일한 정확도를 유지하는 견고성 (robustness) 에서의 분기점을 발견했습니다. 이러한 결과는 수학 추론의 진정한 능력을 평가하는 정량적 지표 (quantitative metric) 를 제공합니다.