Geometry of Reason: Spectral Signatures of Valid Mathematical Reasoning
Valentin Noël
cs.LG
Jan 2, 2026 · v2
cs.AI cs.CL cs.LO
TL;DR
Analyzes attention spectra of LLMs on Lean 4 MiniF2F proofs, using Lean compilation for labels and HFER reranking in Lean proof search.
Abstract
Verifying whether a language model is genuinely reasoning or pattern-matching remains an open problem: learned verifiers are expensive, and output-based heuristics are brittle. We show that valid mathematical reasoning induces a measurable, training-free spectral signature in transformer attention. By treating each attention matrix as a weighted token graph, we extract four diagnostics: Fiedler value, High-Frequency Energy Ratio (HFER), spectral entropy, and smoothness, that require no learned parameters. Experiments across seven models from four architectural families yield effect sizes up to Cohen's $d = 3.30$ ($p < 10^{-116}$), enabling $85$–$96\%$ single-threshold classification accuracy. Two findings sharpen the interpretation. First, Platonic validity: the spectral signal tracks logical coherence rather than compiler acceptance, proofs rejected for timeouts or missing imports are correctly classified as valid, a distinction confirmed by a manual audit ($κ= 0.82$, $n = 51$). Second, architectural determinism: Sliding Window Attention shifts the discriminative feature from HFER to smoothness ($d = 2.09$, $p < 10^{-48}$), showing that attention design governs which spectral channel encodes reasoning quality. Causal ablation confirms the signature traces induction-head circuits. The method generalises to informal chain-of-thought ($d = 0.78$, $p < 10^{-3}$), and in proof search, HFER reranking improves Best-of-16 Pass@1 by $+4.4$–$6.6$%, matching $98\%$ of the AUC of fully supervised probes with zero labels. Spectral graph analysis is a principled, architecture-aware primitive for reasoning verification.
Problem
It is hard to verify whether a language model's mathematical proof reflects valid reasoning. Learned verifiers are expensive. Compiler-based checking in Lean conflates logical validity with technical acceptance, since proofs can fail on timeouts or missing imports.
Approach
Each attention matrix is treated as a weighted token graph. The method symmetrizes the matrices, aggregates heads, and computes four parameter-free spectral diagnostics from the graph Laplacian: Fiedler value, high-frequency energy ratio (HFER), spectral entropy, and smoothness. These are evaluated on Lean 4 MiniF2F theorem-proof pairs (human-written valid proofs vs. model-generated invalid ones) across seven models from four families. Labels are corrected via manual audit of compiler-rejected but logically sound proofs, and HFER is also used to rerank Best-of-16 proof-search candidates.
Results
Single-threshold classification reaches 85.9–95.6% accuracy with effect sizes up to Cohen's d = 3.30. The signal tracks logical coherence rather than Lean acceptance (audit κ = 0.82), and sliding-window attention shifts the best feature to smoothness. HFER reranking improves Best-of-16 Pass@1 by 4.4–6.6% and reaches 98% of the AUC of supervised probes with zero labels.
| Model | Best Metric | abs(d) | Acc. |
|---|
| Llama-3.2-1B | Fiedler (L0) | 3.02 | 93.4% |
| Llama-3.1-8B | HFER (L30) | 3.00 | 94.1% |
| Qwen2.5-7B | HFER (L26) | 2.43 | 89.9% |
| Phi-3.5-mini | Smooth (L25) | 3.30 | 93.4% |
| Mistral-7B (SWA) | Smooth (L26) | 2.09 | 85.9% |
Best spectral discriminator per model on MiniF2F (Lean 4)