Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

İlker Işık, Wenchao Li

TL;DR

This work addresses open-vocabulary symbolic reasoning where interchangeable tokens, such as bound variables, can be renamed without changing meaning. It introduces a Symbol-Invariant Transformer that runs $k$ parallel embedding streams—one per interchangeable token—processed by shared Transformer layers and combined via an aggregated attention mechanism, yielding exact invariance to alpha-renaming. The authors prove alpha-equivalence by construction and demonstrate strong generalization on propositional logic and LTL tasks, outperforming baselines including GPT-5.2 in LTL witness generation and achieving competitive results in relational reasoning while maintaining efficiency. The approach enables post-training vocabulary extension with formal guarantees, offering practical impact for domains like formal verification, program analysis, and theorem proving where symbol renaming is commonplace.

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.

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

TL;DR

This work addresses open-vocabulary symbolic reasoning where interchangeable tokens, such as bound variables, can be renamed without changing meaning. It introduces a Symbol-Invariant Transformer that runs parallel embedding streams—one per interchangeable token—processed by shared Transformer layers and combined via an aggregated attention mechanism, yielding exact invariance to alpha-renaming. The authors prove alpha-equivalence by construction and demonstrate strong generalization on propositional logic and LTL tasks, outperforming baselines including GPT-5.2 in LTL witness generation and achieving competitive results in relational reasoning while maintaining efficiency. The approach enables post-training vocabulary extension with formal guarantees, offering practical impact for domains like formal verification, program analysis, and theorem proving where symbol renaming is commonplace.

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.
Paper Structure (42 sections, 1 theorem, 7 equations, 17 figures, 6 tables, 5 algorithms)

This paper contains 42 sections, 1 theorem, 7 equations, 17 figures, 6 tables, 5 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Alpha-Equivalence
  5. Problem Definition
  6. Language Models and Transformers
  7. Proposed Method
  8. Creation of Streams and Per-Stream Operations
  9. Aggregation and Projection
  10. Overall Architecture
  11. Theoretical Guarantees
  12. Experiments
  13. Tasks and Evaluation Metrics
  14. Alpha-Covariance
  15. Experimental Setup and Baselines
  16. ...and 27 more sections

Key Result

Theorem 4.1

Let $M$ denote the proposed model and $f \colon {\mathbb{V}} \to {\mathbb{V}}$ be an alpha-renaming function that fixes ${\mathbb{V}}_n$ and permutes ${\mathbb{V}}_i$. For any input sequence ${\bm{x}}$, let $\hat{{\bm{y}}} = M({\bm{x}})$ denote the model's output. Then for the alpha-renamed input ${ Equivalently, $\hat{{\bm{y}}}' = f(\hat{{\bm{y}}})$, i.e., the model's prediction on alpha-renamed

Figures (17)

  • Figure 1: Method overview. The numbered sections correspond to: (1) Creation of parallel embedding streams with actual and placeholder embeddings for interchangeable tokens, (2) per-stream self-attention over individual streams, (3) aggregated attention between each stream and the fused view, (4A/4B) cross-attention between decoder streams and encoder streams with per-stream or aggregated modes, (5) applying feed-forward networks per stream, and (6) projection that averages base token logits and preserves interchangeable token logits. The bottom right section illustrates the aggregation process that fuses parallel streams into a single view while restoring true embeddings at interchangeable token positions. All parameters are shared across streams, which enables post-training vocabulary extension. Common transformer components (e.g., layer normalization, residual connections) are omitted for clarity.
  • Figure 2: Heatmaps showing prediction accuracy on test sets with varying formula complexity for LTL (top) and propositional logic (bottom) tasks. Brightness indicates sample density, with full brightness representing 100 samples. The dashed white box marks the training data distribution boundary.
  • Figure 3: LTL training set distribution before and after augmentation in log scale.
  • Figure 4: Heatmap evaluation of the alpha-renaming baseline before and after augmenting the training set to address imbalance.
  • Figure 5: Ablation heatmaps for propositional logic assignment prediction.
  • ...and 12 more figures

Theorems & Definitions (2)

  • Theorem 4.1: Alpha-Renaming Invariance
  • proof