Sparse Autoencoders Are a Shared Coordinate System for Symbolic Matching
Xiaocong Yang, Xuanyu Meng, Yuji Zhang, Jiawei Han, ChengXiang Zhai
cs.LG
Oct 14, 2026 · v1
cs.AI cs.CL cs.SC
TL;DR
Uses Lean 4 miniF2F statements as queries for matching equivalent statements in Isabelle, Metamath and HOL Light, as part of the evaluation.
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.
Problem
Building large neuro-symbolic systems requires aligning heterogeneous symbolic systems. These include proof assistants, code, table schemas, knowledge graphs and ontologies. The first step is matching corresponding units across systems.
Approach
SAE-IDF feeds each symbol, in its native context, through an LLM. It encodes the residual-stream states with a pretrained sparse autoencoder, averages the resulting sparse codes, and re-weights each feature by inverse document frequency. Candidates are ranked by cosine similarity. One task family retrieves the counterpart of each Lean 4 miniF2F statement among the statements of another prover (Isabelle, Metamath, HOL Light), with names and proofs stripped.
Results
With Gemma-2-9B, SAE-IDF beats the same model's dense state on all 12 tasks. With Llama-3.1-8B it wins on all but one. The largest gain is +0.45 MRR on Lean 4 to Metamath. Ablations show that both the learned SAE dictionary and the idf weighting are needed. Dedicated trained retrievers still lead on the formal-mathematics pairs.
| Task | Strings | Dense | Dense, PC1 rm. | SAE-IDF |
|---|
| Lean 4 → Isabelle | 0.825 | 0.912 | 0.926 | 0.961 |
| Lean 4 → Metamath | 0.615 | 0.210 | 0.151 | 0.661 |
| Lean 4 → HOL Light | 0.741 | 0.539 | 0.531 | 0.898 |
miniF2F cross-prover matching MRR (Gemma-2-9B, layer 20)