REVIEW 3 major objections 5 minor 1 cited by
A Transformer with parallel per-symbol streams achieves exact renaming invariance by construction, and this built-in property yields large gains on open-vocabulary logic tasks.
Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →
T0 review · deepseek-v4-flash
2026-08-03 06:13 UTC pith:ASQEG52N
load-bearing objection Good architecture, overstated claims—worth reviewing, but the proof and the GPT comparison need work. the 3 major comments →
Names Don't Matter: Symbol-Invariant Transformer for Open-Vocabulary Learning
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The central discovery is that exact alpha-renaming invariance can be achieved by construction, not by randomization or data augmentation. The architecture routes each interchangeable token through its own embedding stream, using a shared weight matrix and a placeholder embedding for the other symbols, then fuses streams through a commutative aggregation operation. Theorem 4.1 shows that the model's output on an alpha-renamed input is the alpha-renamed version of its output on the original input, provided every operation commutes with permutation of the streams; the proof checks per-stream and aggregated operations. This invariance transfers to unseen symbols at test time, yielding perfect al
What carries the argument
The central object is the parallel embedding stream: for each of k interchangeable tokens, the input is re-encoded with that token as an 'actual' embedding and every other interchangeable token as a shared 'placeholder' embedding. These k streams are processed by shared-parameter Transformer layers, with per-stream self-attention and an 'aggregated attention' step that averages across streams then restores each token's true hidden state at its own positions. The projection averages base-token logits across streams and takes each interchangeable token's logit from its own stream. The load-bearing identity is that alpha-renaming simply permutes the streams, and both per-stream operations (shar
Load-bearing premise
The theorem assumes that every operation in the deployed model—including the cosine-loss feature normalization, AdaCos adaptive scaling, positional encodings, and beam-search decoding—commutes exactly with permutation of the streams; the proof only verifies the core per-stream and aggregation blocks, so the exact-invariance guarantee stands or falls with those unverified components.
What would settle it
Find one alpha-equivalent pair of formulas for which the deployed model, after undoing the renaming in the outputs, produces different predictions; even a single mismatch would falsify Theorem 4.1 as applied to the system. A concrete experiment is to train with k=5 interchangeable tokens, evaluate on formulas with 10 atomic propositions, and check whether alpha-covariance remains 1.0 for the 6-10 token cases; any drop would show that the vocabulary-expansion claim is unsupported.
If this is right
- Training can be done on a small set of symbols and the model will generalize to larger symbol vocabularies without retraining.
- Alpha-covariance becomes a guaranteed property rather than a statistically encouraged one, eliminating seed-dependent behavior.
- The method removes the need for random-embedding tricks and their hyperparameter sensitivity.
- On relational reasoning tasks like propositional logic, the inductive bias yields accuracy above full-vocabulary training.
- The same architecture can be extended to other renaming-symmetric domains, such as program analysis or theorem proving.
Where Pith is reading between the lines
- A natural stress test is to permute the stream order in a model trained with the cosine-loss normalization and AdaCos scaling and check whether alpha-covariance remains exactly 1; the paper's proof does not enumerate those components, so a violation here would mean the theorem holds only for the idealized architecture.
- The same stream trick could be applied to any symmetry group that acts by permuting 'slots' of a structure, not only alpha-renaming of variables—e.g., graph nodes in a message-passing network—though the paper only claims the renaming case.
- The reported gains on propositional logic but not LTL suggest the architecture's advantage is tied to the amount of relational, name-dependent reasoning in the task; one testable prediction is that injecting the same streams into a model for a relational task with many operator pairs would produce a bigger win.
- If the perfect alpha-covariance numbers are real, they indicate that the model has essentially learned the logical structure independent of naming; if they are implementation artifacts of the specific normalization or decoding choices, a version without those choices would show lower covariance.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes a Transformer encoder-decoder architecture for symbolic reasoning over interchangeable tokens. For k interchangeable tokens, the input is expanded into k parallel embedding streams, where each stream uses an 'actual' embedding for one token and a shared placeholder for the other interchangeable tokens. The encoder and decoder apply per-stream self-attention, aggregated-view attention, and per-stream feed-forward layers with shared weights; the final projection averages base-token logits across streams and takes each interchangeable-token logit from its corresponding stream. Theorem 4.1 claims exact alpha-renaming invariance, with a proof in Appendix B based on stream permutation and commutativity of aggregation. Experiments cover copying, propositional logic assignment, and LTL witness generation, reporting perfect alpha-covariance and large OOD gains on propositional logic (95.05% vs. 84.41% for the full-vocabulary baseline), along with an extensive ablation and cost analysis.
Significance. If fully established, this is a significant and clean contribution to open-vocabulary neuro-symbolic learning. The architecture is a lightweight modification of a standard encoder-decoder, and the invariance theorem is parameter-free: it does not rely on fitted constants or circular assumptions. The empirical work is thorough, covering dataset perturbations, reduced-data regimes, ablations over six attention components, top-N accuracy, and computational scaling. The reported 100% alpha-covariance is a useful implementation-fidelity check for the tested inputs. The main reservation is that the theorem's proof does not cover all components used in the evaluated system, and the theorem's scope should be explicitly separated from the empirical vocabulary-expansion results.
major comments (3)
- [Appendix B / §3.3 / §5.2] The proof of Theorem 4.1 verifies invariance only for per-stream operations and commutative aggregation. The deployed system additionally uses cosine-loss feature normalization and AdaCos (§3.3), RoPE/tree positional encodings (§5.2), and beam-search decoding (§5.2). None of these is shown to commute with stream permutation in Appendix B. Since the theorem is stated for 'any input sequence' and for the model's output, the proof must either verify these components or define M as the raw network without decoding. In particular, beam search with token-index tie-breaking is not equivariant when scores tie; the perfect alpha-covariance numbers are evidence for the tested inputs, not a substitute for the missing proof.
- [§4.4 / §5.4] Theorem 4.1 is an invariance statement for a fixed input; it does not by itself imply that weights trained with k≤5 APs will perform well when evaluated with k=10 APs. The large OOD gain (95.05% vs. 84.41% on propositional logic) is an empirical result. Please state this separation explicitly in §4.4 or §5.4, so the theorem is not read as guaranteeing the vocabulary-expansion results.
- [Appendix B, Step 2 / Algorithms 3-4] The proof's list of per-stream operations omits the aggregated-view attention (Algorithm 3: MHA(H1,G,G,m)) and cross-attention in both modes. These operations have per-stream queries but depend on the aggregated stream G or on encoder streams; they are equivariant only if the keys/values are permuted consistently and shared parameters are used. Please state the general equivariance lemma for an operation applied identically to each stream with an invariant key/value source and check it against Algorithms 3 and 4.
minor comments (5)
- [Eq. (2)] Alpha-covariance is undefined when |P|=1 because the denominator is zero. Please state the assumption |P|≥2, which is used in the evaluations.
- [Table 3] The entries for the proposed method are garbled (e.g., 'LTL 64841024 768 52K' and 'Propositional Logic 966 6768 1024 50K'). Please repair the table formatting.
- [Figure 2 caption] The caption says 'LTL (top) and propositional logic (bottom)' while the panels are labeled (a) Propositional Logic and (b) LTL. Align the caption with the panel order.
- [Algorithm 2] The expression 'P[:, N one]' should be 'P[:, None]'.
- [§5.1.1] The phrase 'Given Vi = |Vi| interchangeable tokens' conflates a set with its cardinality. Use k or |Vi| consistently.
Circularity Check
No significant circularity: Theorem 4.1 is a self-contained equivariance proof; self-citations are not load-bearing.
full rationale
The central claimed derivation, Theorem 4.1, is a parameter-free equivariance proof from the architecture's stated operations (Algorithms 1-5): alpha-renaming permutes the parallel streams, per-stream operations with shared weights commute with stream permutation, and the aggregation/projection steps are commutative sums and index selections that are permutation-equivariant. No fitted constant enters the guarantee, and the proof does not assume the conclusion. The reported 100% alpha-covariance is therefore a corollary of the construction rather than a fitted prediction; the paper's phrase 'validating Theorem 4.1' is a sanity check of implementation fidelity, not independent evidence, but this is not circularity. The self-citations to Isik et al. (2025) provide the alpha-covariance metric, random-embedding baseline, dataset variants, and hyperparameters; these are evaluation instruments and baselines, not assumptions in the proof of invariance, so they are not load-bearing. The external validators (pyaiger, Spot) and comparisons against GPT-5.2 and other baselines show the empirical claims are not self-referential. The substantive caveat identified by the skeptic - Appendix B does not explicitly enumerate cosine-loss feature normalization, AdaCos scaling, RoPE/tree positional encodings, or beam-search tie-breaking - is an omitted-case/completeness risk, not a circularity: if any deployed component breaks exact equivariance, the theorem would be false or only approximate, but that is a proof gap rather than a derivation that reduces to its own inputs. A minor self-citation dependence for the evaluation framework prevents a score of 0, but the central derivation is self-contained.
Axiom & Free-Parameter Ledger
free parameters (4)
- Per-task attention component configuration (EP/DP/EA/DA/CP/CA) =
Prop logic: EP-DP-EA-DA-CP; LTL: EP-DP-EA-CP
- Per-task model hyperparameters (embedding dim, FF size, layers, heads, batch, steps) =
emb 96/64, FF 768/1024, 6/8 layers, 8 heads, batch 1024/768, 50K/52K steps
- Beam width / Top-N for generation and GPT comparison =
3 for main results; 10/25 for GPT parity claim
- AdaCos adaptive logit scale =
adaptive during training (value not reported)
axioms (5)
- standard math Commutativity of summation over parallel streams and equivariance of shared-parameter per-stream operations
- domain assumption Renaming atomic propositions (APs) preserves satisfiability and task semantics (alpha-equivalence)
- ad hoc to paper All deployed components beyond per-stream/aggregated ops — cosine-loss feature normalization, AdaCos scaling, RoPE/tree positional encodings, beam search — commute with stream permutation
- ad hoc to paper Identity-free representation suffices: collapsing all interchangeable tokens onto one shared 'actual' embedding preserves enough signal for relational reasoning
- domain assumption Shared weights trained with k≤5 streams transfer to k=10 streams at test (post-training vocabulary expansion)
read the original 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/
Figures
Forward citations
Cited by 1 Pith paper
-
When Symbol Names Should Not Matter: A Logistic Theory of Fresh-Symbol Classification
Regularized kernel logistic classifiers decompose into an ideal template classifier plus a perturbation from token overlaps modeled by a colored collision graph, yielding high-probability margin-transfer guarantees fo...
Reference graph
Works this paper leans on
-
[2]
” separates time steps, while “ {
18 For example,XX a specifies that proposition a must be true at the third time step. The formulaTU a demands that a becomes true at some point in the future. A more complex example isX b∧a Uc, which requires b to hold at the second step, c to eventually hold, and a to remain true at all time steps prior to whencholds. Symbolic T races.A key distinction b...
2021
-
[6]
Amir Pnueli
URLhttps://api.semanticscholar.org/CorpusID: 208310037. Amir Pnueli. The temporal logic of programs. In18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46–57,
1977
-
[7]
URLhttps://arxiv.org/abs/2103.00020. Rajeev Ranjan, Carlos D. Castillo, and Rama Chellappa. L2-constrained softmax loss for discriminative face verification,
-
[9]
Jianlin Su, Murtadha Ahmed, Yu Lu, Shengfeng Pan, Wen Bo, and Yunfeng Liu
URLhttps://arxiv.org/abs/2601.03267. Jianlin Su, Murtadha Ahmed, Yu Lu, Shengfeng Pan, Wen Bo, and Yunfeng Liu. Roformer: Enhanced transformer with rotary position embedding.Neurocomput., 568(C), February
-
[11]
URLhttps://arxiv.org/abs/2408.02265. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. InAdvances in Neural Information Processing Systems, volume 30,
-
[12]
Hengyuan Xu, Liyao Xiang, Hangyu Ye, Dixi Yao, Pengzhi Chu, and Baochun Li
URLhttps://arxiv.org/abs/2306.15880. Hengyuan Xu, Liyao Xiang, Hangyu Ye, Dixi Yao, Pengzhi Chu, and Baochun Li. Permutation equivariance of transformers and its applications,
-
[13]
Xiao Zhang, Rui Zhao, Yu Qiao, Xiaogang Wang, and Hongsheng Li
URLhttps://arxiv.org/abs/2304.07735. Xiao Zhang, Rui Zhao, Yu Qiao, Xiaogang Wang, and Hongsheng Li. Adacos: Adaptively scaling cosine logits for effectively learning deep face representations.2019 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), pages 10815–10824,
Pith/arXiv arXiv 2019
-
[14]
Here,Tdenotes the constantTrue, and the operators include negation ( ¬), conjunction ( ∧), disjunction ( ∨), equivalence (↔), and exclusive or (⊕). ϕ:=T|p| ¬ϕ|ϕ 1 ∧ϕ 2 |ϕ 1 ∨ϕ 2 |ϕ 1 ↔ϕ 2 |ϕ 1 ⊕ϕ 2 (7) The satisfiability problem in propositional logic asks whether there exists a Boolean assignment to the atomic propositions in P that makes a given formula...
1977
-
[2017]
Novel positional encodings to enable tree-based transformers
Vighnesh Leonardo Shiv and Chris Quirk. Novel positional encodings to enable tree-based transformers. In NeurIPS 2019, December
2019
-
[2019]
Bingbin Liu, Jordan T Ash, Surbhi Goel, Akshay Krishnamurthy, and Cyril Zhang
URL https://arxiv.org/ abs/1810.00825. Bingbin Liu, Jordan T Ash, Surbhi Goel, Akshay Krishnamurthy, and Cyril Zhang. Transformers learn shortcuts to automata
-
[2020]
doi: 10.18653/v1/2020.emnlp-main.731
Association for Computational Linguistics. doi: 10.18653/v1/2020.emnlp-main.731. URL https://aclanthology.org/2020.emnlp-main.731/. 11 Ryoma Kumon, Daiki Matsuoka, and Hitomi Yanaka. Evaluating structural generalization in neural machine translation.ArXiv, abs/2406.13363,
Pith/arXiv arXiv 2020
-
[2021]
Jesse Michael Han, Jason M. Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models.ArXiv, abs/2102.06203,
-
[2022]
Kreber, Markus Norman Rabe, and Bernd Finkbeiner
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus Norman Rabe, and Bernd Finkbeiner. Teaching temporal logics to neural networks. In9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021,
2021
-
[2024]
doi: 10.1016/j.neucom.2023.127063
ISSN 0925-2312. doi: 10.1016/j.neucom.2023.127063. URLhttps://doi.org/10.1016/j.neucom.2023.127063. Andong Tan, Fengtao Zhou, and Hao Chen. Explain via any concept: Concept bottleneck model with open vocabulary concepts,
arXiv 2023
-
[2025]
Najoung Kim and Tal Linzen
URLhttps://openreview.net/forum?id=2MPI9KSBV5. Najoung Kim and Tal Linzen. COGS: A compositional generalization challenge based on semantic inter- pretation. In Bonnie Webber, Trevor Cohn, Yulan He, and Yang Liu, editors,Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 9087–9105, Online, November
2020
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.