Geometry of Reason: Spectral Signatures of Valid Mathematical Reasoning

Motivation

Known: 기존 reasoning 검증법은 크게 두 갈래로, Lean/Coq/Isabelle 같은 formal proof assistant를 통한 output 기반 검증과, model internals나 output feature에 학습된 classifier(probe)를 활용하는 learned verification이 있다. Attention 패턴을 induction head 등 mechanistic interpretability 관점에서 분석하는 연구, 그리고 spectral graph theory를 신경망에 적용하는 연구(spectral graph convolution, over-smoothing 분석, Attention Graphs)도 존재한다.
Gap: Output 기반 검증은 논리적 타당성과 컴파일 성공 여부(syntactic acceptability)를 혼동하여 timeout이나 import 누락으로 정당한 증명도 기각시키는 문제가 있고, learned verification은 대량의 라벨 데이터가 필요하며 아키텍처 간 일반화가 어렵고 spurious correlation을 학습할 위험이 있다. 학습 파라미터 없이 아키텍처에 무관하게 작동하는 원리적인(training-free) reasoning validity 진단 방법이 부재했다.
Why: 추론 검증은 자동 정리 증명, 수학 교육, 과학적 발견 등 고위험(high-stakes) 응용에서 탐지되지 않은 오류가 전파될 수 있는 중요한 문제이며, 학습된 verifier는 비용이 크고 output 기반 휴리스틱은 취약하기 때문에 training-free이면서 아키텍처를 인식하는(architecture-aware) 원리적 대안이 실용적·이론적으로 큰 가치를 지닌다.
Approach: 각 attention matrix를 가중 토큰 그래프로 취급하고 Graph Laplacian L=D-1/2(A+A^T)의 스펙트럼 특성(Fiedler value, HFER, spectral entropy, smoothness)을 학습 파라미터 없이 추출하여 valid/invalid proof를 구분하는 diagnostics로 사용한다.

Achievement

Figure 5. Architectural Determinism of Validity. Comparing Llama-3.1-8B (Global Attention) and Mistral-7B (Sliding Windo

Training-free 분류 프레임워크: attention graph의 spectral analysis만으로 nested cross-validation 하에서 82.8-85.9%, calibrated threshold로는 최대 95.6%의 정확도를 달성.
아키텍처 보편성(cross-architecture universality) 입증: 4개 architectural family에 속한 7개 모델에서 |d|≥2.09, p<10^-47을 일관되게 확인하고 난이도 계층 전반(복잡한 증명 d≥1.31)에서도 견고함을 보임.
Platonic validity 발견: 스펙트럼 신호가 compiler acceptance가 아니라 실제 logical coherence를 추적함을 발견 (timeout·import 누락으로 기각된 증명도 valid로 정확히 분류, manual audit κ=0.82).
Architectural determinism 발견: Sliding Window Attention에서는 discriminative feature가 HFER에서 smoothness로 이동함(d=2.09)을 보여, attention 설계가 reasoning quality를 encoding하는 spectral channel을 결정함을 규명.
인과적 검증(causal ablation): 신호가 induction-head circuit에서 비롯됨을 확인, informal chain-of-thought로 일반화(d=0.78)하고 proof search에서 HFER reranking으로 Best-of-16 Pass@1을 +4.4-6.6% 개선하며 fully supervised probe AUC의 98%에 zero-label로 도달.

How

Figure 6. Layer-wise spectral metrics (Combined) for Llama 3.2 1B Instruct.

Attention matrix A^(ℓ,h)를 directed weighted graph의 adjacency로 해석하고 대칭화하여 Graph Laplacian L=D-1/2(A+A^T) 구성
Laplacian의 고유값·고유벡터로부터 Fiedler value(algebraic connectivity), High-Frequency Energy Ratio(HFER), spectral entropy, smoothness의 4가지 diagnostics 추출
7개 모델(4개 architectural family: 예 Llama-3.1-8B의 Global attention vs Sliding Window Attention 모델 등)에 대해 layer-wise/head-wise로 spectral metric을 계산하고 Cohen's d, Mann-Whitney p-value로 valid/invalid 증명 그룹 간 효과크기 측정
단일 threshold 분류기와 nested cross-validation으로 정확도 평가, calibrated threshold로 성능 개선
Formal proof assistant의 기각 사유(timeout, missing import 등)를 수동으로 audit(κ=0.82, n=51)하여 Platonic validity 검증
Causal ablation으로 induction head를 제거/개입하여 spectral signature와의 인과관계 확인
Informal chain-of-thought 데이터로 방법 일반화 테스트, proof search에서 HFER 기반 reranking을 Best-of-16 Pass@1 개선에 적용하고 supervised probe와 AUC 비교

Originality

Attention matrix를 weighted token graph로 보고 spectral graph theory(Laplacian eigen-analysis)를 reasoning validity 검증에 직접 적용한 최초의 training-free 접근
Compiler acceptance와 logical coherence를 분리해 "Platonic validity"라는 개념을 실증적으로 정의하고 manual audit으로 검증
Sliding Window Attention 등 아키텍처 차이가 discriminative spectral channel(HFER↔smoothness)을 결정한다는 "architectural determinism" 현상을 발견
순수 output 기반이나 학습된 probe에 의존하지 않고, 인과적 ablation을 통해 induction-head circuit과 spectral signature를 연결한 mechanistic 설명 제공

Limitation & Further Study

실험이 수학 증명(주로 formal/informal proof) 도메인에 집중되어 있어, 일반적인 자연어 추론이나 다단계 계획(planning) task로의 일반화는 추가 검증 필요
4개 architectural family, 7개 모델로 한정되어 있어 더 다양한 규모(초대형 모델)나 최신 아키텍처(MoE, 매우 긴 context 등)에 대한 검증이 부족
Manual audit 표본이 n=51로 비교적 작아 Platonic validity 결론의 통계적 강건성에 한계가 있을 수 있음
Threshold 기반 단일 분류기가 특정 모델·태스크에 과적합될 위험이 있으며, 실제 배포 환경에서 threshold의 안정성에 대한 추가 검증이 필요
Causal ablation이 induction head에 집중되어 있어 다른 circuit(예: attention sink, retrieval head 등)과의 상호작용 분석이 부족

같이 보면 좋은 논문

Generative language modeling for automated theorem proving

기반 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Generative language modeling for automated theorem proving'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.

Large Language Models

기반 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 LLM Benchmarking and Agent Evaluation가 맞닿아, 'Large Language Models'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.

Towards large language models as copilots for theorem proving in lean

기반 연구SPECTER2 유사도 0.93로 LLM Reasoning and Safety Benchmarks와 Formal Methods and Computational Reasoning가 맞닿아, 'Towards large language models as copilots for theorem proving in lean'가 이 ICML 2026 논문의 배경·대안·응용 맥락을 보완한다.

Multiple-Comparison Testing for Cross-Validation Path Optimization Benchmarks: A Hessian-Mismatch Diagnostic for Holm--Bonferroni Failure Modes

기반 연구attention 구조 분석을 통한 모델 내부 표상 해석의 방법론적 토대를 제공한다.

TorchLean: Formalizing Neural Networks in Lean

기반 연구Lean 기반 프로그램 검증을 신경망 훈련 파이프라인에 적용하는 사례로 연결된다.

Divide and Abstract: Autoformalization via Decomposition and Abstraction Learning

기반 연구계층적 분해 기법을 확장하여 적용하는 후속 연구로 추정된다.

How Should Transformers Encode Numeric Values in Electronic Health Records?

기반 연구임상 예측 과제에서 transformer 인코딩 방식을 확장 검증한다.

Behavior Is Not Representation: Hypothesis Tests for Concept Steering in LLMs

다른 접근추론 타당성 판별을 위한 다른 형태의 내부 신호 기반 지표를 사용한다.

Detecting Hidden Chain-of-Thought in Large Language Models With Linguistic, Behavioral, and Mechanistic Indicators

다른 접근학습 없이 LLM 추론 품질을 평가하는 유사한 training-free 접근법을 제안한다.