Names Don't Matter: Symbol-Invariant Transformer for Open-Vocabulary Learning

AI summary

Overview

Research area: Machine learning / neural architecture design for symbolic reasoning, specifically open-vocabulary generalization and invariance to variable renaming.

Technical level: Advanced. The paper defines alpha-equivalence formally, states and proves an invariance theorem, and modifies Transformer encoder–decoder internals (self-attention, cross-attention, projection, embedding tying).

Scope: The paper proposes a Transformer variant whose outputs are provably invariant to the renaming of interchangeable symbols, and evaluates it on propositional logic assignment prediction and Linear Temporal Logic (LTL) witness generation, including a comparison against GPT-5.2.

What This Paper Is About

Many symbolic systems contain tokens that are semantically interchangeable: renaming a bound variable or an atomic proposition does not change meaning (a property called alpha-equivalence). Neural models trained on fixed vocabularies tend to latch onto specific symbol identities, so they degrade when symbols are renamed and they have no representation at all for symbols unseen during training. The paper's goal is an architecture that is exactly invariant to such renaming by construction, rather than by data augmentation or statistical encouragement, while still being able to extend its vocabulary after training.

Key Contributions

1. Architecture. A symbol-invariant Transformer that maintains k parallel embedding streams, one per interchangeable token, processed by shared Transformer layers, plus an aggregated attention mechanism that fuses the streams into a single view. It introduces only a small number of additional hyperparameters and can be implemented as a lightweight modification of standard encoder–decoder Transformers.
2. Theory. A formal guarantee (Theorem 4.1, "Alpha-Renaming Invariance") that the model's prediction on an alpha-renamed input is the alpha-renamed version of its original prediction, i.e. f^{-1}(ŷ') = ŷ.
3. Empirics. Validation on open-vocabulary symbolic reasoning tasks, reporting state-of-the-art performance and perfect alpha-covariance, including outperforming GPT-5.2 on LTL witness generation.
4. Conversion recipe. A parameter-preserving procedure for turning an existing pre-trained vanilla Transformer into the proposed architecture with minimal fine-tuning (the paper reports results after 1 and 5 fine-tuning epochs).

Main Findings

• Perfect invariance in practice. The proposed method achieves 100.0% alpha-covariance at 3, 4, and 5 atomic propositions (APs) in every reported training regime (Normal and Reduced) on both propositional logic and LTL, validating Theorem 4.1.
• Propositional logic accuracy. Under Normal training, the proposed method reaches 98.03% correct and 60.96% exact match, versus 95.62%/57.94% for the Baseline, 93.85%/57.24% for Alpha-Renaming, and 93.25%/56.45% for Random Embedding. Under Reduced training (80K instead of 800K samples), it reaches 70.43%/35.81%, versus 63.26%/29.31% (Baseline), 57.48%/26.77% (Alpha-Renaming), and 55.23%/26.28% (Random Embedding).
• LTL accuracy. Under Normal training, the proposed method reaches 98.24% correct and 79.65% exact, versus 98.23%/83.23% (Baseline), 97.96%/77.66% (Alpha-Renaming), and 95.94%/76.45% (Random Embedding). Under Reduced training: 93.46%/68.63%, versus 87.47%/63.61%, 89.50%/64.15%, and 87.32%/59.04% respectively.
• Renaming hurts ordinary models. On the renamed propositional logic dataset, the Baseline collapses to 41.57% correct and 9.04% exact, with alpha-covariance of 14.96% (3 AP), 16.85% (4 AP), and 10.65% (5 AP). On renamed LTL, the Baseline drops to 34.13%/12.12%.
• The proposed method can beat a baseline trained on clean data. When trained on the renamed dataset, it surpasses the baseline trained on the unmodified dataset, which the authors interpret as a Pareto improvement in the bias-variance trade-off.
• GPT-5.2 comparison. GPT-5.2 achieves 99.73% correct but only 25.60% exact on propositional logic (alpha-covariance 42.97%/29.87%/1.03%), and 86.83% correct / 35.93% exact on LTL (alpha-covariance 81.76%/82.97%/77.56%). The paper states GPT-5.2 achieves 99.49% accuracy on propositional logic and only 81.45% on LTL, underperforming all other methods there.
• Latency of GPT-5.2. With medium reasoning effort, GPT-5.2 requires 10–90 seconds per sample, averaging 37 seconds on 387 LTL test samples, while the proposed method generates predictions nearly instantaneously on consumer-grade hardware.
• Top-N parity. The proposed model is on par with GPT-5.2 at top-10 and top-25 accuracy on propositional logic, achieving 99.03% and 99.54%.
• Ablation, propositional logic (heatmap accuracy). Best model 95.05%; +CA 92.66%; -CP+CA 28.51%; -EA 92.47%; -DA 84.48%; -EA-DA 72.35%; -EP 91.44%; -DP 46.55%.
• Ablation, LTL (heatmap accuracy). Best model 90.47%; +CA 90.27%; -CP+CA 20.93%; -EA 84.13%; +DA 89.47%; -EP 84.13%; -EP-DP+DA 20.27%.
• Per-stream cross-attention is critical. Replacing it with aggregated cross-attention causes catastrophic degradation (20.93% LTL, 28.51% propositional logic), worsening as the number of APs grows.
• Aggregated attention matters more for propositional logic. Removing DA drops propositional logic accuracy to 84.48%, while LTL slightly improves when DA is added (89.47% to 90.27%). The authors attribute this to relational reasoning being the bottleneck in propositional logic but not in LTL.
• Fine-tuning conversion works. On LTL, converted and fine-tuned models reach 94.75%/92.44%/85.91% (1 epoch) and 95.12%/92.02%/85.88% (5 epochs) on 5 AP validation / 10 AP validation / heatmap, comparable to or better than the from-scratch model (94.77%/91.34%/84.13%). On propositional logic, fine-tuning closes the gap (90.55%/68.78%/71.35% at 5 epochs versus 91.47%/69.97%/72.35% from scratch).
• Cost. Standard attention is O(L²); the proposed architecture is O(SL²) in time and O(SLd) in activation memory. For S=10, average time per sample increases from 3.38 ms to 5.13 ms on propositional logic. On the LTL heatmap, memory from 5 to 10 APs scales from 1.9 GB to 3.9 GB for the proposed method and 3.1 GB to 3.2 GB for the full vocabulary baseline, at batch size 64.
• Generalization setting. The heatmap test set varies AP count and formula length out of distribution, with at most 100 test samples per combination; the maximum test formula length is 50 versus a training maximum of 35, and the maximum test AP count is 10 versus a training maximum of 5.
• Stated limitations. Cost scales with the number of streams S, which is constrained by compute; domains such as program synthesis or theorem proving may involve hundreds of distinct local variables. The model cannot generate a fresh interchangeable token with no corresponding stream, so tasks such as constructive proof generation or code synthesis are out of scope.

Methodology in Plain English

The core idea is to stop asking one embedding table to both identify a symbol and represent its meaning. Instead, the model creates k parallel "views" of the input, one per interchangeable token. In the stream dedicated to token i, positions holding token i get an "actual" embedding, positions holding any other interchangeable token get a shared "placeholder" embedding, and ordinary tokens are left alone. A binary mask records where each token occurs so its true representation can be restored later.

Each stream runs through its own self-attention and feed-forward network, but all streams share the same weights. Because the weights are shared, the identity of a symbol never enters the computation: the streams are interchangeable, and renaming a symbol just permutes which stream carries it.

To let streams exchange information, the model averages their hidden states into one aggregated view, then restores each interchangeable token's specialized hidden state from its own stream at the positions where that token appears. The final projection follows the same pattern: logits for ordinary tokens are averaged across streams, while the logit for interchangeable token i comes from stream i. Encoder and decoder both use per-stream self-attention plus aggregated attention, and cross-attention can run per-stream or aggregated (the experiments show per-stream cross-attention is essential).

Training uses three-way weight tying between the decoder embedding, encoder embedding, and final projection, plus cosine loss with adaptive AdaCos scaling, following prior work. RoPE is the default positional mechanism, tree-positional encoding is used in the encoder for logic tasks, and beam search with beam width k=3 is used at generation. Evaluation covers a copying toy task, propositional logic assignment prediction built on PropRandom35 from DeepLTL, and LTL witness generation built on LTLRandom35, validated with pyaiger and spot 2.11.6. Robustness is measured with the alpha-covariance metric, computed over all alpha-equivalent permutations of 1000 test samples (100 for GPT-5.2).

Why This Matters

Impact on research. The paper offers invariance as an architectural guarantee rather than a statistical tendency. It contrasts with prior random-embedding approaches, which have no formal guarantee (different seeds can yield different predictions on alpha-equivalent inputs) and need hyperparameter tuning, and with prior provably invariant Transformers that did not consider vocabulary expansion. It also provides a conversion path so existing pre-trained models can gain the guarantee without discarding prior training.

Real-world applications (as discussed or implied in the paper):

• Formal verification of temporal system properties, where LTL formulas are written over atomic propositions that are interchangeable.
• Automated reasoning and theorem proving, where universally quantified variables and bound variables can be renamed freely.
• Program analysis and coding tools, where the paper notes LLM performance on coding tasks can degrade by up to 70% under semantics-preserving mutations such as variable renaming.
• Open-vocabulary symbolic tasks where test-time symbol sets exceed the training vocabulary, avoiding retraining on matching datasets as generation costs grow.

Industry relevance. Dataset synthesis for logic tasks scales steeply in empirical cost with AP count and formula length, and the LTL task is PSPACE-complete, so generalizing to larger AP sets and longer sequences without retraining is a practical scalability lever. The method also runs on consumer-grade hardware at milliseconds per sample, in contrast to GPT-5.2's 10–90 seconds per sample at medium reasoning effort.

Future Directions

• Managing stream cost. Sparsification to reduce O(SL²) time and O(SLd) memory while preserving alpha-equivalence, using input-symmetric criteria such as positional frequency or Top-K stream gating rather than identity-based dropping.
• Scaling to large variable sets. Extending tractability beyond the reported S ≤ 10 to domains with hundreds of distinct local variables, such as program synthesis or theorem proving.
• Generating fresh interchangeable tokens. Maintaining a reserved pool of fresh-symbol streams so the model can invent new variable names in constructive proof generation or code synthesis.
• Broader architectural adoption. Applying the conversion-and-fine-tuning procedure more widely and determining which tasks benefit from aggregated attention versus per-stream attention, since the best configuration was task-dependent (EP-DP-EA-DA-CP for propositional logic, EP-DP-EA-CP for LTL).

Target Audience

Researchers and engineers working on neural architectures for symbolic reasoning, formal verification, program analysis, or any sequence-to-sequence task involving bound variables, quantified variables, or atomic propositions. It is also relevant to practitioners who need models to generalize to symbol sets larger than those seen in training and who care about deployment cost relative to large general-purpose models. Readers without a background in Transformers, attention mechanisms, or formal logic notation will find the theory and ablations difficult.

Authors’ abstract

Current neural architectures lack a principled way to handle interchangeable tokens, i.e., symbols that are semantically equivalent yet distinguishable, such as bound variables. As a result, models trained on fixed vocabularies often struggle to generalize to unseen symbols, even when the underlying semantics remain unchanged. We propose a novel Transformer-based mechanism that is provably invariant to the renaming of interchangeable tokens. Our approach employs parallel embedding streams to isolate the contribution of each interchangeable token in the input, combined with an aggregated attention mechanism that enables structured information sharing across streams. Experimental results confirm the theoretical guarantees of our method and demonstrate substantial performance gains on open-vocabulary tasks that require generalization to novel symbols. Project page: https://bu-depend-lab.github.io/Symbol-Invariant-Transformer/