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

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/

Language models that reason about logic (for example, checking whether a software system is correct or solving logical puzzles) often depend on the specific names used for variables. If such a model is trained on formulas that use the letters a and b, it may fail on an identical formula that uses x and y instead, even though swapping names changes nothing about the underlying logic. This issue limits how well these models generalize to new, larger problems. We built a new type of language model, called a Symbol-Invariant Transformer, that treats interchangeable names as truly interchangeable. The model creates parallel "views" of the input, one for each variable name, and combines them using an operation that is blind to which name is which. This gives a mathematical guarantee: renaming variables can never change the model's answer, by design. As a result, our model solves logic problems involving more variable names than it has ever seen in training, without any retraining. We also show that an existing language model can be converted to use our approach with a small amount of additional training. This is a step toward AI systems that can reliably assist with software verification and formal reasoning at scales beyond their training data.