Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
Interchangeable Token Embeddings combine shared semantics with random identity, reaching 95.94% LTL correctness and extending vocabularies.
Key Findings
Methodology
The method decomposes token embeddings into a shared learnable component α and a randomized identity component βi. Non-interchangeable tokens use learned vectors, while interchangeable tokens concatenate the same α with distinct βi. βi is resampled at every training forward pass and fixed once at inference. The system uses three-way weight tying, L2 normalization of embeddings and features, and a sequence-adapted AdaCos objective.
Key Results
- In copying, 10 million random strings were generated with length at most 80 and at most 20 unique characters. Fixed learned embeddings failed on unseen characters, whereas the proposed model generalized nearly perfectly to joint vocabulary-size and length settings approaching 160.
- On LTLRandom35, the proposed model achieved 95.94% correct predictions and 76.45% exact matches. Under 3-, 4-, and 5-AP alpha-equivalence tests, alpha-covariance was 97.66%, 97.76%, and 98.29%, respectively.
- The alpha-renaming baseline reached 97.96% correctness and 77.66% exact match, with alpha-covariance of 99.55%, 99.49%, and 98.86%. The proposed model was slightly less invariant but generated unseen-token embeddings without explicitly learning the expanded vocabulary.
Significance
The paper turns a long-standing weakness of formal language models into an explicit representation-learning problem: symbols can be semantically interchangeable yet individually addressable. This matters for LTL, propositional logic, lambda calculus, program analysis, and proof generation. In practical verification systems, new atomic propositions need not automatically trigger reconstruction of a fixed embedding table.
Technical Contribution
The work contributes alpha-covariance, a structured extendable embedding matrix, and a compatible Transformer encoder-decoder training recipe. The random component is not ordinary augmentation: it provides identity while shared parameters encode category-level semantics. Resampling forces invariance to random-code idiosyncrasies. The authors also adapt AdaCos to language modeling by flattening batch and sequence dimensions, ignoring padding, and clipping its scale at 100.
Novelty
Most language models assign independent parameters to every symbol; alpha-renaming is typically treated as data augmentation. This paper formally defines extendable vocabulary generalization for interchangeable tokens and builds the desired inductive bias into the embedding generator itself. Its central innovation is the simultaneous enforcement of semantic sharing and token distinguishability, rather than merely exposing a model to more names.
Limitations
- Discrete random-vector families grow exponentially with dβ. The Neighboring Points and Hypercube Vertices implementations require uniqueness management, and integer-based reservoir sampling becomes problematic beyond 32 dimensions.
- Experiments focus on synthetic copying, LTL, and propositional logic. Natural-language entities are only conditionally interchangeable, so the method's direct applicability to ordinary language remains untested.
- Alpha-covariance measures consistency, not correctness; a model can be consistently wrong across every renamed instance.
Future Work
Future work should study multiple interchangeable-token classes, hash-based or continuous identity codes, larger language models, and real code or proof corpora. A unified benchmark should jointly report correctness, exact match, alpha-covariance, memory, and sampling cost. The effects of dα, dβ, generator choice, and positional encoding also warrant systematic theoretical and empirical analysis.
AI Executive Summary
Transformers now solve symbolic integration, theorem-proving subproblems, and linear temporal logic, but their vocabularies are usually closed. A symbol absent during training cannot be embedded directly. More fundamentally, formal systems contain interchangeable names: renaming a bound variable preserves meaning, yet ordinary embeddings treat every name as unrelated. This blocks systematic vocabulary expansion and alpha-equivalence.
Işık, Cinbis, and Gol propose Interchangeable Token Embeddings. Each interchangeable token receives a shared learnable vector α, representing common semantics, plus a randomly generated vector βi, preserving identity. Resampling βi during training prevents memorization of a particular code; fixing it during inference ensures consistent autoregressive decoding. The method uses Transformer encoder-decoder models, RoPE, tree-positional encoding, three-way weight tying, and a sequence adaptation of AdaCos.
The copying benchmark shows nearly perfect extrapolation from at most 20 characters and length 80 to settings approaching 160 in both dimensions. On LTLRandom35, the model obtains 95.94% correctness and 76.45% exact match, with alpha-covariance above 97.6% for three to five atomic propositions. The approach still faces scalability and domain-transfer limits, but establishes a practical foundation for expandable, permutation-aware formal reasoning.
Deep Analysis
Background
Transformers have been applied to symbolic integration, symbolic regression, and LTL solving. Hahn et al. showed that tree-positional encoding supports length generalization, while classical tools such as spot and aalta solve LTL through established algorithms. Yet neural models normally treat every atomic proposition, variable, or symbol as a fixed vocabulary item. The same weakness appears in lambda calculus and mathematical expressions, where alpha-equivalent renamings preserve semantics.
Core Problem
Let V=Vi∪Vn, where Vi contains interchangeable tokens and Vn contains non-interchangeable tokens. Any bijection f that permutes Vi while fixing Vn should transform an input-output pair (a,b) into a semantically equivalent pair (a′,b′). The model must both remain correct under these alpha-conversions and operate after training on V with an expanded vocabulary V′ containing unseen members of Vi.
Innovation
The paper introduces three connected innovations. First, it defines an experimental protocol for vocabulary expansion with interchangeable symbols. Second, alpha-covariance measures whether predictions from all renamed variants become identical after inverse conversion. Third, the dual-part embedding combines a shared semantic vector with a random identity vector. Unlike fixed embeddings or alpha-renaming augmentation, this mechanism generates new identities at inference while structurally encoding the desired inductive bias.
Methodology
- �� Embedding construction: learned regular-token matrix L has n rows and dα columns; interchangeable tokens share α∈R^(1×dα) and receive βi∈R^(1×dβ), with dmodel=dα+dβ.
- �� Random generation: βi comes from Normal Distribution, Neighboring Points {-1,0,1}, or Hypercube Vertices {-1,1}; finite sets use reservoir sampling for uniqueness.
- �� Training: reconstruct and resample the embedding matrix every forward pass, preventing dependence on one random realization.
- �� Projection: tie encoder, decoder, and output projection weights; normalize embedding rows and feature vectors with L2 normalization.
- �� Objective and positions: use sequence-adapted AdaCos, flattening valid batch-length positions and clipping scale at 100; use tree positions for logic encoders and RoPE elsewhere.
Experiments
All experiments use Transformer encoder-decoder models. Tasks are extendable-vocabulary copying with 10 million strings, DeepLTL's LTLRandom35 plus matched synthetic datasets, and propositional-logic assignment prediction. Baselines include standard embeddings on the original vocabulary, standard embeddings on a larger vocabulary, and random alpha-renaming augmentation. LTL outputs are checked by spot 2.11.6 with beam size 3; metrics are correctness, exact match, and alpha-covariance.
Results
Fixed embeddings cannot extrapolate to unseen copying characters, while the proposed model is nearly flawless for vocabulary and length scales approaching 160. On LTLRandom35, the normal baseline scores 98.23% correct and 83.23% exact; the perturbed baseline falls to 34.13% and 12.12%. Alpha-renaming scores 97.96% and 77.66%, while the proposed method scores 95.94% and 76.45%. Llama 3.2 3B reaches only 24.33% correct and 0.34% exact.
Applications
The method directly targets LTL verification with newly introduced propositions, propositional assignment prediction, variable-renaming robustness in programs, lambda-calculus manipulation, and formal proof generation. It requires a reliable declaration of interchangeable classes and a semantics where synchronized permutation is valid. It can be inserted into existing Transformer systems without requiring a separately learned vector for every future symbol.
Limitations & Outlook
The approach assumes a clean, known equivalence class; real-language entities often depend on context, discourse, and world knowledge. Discrete identity spaces grow exponentially, while continuous sampling cannot guarantee strict uniqueness. The evidence is limited to synthetic or formal tasks and relatively modest model settings. Future studies should test real code and proofs, multiple token classes, larger models, adaptive identity generation, and metrics that combine invariance with semantic correctness.
Plain Language Accessible to non-experts
Imagine a factory that makes products from labels. In an ordinary factory, every label gets its own permanent mold. If a new label arrives, the factory has no mold and stops. Worse, some labels may look different but describe exactly the same kind of product; the factory still treats them as unrelated because it only memorizes names.
This paper gives each interchangeable item two labels. The first is a shared category mark: it says that all these items serve the same role. The second is a temporary identity number, so the factory can still tell item A from item B in the current order. During training, the temporary numbers keep changing, forcing the factory to learn relationships rather than memorize a number.
When a new item appears, the system can create a fresh identity without rebuilding the whole catalog. In the copying task, training used no more than 20 characters and length 80, yet the proposed system handled settings near 160. In logical tasks, changing a variable's name did not destroy the learned behavior. The idea is simple: share what should mean the same, randomize only what must remain distinguishable.
ELI14 Explained like you're 14
Think of a game where three characters are called A, B, and C. The puzzle cares about what each character does, not the letters in their names. If A is renamed Z everywhere, the correct solution should stay the same. A regular AI may fail because it treats every name like a totally different game power. If it never saw Z, it may panic!
This paper gives each character two pieces of information. One shared piece says, “these are all the same kind of character.” Another random piece acts like a temporary player ID, so the AI still knows who is who. The IDs change during practice, so the AI cannot simply memorize them. It has to learn the actual rules.
The researchers tested copying strings, solving time-based logic puzzles called LTL, and predicting answers for propositional logic. In copying, the AI trained with up to 20 characters and length 80, then handled combinations close to 160. On LTLRandom35, it got 95.94% of predictions correct.
That is impressive, but not magic. Too many random IDs can become expensive, and the tests were mostly computer-generated logic problems. The next challenge is seeing whether this trick helps with real programs, mathematics, and bigger language models. Why memorize every name when you can learn the rules behind the names?
Glossary
Interchangeable Token Embedding
An embedding design for symbols that share semantics but must remain individually identifiable. It concatenates a shared learned component with a generated identity component.
This is the paper's central representation method.
Alpha-equivalence
A relation in which consistently renaming bound variables leaves meaning unchanged. The corresponding input and output symbols must be renamed together.
It defines the invariance target in formal tasks.
Alpha-covariance
A consistency metric obtained by inverse-renaming predictions from alpha-equivalent inputs and evaluating whether they agree. Higher values indicate greater transformation robustness.
The paper introduces it for model evaluation.
Tree-positional encoding
A positional representation based on locations in a syntax tree rather than only linear sequence indices. It exposes hierarchical structure to logic models.
It is used in logic-task encoders.
AdaCos
An adaptive method for scaling cosine-based logits during classification. The paper modifies it for sequence modeling and clips the scale at 100.
It trains normalized embeddings and features.
Open Questions Unanswered questions from this research
- 1 It remains unclear whether the method transfers to natural language, where two names are rarely interchangeable independently of context. Evaluation requires datasets with explicit scope, coreference, and semantic-preservation annotations.
- 2 The relationship between dβ, identity-space capacity, collision probability, and generalization has no formal bound. Better theory and scalable identity generators are needed.
Applications
Immediate Applications
LTL verification
Verification teams can represent atomic propositions as an interchangeable class and generate embeddings for newly added system variables. Combined with spot-based checking, this may reduce retraining caused solely by vocabulary expansion.
Program variables and proofs
Program-analysis or proof-generation models can be trained to preserve behavior under systematic variable renaming. Reliable scope parsing and synchronized transformation of inputs and outputs are required.
Long-term Vision
Systematic neuro-symbolic reasoning
A future reasoning stack could expand symbol inventories, generalize sequence length, and preserve permutation consistency at once. Obstacles include contextual equivalence, large-scale training, and verified semantic correctness.
Abstract
Language models lack the notion of interchangeable tokens: symbols that are semantically equivalent yet distinct, such as bound variables in formal logic. This limitation prevents generalization to larger vocabularies and hinders the model's ability to recognize alpha-equivalence, where renaming bound variables preserves meaning. We formalize this machine learning problem and introduce alpha-covariance, a metric for evaluating robustness to such transformations. To tackle this task, we propose a dual-part token embedding strategy: a shared component ensures semantic consistency, while a randomized component maintains token distinguishability. Compared to a baseline that relies on alpha-renaming for data augmentation, our approach demonstrates improved generalization to unseen tokens in linear temporal logic solving, propositional logic assignment prediction, and copying with an extendable vocabulary, while introducing a favorable inductive bias for alpha-equivalence. Our findings establish a foundation for designing language models that can learn interchangeable token representations, a crucial step toward more flexible and systematic reasoning in formal domains. Our code and project page are available at https://necrashter.github.io/interchangeable-token-embeddings