Sparse Autoencoders Are a Shared Coordinate System for Symbolic Matching

AI summary

Overview

Research area: Interpretability and neuro-symbolic AI — specifically using sparse autoencoders (SAEs) trained on large language model (LLM) internals to perform symbolic matching: deciding which symbol in one structured system corresponds to a symbol in another.

Technical level: Intermediate (the pipeline is simple — encode, weight, cosine — but assumes familiarity with residual streams, SAEs, and IR-style weighting).

Scope (one sentence): The paper proposes SAE-IDF, a training-free method that encodes a symbol in its native context into an SAE feature code, weights features by rarity, and matches symbols by cosine across 12 tasks spanning six kinds of symbolic system.

What This Paper Is About

Symbolic systems (proof assistants, knowledge graphs, ontologies, table schemas, codebases) each describe knowledge in their own schema, so the same concept appears under different names — TrainStation in one knowledge graph and RailwayStation in another. Building a general neuro-symbolic model at LLM scale requires reusing these existing systems rather than hand-building one, and the first step is automatically matching units across them. The paper asks whether an LLM's sparse feature dictionary can serve as a shared coordinate system for that matching, so that a match can be computed without any aligned training pairs and then read off as named concepts.

Key Contributions

1. SAE-IDF, a training-free, general, and interpretable matching method: the LLM reads each symbol in its native context, a sparse autoencoder encodes the residual stream into a sparse code, each code dimension is re-weighted by its inverse document frequency, and candidates are ranked by cosine similarity.
2. Broad empirical validation: 12 tasks across 6 kinds of symbolic system (formal mathematics, code, table schemas, knowledge graphs, cross-lingual ontologies, biomedical ontologies), beating the same model's dense hidden state on every task with Gemma-2-9B and on 13 of 14 metric rows with Llama-3.1-8B.
3. Ablations isolating the two ingredients (the learned SAE dictionary and the rarity weighting), plus sweeps over SAE layer, dictionary width, sparsity, model size (2B–27B) and a second model family — 39 configurations, 78 runs.
4. A feature-level interpretability analysis with rule-selected case studies, an externally-labelled feature taxonomy (Neuronpedia explanations), a Valentine column-type split, and a four-prover merge test using transitivity, purity and adjusted Rand index.

Main Findings

• Consistent gains over dense hidden states: With Gemma-2-9B at layer 20 and a 131k-feature Gemma Scope SAE, SAE-IDF beats the model's dense state on all 12 tasks, by up to +0.45 MRR (Lean 4 → Metamath: 0.210 dense vs. 0.661 SAE-IDF). With Llama-3.1-8B at layer 15 and Llama Scope, it wins on 13 of 14 metric rows, the exception being XLCoST MRR (−0.01).

• Gain size tracks notational distance: Isabelle resembles Lean 4, so the gain is small (0.912 → 0.961); Metamath and HOL Light look very different, and dense collapses to 0.210 and 0.539 where SAE-IDF keeps 0.661 and 0.898. XLCoST programs share identifiers across languages, so word TF-IDF is strong (0.468) and SAE-IDF gains only +0.01.

• Both ingredients are necessary: Without IDF weighting, the sparse code alone trails dense on 15 of 18 main-table comparisons and leads by at most 0.012 on the other three. A random dictionary of the same width and sparsity with the same IDF stays below dense on every task (e.g., 0.146 on Metamath and 0.349 on HOL Light, versus dense's 0.210 and 0.539).

• Robust across configurations: Across 39 configurations SAE-IDF beats both dense and Dense−PC1 on Lean 4 → HOL Light and → Metamath, by +0.18 to +0.55 MRR over dense on HOL Light and +0.08 to +0.58 on Metamath, and beats the unweighted code in all 78 runs by +0.11 to +0.66. HOL Light MRR rises from 0.817 at a 16k dictionary to 0.935 at 1M; Metamath levels off from 65k.

• Scaling with model size: HOL Light MRR rises from 0.87 to 0.94 and Metamath from 0.65 to 0.74 across Gemma-2-2B, 9B and 27B; Gemma-2-27B reaches 0.939 and 0.738 against dense 0.41 and 0.20.

• Matches decompose into named concepts: A single feature ("mathematical or programming notation", f106376, active on 99% of Pile tokens) is among the five largest contributions in 99% of correct unweighted matches and in none under SAE-IDF. Features active on more than 1% of the Pile carry 56–91% of the unweighted cosine but only 0–6% with rarity weighting, measured over 2,315 correct matches on ten tasks.

• Two interpretability regimes: On knowledge-graph and ontology terms, 87–94% of the cosine comes from features active on under 0.1% of the Pile; on MultiFarm, about a quarter comes from surface features firing on both the foreign term and its English counterpart.

• Better merges: Linking the four miniF2F provers by mutual top-1 matches over twelve ordered pairs, SAE-IDF links almost twice as many statements as dense (coverage 0.639 vs. 0.340) at equal or higher consistency (transitivity 0.981 vs. 0.963; purity 0.981 vs. 0.979), and its merged components come closest to the true 489 problems (adjusted Rand index 0.795 vs. 0.519; 758 components vs. 1,096).

• Usable confidence for abstention: At 90% precision, SAE-IDF answers 24% of Metamath and 93% of HOL Light queries, against 1% and 24% for dense.

• Competitive with trained retrievers: It beats BGE-M3 on 10 of 15 rows and leads Qwen3-Embedding-8B on code, YAGO → Wikidata, MultiFarm Arabic and Bio-ML, while trailing on 8 rows, mainly formal mathematics where Qwen3 reaches 0.97–0.99 MRR — which the authors attribute to possible memorization of these long-public benchmarks.

Methodology in Plain English

Take a symbol — say a Lean theorem, a table column, or a knowledge-graph class — and gather the views the system already records for it: the statement itself, the term's axioms, sixteen sampled cell values, up to sixteen class instances. Wrap each view in a short template: context first, the symbol's label last.

Run that text through an open LLM and, at one chosen layer, read the residual-stream activations at the symbol's own token positions. Earlier tokens have already mixed their information into those positions through attention, so the symbol's state carries its context.

Pass each state through a sparse autoencoder for that layer. The SAE writes a dense vector as a sparse, non-negative combination of interpretable dictionary features — in effect a bag of named concepts. Average the codes over tokens and over views to get one sparse vector per symbol.

Then apply classic text-retrieval logic: count how many symbols in a reference collection each feature fires on, and down-weight features that fire everywhere (an inverse document frequency, floored at zero) while amplifying rare ones. Match by cosine similarity, which decomposes exactly into per-feature contributions, so every match can be explained by which features carried it.

The baselines use the exact same texts and token positions: the raw dense hidden state, a dense state with the first principal component removed, and the unweighted SAE code.

Why This Matters

Impact on research. The paper reframes an LLM's SAE dictionary as reusable infrastructure: a coordinate system in which symbols from unrelated formalisms become comparable without any alignment training data. That reframes SAE interpretability work from "explaining a model" to "doing useful work with a model's internals," and it positions cross-system matching as the foundational step toward a general neuro-symbolic backbone rather than a benchmark-specific engineering task.

Real-world applications:

• Biomedical ontology harmonization — the paper evaluates NCIT → DOID and mouse → human anatomy, the kind of alignment that underlies clinical data integration.
• Enterprise data catalog and schema integration — Valentine covers joinable and unionable table pairs, i.e., automatic schema matching across databases.
• Cross-language code retrieval and migration — XLCoST matches programs across Java, C++, Python, C#, JavaScript, PHP and C.
• Multilingual knowledge-base merging — MultiFarm matches Chinese, Russian and Arabic terms against English terms from a different conference ontology.
• Verifiable math library migration — moving problems between Lean 4, Isabelle, Metamath and HOL Light while preserving identity of statements.

Industry relevance. The method needs no training and no labelled pairs, so it inherits every future SAE release at zero cost — and

Authors’ abstract

Large language models (LLMs) hold broad knowledge in one set of weights, but lack interpretability and trustworthy reasoning, especially in high-stakes use cases. A neuro-symbolic model, with its interpretable architecture and System 2 reasoning capacity, is a promising alternative if built at the scale of LLMs; however, its symbolic backbone is usually constructed with human effort, so existing neuro-symbolic models are bottlenecked by the scope of the symbol component and usually domain-specific. A data-driven method could instead build a larger symbolic system by aligning and merging existing ones. We target its first, foundational step: matching units across these heterogeneous systems. Our method, SAE-IDF, encodes a symbol in its native context into a sparse code with a sparse autoencoder (SAE), re-weights each dimension by its rarity and matches across systems. On 12 tasks across 6 kinds of symbolic system, SAE-IDF outperforms the same LLM's dense baseline on all tasks with Gemma-2-9B and all but one with Llama-3.1-8B, by up to 45 points, consistently across SAE layers and configurations. SAE-IDF is also interpretable: every dimension of the sparse code has a human-readable meaning, so each match decomposes into named concepts (features). Our work paves the way to a universal symbolic backbone.