Research map / Learning theory and algorithms / Prediction and decision losses

Compact Proofs of Model Performance via Mechanistic Interpretability

NeurIPS 2024 · Learning theory and algorithms › Prediction and decision losses · approach: Active learning and subset selection · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Uses mechanistic interpretability of tiny one-layer attention-only transformers trained on Max-of-K to derive and compactly prove accuracy lower bounds, producing 102 proof strategies that trade off proof length against bound tightness.

Problem

Formal guarantees on global model performance usually come from brute-force checking or from architecture-level verification that scales poorly; the paper asks whether reverse-engineered mechanisms can yield compact, non-vacuous proofs of model accuracy.

Approach

Use the reverse-engineered QK, OV and direct-path circuits of a trained attention-only transformer to design computer-assisted proof strategies with pessimal ablation over unexplained parts; measure proof length (FLOPs, asymptotic complexity) against bound tightness and an "unexplained dimensionality" metric for mechanistic understanding.

Key results

• Cubic proof bounds accuracy at about 94.1% (std 1.1%) on Max-of-4 models while brute force gives about 99.9%, with far fewer FLOPs.
• Across 102 proof strategies on 151 models, more compact proofs yield looser bounds, and proof length is negatively correlated with mechanistic understanding (unexplained dimensionality).
• Cubic proof on Max-of-20 completes in under two minutes with a non-vacuous accuracy bound, whereas brute force would need about 10^23 times the cost of GPT-3 training.

Measured effects reported in the paper

Surprising findings

• Significantly compact proofs have vacuous accuracy bounds by default; compounding worst-case structureless errors across composed low-rank approximations make bounds trivial.

Limitations

• Studies only one-layer attention-only transformers on a toy algorithmic task; MLPs and layernorm not covered.
• The OV circuit could not be significantly compacted.
• Compounding structureless errors make many compact strategies yield vacuous bounds.

Experimental setup

Datasets: Max-of-K synthetic task (uniformly sampled integer sequences, vocab size 64)

Benchmarks: Max-of-4 (brute-force accuracy) Max-of-5 Max-of-10 Max-of-20

Metrics: accuracy lower bound bound tightness (bound / true accuracy) estimated FLOPs asymptotic complexity unexplained dimensionality

Baselines: brute-force proof cubic proof null proof

Builds on: brute-force verification path decomposition of transformers (Elhage et al.) PAC-Bayes generalization bounds

Closest papers by meaning

• Validating Mechanistic Interpretations: An Axiomatic Approach (ICML 2025 · similarity 0.88)
• Everything, Everywhere, All at Once: Is Mechanistic Interpretability Identifiable? (ICLR 2025 · similarity 0.86)
• Faithful Model Explanations through Energy-Constrained Conformal Counterfactuals (AAAI 2024 · similarity 0.85)
• FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence (NeurIPS 2026 · similarity 0.85)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.84)
• Mechanistic Circuit Identification for Controllable Data Generation (NeurIPS 2026 · similarity 0.84)