Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
Authors: İlker Işık
Ramazan Gokberk Cinbis
Ebru Aydin Gol
Venue: ICML 2025 poster (2025)
Keywords: embedding methods
interchangeable tokens
extendable vocabulary
transformer models
linear temporal logic
propositional logic
formal reasoning
token generalization
alpha-equivalence
inductive bias
language models
symbolic representation
neural networks
Primary area: general_machine_learning->scalable_algorithms
TL;DR: Our novel approach for learning interchangeable tokens generalizes to larger vocabulary sizes as demonstrated on a copying task and two logic tasks.

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

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
ilker Işik
Ramazan Gokberk Cinbis
Ebru Aydin Gol
Abstract
perform well in neurosymbolic reasoning tasks, such as theorem proving (Han et al., 2021) and mathematical rea- soning (Rabe et al., 2020). The formal reasoning capabilities of these models were once doubted, but Liu et al. (2023) demonstrated the ability of Transformer models ( (Vaswani et al., 2017) to learn shortcuts to automata. Of particular in- terest the generalization ability of such models to unseen, out-of-distribution data (Sanh et al., 2022), enhancing their appeal for logical reasoning (Abbe al., 2023).
Language models lack the notion of interchange- able tokens: symbols that are semantically equiva- lent yet distinct, such bound variables in formal logic. This limitation prevents generalization larger vocabularies and hinders the model's 's ability to recognize bound variables preserves meaning. We formal- ize this machine learning problem and introduce alpha-covariance, metric for evaluating robust- ness such transformations. To tackle this task. propose dual-part token embedding strategy: shared component ensures semantic consistency, while randomized component maintains token distinguishability. Compared to baseline that re- lies on alpha-renaming for data augmentation, our approach demonstrates improved generalization to unseen tokens in linear temporal logic solv- ing, propositional logic assignment prediction, and copying with an extendable vocabulary, while introducing favorable inductive bias for alpha- equivalence. Our findings establish a foundation for designing language models that can learn inter- changeable token representations, a crucial step toward more flexible and systematic reasoning formal domains. Our code and project page are available wwwrrashee.gihuub.bo//eeerrotete token-embeddinns
where renaming
Another application area is linear-time temporal logic (LTL), which is heavily utilized by the formal verification commu- nity (Clarke et al., 2018; Baier & Katoen, 2008) for reason- ing about how logical propositions change over time (Pnueli, 1977). Through the use of temporal operators, LTL formu- lae can specify, for example, that proposition p must hold at all time steps (Gp), or at least one time step (Fp). LTL formulae operate on traces, which describe how the proposi- tions change over time.
Solving a given LTL formula involves finding a satisfying trace, and it proved essential for generating examples for system specifications in the literature. This field was domi- nated by the methods that use classical algorithms, such as spot (Duret-Lutz et al., 2022) and aalta (Li et al., 2014), However, following the success of Transformer models on end-to-end symbolic integration (Lample & Charton, 2019), Hahn et al. (2021) attacked the LTL solving problem using the same approach. Their capability to generalize to longer formulae is especially noteworthy, and it was made possible thanks tree-positional encoding (Shiv & Quirk, 2019).
However, generalization to longer formula lengths is not the only concern. In particular, each LTL formula features set of atomic propositions (henceforth APs), and it's de- sirable for the model to generalize to more APs. But the architecture of the model does not even accept new APs that are not seen during training, despite the fact that all APs represent semantically equivalent concepts while being dis- tinguishable from each other. This situation arises in many other application areas, such mathematical expressions and lambda calculus (alp, 1984), where renaming the bound variables does not change the meaning. This phenomenon is described as alpha-equivalence alpha-renaming refers to the process of creating alpha-
1. Introduction
Following the deep learning revolution that affected nu- merous application areas (Dargan et al., 2020), recent lit- crature shows that deep learning based approaches also
'Department of Computer Engineering, Middle East Technical University, Ankara, Turkey *Microsoft, Istanbul, Turkey. Cor- respondence ilker Işık <ilker@ seng.metu.edu.try Ramazan Gokberk Cinbis <geinbis@ ceng. www.. Ebru Aydin Gol <ebruaydingol microsoft.com>>.
Proceedings of the 42nd International Conference Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).
Alpha-conversiee (or

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
equivalent input-output pairs.
in modern deep learning, was initially proposed as a genera- tive model to translate between natural languages autoregres- sively. This led to many successful attempts to frame formal reasoning tasks as language modeling problems, such as symbolic integration (Lample & Charton, 2019), symbolic regression (Kamienny et al., 2022; Vastl et al., 2022), LTL solving (Hahn et al., 2021), 1), and many more. Further de- velopments shifted the field towards large language models (LLMs), e.g., by prompting model pre-trained on gigan- tic scale (Frieder et al., 2023), by enhancing the prompt with retrieved references for proof generation (Welleck et al., 2022; Yang et al., 2023), by training an LLM on a spe- cialized dataset for mathematics (Azerbayev et al., 2023). However, the reasoning abilities of LLMs were questioned by (Tang et al., 2023), who showed LLMs struggle with symbolic reasoning when semanties are decoupled, and by others (Wu et al., 2023).
In this paper, we propose a novel approach for represent- ing interchangeable tokens in neural network models. To summarize, our method constructs some part of the token embeddings on-the-fly instead of learning all of them during training. The token embeddings for interchangeable tokens consist of two parts: a learnable part and randomized part. The learnable part is shared across all interchangeable to- kens, and the model must depend on the randomized part to differentiate these tokens. Thanks to the randomized com- ponent, our method can generate embeddings for arbitrarily many interchangeable tokens as needed during both training and inference, with the only practical limitation being the ex- ponentially growing sampling set size for discrete random generation methods. We use the weight tying technique (Press& & Wolf, 2016) to share the same token embeddings with the final projection matrix, which calculates the logits (i.e., next-token probabilities before softmax).
Extensible vocabulary. Efforts to create an extensible vocabulary for neural networks are scarce in the broader machine learning community, let alone the formal reason- ing literature. Morazzoni et al. (2023) exploited dictio- nary definitions to create extensible word embeddings. Wei et al. (2016) proposed a vocabulary-extensin guage recognition framework by using component based approach, where each sign gesture is recognized based on common components such as hand shape, orientation, axis, rotation, and trajectory. These studies depend on either external information (dictionary definitions) or properties specific to an application area (components of hand gesture); they do not attempt to design an extensible vocabulary for interchangeable tokens, which has been neglected by the literature alongside the concept of alpha-equivalence.
We use our embedding method in a Transformer encoder- decoder model and evaluate it on three tasks: copying with an extendable vocabulary, solving LTL, formulae, and pre- dicting assignments for propositional logic. As baseline, consider simpler approach that uses alpha-renaming for data augmentation during training to expose the model to a larger vocabulary, which is also new in the literature to the best of our knowledge. Overall, our method demon- strates generalization capabilities to larger vocabulary sizes, and also combines well with positional encodings that ex- hibit length generalization. We also experiment with dataset perturbation show that our method introduces helpful inductive bias for alpha-equivalence. Finally, we present alpha-covariane a metric for measuring robustness against alpha-conversions that is applicable to any domain where alpha-equivalence is relevant.
sign lan-
3. Problem Definition
Overall, our contributions can be summarized as follows.
In language modeling, the goal is to predict the next token in the output sequence given the input and the past output. (See Appendix A for more background.) Let V denote the set of all unique tokens, i.e., the vocabulary of a language modeling problem. We use V to denote the set of all fi- nite sequences of tokens (strings) from V. We assume that V, is the set of interchangeable tokens and V,, = V. is the set of non-interchangeable tokens. The core idea be- hind dipha-equivalence is that renaming interchangeable tokens between each other in both input and output pre- serves meaning. Let f: V + V be bijection such that fz) = x for all x E Wn, i.e., f arbitrarily renames the interchangeable tokens between each other in one-to-one correspondence and preserves the rest of the tokens. We apply f to each token in a given pair of input a E V and output b E V strings, obtaining a' = (f f(a))....) and b' (b2),....) We call this operation alpha- conversion or alpha-renaming The set of interchangeable
1. Identify the problem of generalizing to larger vocabular- ies in (formal) language modeling tasks, and define an experimental protocol to study this problem.
2. Propose alpha-covariance, novel metric for measuring robustness against copper-onverssons, applicable to any domain with interchangeable tokens.
3. Introduce dual-part embedding method for vocabulary generalization and improved civaraccv with neg- ligible computational overhead.
4. Verify the proposed method thoroughly on three tasks: copying with extendable vocabulary, solving LTL formu- lae, and predicting assignments for propositional logic.
2. Related Work
Language modeling and formal reasoning. The trans- former architecture (Vaswani et al., 2017), now ubiquitous
2

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalenee
tokens V. must be defined such that a' and b' form a valid input-output pair semantically equivalent to (a, b) for all possible f.
tokens, L E Raxd, represents the matrix of learnable em- heddings for non-interchangeable tokens, E 1Ixxd the shared learnable embedding for interchangeable tokens, and B E I 1xdg the sundomly-genrran
embedding for the ith interchangeable token where 1 < i S m. Note that a and B3 are row vectors. A zero matrix of size i x j is represented by 0 In addition, we define two row-based L2 normalization functions for( and (X)) that divide each row X1: by its L.2 norm || These two functions are identical but can be disabled independently from each other, hence the separation. Finally, the overall structure of the embedding matrix U is shown in Equation 1. In this construction, the interchangeable tokens are assumed to come after the non-interchangeable tokens. Note that it's also possible to implement multiple sets of different interchangeable tokens via a trivial extension.
Our task is to design an embedding method that alongsiee being resilient to alpha-renaming by construction-can sup- port a new vocabulary V = Vi U V where V, C Vi after training on V. In other words, the model should be able to operate on a larger vocabulary than the one seen during training, as long as the newly introduced tokens belong to the class of interchangeable tokens. Although we don't 't im- pose any restrictions about the size of V in this problem definition, the maximum size of V in practice may change as function of the number of embedding dimensions. Thus, while setting the hyperparameters, the expected size of V must be considered.
Example. In the LTL solving problem (Appendix B), the set of non-interchangeable tokens Vn includes the operators, constants, delimiter tokens (";", "{", "["""""" "I"), and any special tokens such as the end token. The set of interchangeable to- kens equals to the set of atomic propositions (APs): V, = P. Assuming P- = {a, b), the formula-trace pair ("&axb", "a,b; b; {1) } "") is alpha-equivalent ("&bXa", "b; a; (1)"). Further, assume that the augmented set of interchangeable tokens is V = P' = {a, c, d). Now, the aforemen- tioned pair can also be equivalently represented as cxd", "c; d; (1)". The augmented vocabulary allows the expres- sion of formula- trace pairs that feature up to 4 APs instead of 2. For example, ("& a abx& cd", "a "&ab; &ed; (1) (1)") can- not be expressed using p {a, b.. Our goal is to create model that can handle such inputs despite being trained the limited vocabulary V - V, U.P
fbn [bn( fan((a
On (31)
U= fff
(
(1)
(cx
Stn [mm((m)
During training, the embedding matrix must be recon- structed in each forward pass with resampled random vec- tors B1 to Bm. Resampling 3, for S S m during training prevents the model from adapting to the idiosyn- cracies of particular random generation and forces it to distinguish between interchangeable tokens regardless of the contents of B.. During inference, it's created once at the start and remains the same since the autoregressive genera- tion involves multiple forward passes on the same input.
4. Proposed Method
Normalization. There are several concerns that warrant the heavy use of normalization while constructing U, as seen in Equation 1. Firstly, da dimensions and dg dimensions should not overwhelm each other in terms of magnitude. Normalizing a and G3 separately addresses this issue. The magnitude of the concatenated embedding is another con- cern, which is handled by the final normalization. The redundant (since the final normaliza-
To address the problem of learning semantically equivalent but distinguishable (quivaleuuialentt tokens, our method employs two ideas: sharing some part of the embeddings between such tokens to convey their semantic equivalence; and assigning a unique mandomly-generater vector to the rest of the embedding for each interchangeable token, allowing the model to distinguish between them. The number of shared and mondoml--generted dimensions are denoted by da and de respectively. The sum of these two yields the total number of embedding dimensions in the model, denoted by dmoodl dæ + dg. For non- non-interchangeable tokens, da dimensions contain separate learnable parameters and dg dimensions are set to 0. The structure of the embedding matrix is visualized in Figure 1.
normalization of tion does the same operation after the concatenation with zeros) but kept in Equation for readability.
4.2. Random embedding generation
This section will explain how the distinguishing part of the interchangeable token embeddings, Br, < S m, are created. To this end, we developed 3 methods to generate random vectors. Table provides a summary at a glance. The first method simply samples the standard normal distri- bution for each dimension. The second one uses the neigh- boring grid points around the origin, which correspond to the 8 directions in 2D. For each interchangeable token, a
4.1. Embedding matrix
Construction of the embedding matrix. For a vocabulary with n non-interchangeable tokens and m interchangeable
3

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
Regular Tokens
Leamable
Zeros
Table 1. Comparison of random vector generation methods.
Method
Normal Distribution
Neighboring Points
Hypercube Vertices
a; ~ (0,1)
a, E [-100,1] |a # 0
a E 1,11
Inter- Leurnable (Shared Rows)
Formula
chmngeahle
Randomly Genernred
Tokens
Size for n-dims
Continuous
2
Emabediing Dimeusioos
Sample Visualization
Figure 1. Visual structure of the embed- ding matrix in the proposed method.
unique vector in this set is sampled. The last method is similar, but its set consists of the vertices of a hypercube centered around the origin, i.e., diagonal direction vectors.
are tied in addition to the final projection matrix. Three- way weight tying is particularly appropriate for the LTTL solving task since many tokens are shared between the LTL formulae and traces.
Uniqueness constraint. In the normal distribution method, we don't have any additional constraints to ensure distin- guishability between vectors. However, in other two meth- ods, we need to make sure that each interchangeable token gets assigned to a unique vector since the sampling set is fi- nite. To achieve this quickly and space-efficiently. we define mapping from integers possible vectors. The unique vectors are generated by sampling unique random inte- gers (which can be calculated efficiently using the reservoir sampling technique), and then using the defined mapping to convert these integers to the vectors. This strategy avoids materializing the whole set possible vectors. In the hyper- cube vertices method, we map the binary digits of an integer in [0, 2da) to 1) Although "Neighboring Points" is simply the ternary version of the same idea, avoiding the zero vector requires special care. The zero vector maps to the integer ig = (3da - 1)/2. Therefore, we define our do- main as the integers in [0. ad - 1) and add 1 to the integer i before converting it i 2 ig. Integer mapping approach for generating unique vectors works well for up to 32 di- mensions, after which the limits of integer representation become an issue for reservoir sampling. Therefore, in such cases, we simply disable the uniqueness check because the exponentially growing size of the sampling set renders the probability of drawing the same sample negligible.
Feature normalization. Given the output of the last layer before the final projection v (henceforth called feature vec- tor), instead of directly applying the final projection as in Uv, we apply L2 normalization to the feature vector v be- fore passing it through the final projection: (f) This matrix multiplication constitutes taking dot product with each row. Since b = |a]] [[][]|[[[o [|][]cs(()) where 0 is the angle between a and b, normalizing both the embeddings and the feature vector leaves only the cosine term to determine the logits. This forces the model to distinguish between tokens based solely on the directions, which may improve the gradient flow.
Cosine loss. If we normalize both the embeddings and the feature vector, the only thing that determines each logit is the cosine of the angle between the feature vector and the embedding. Applying the softmax loss to such logits is known as cosine loss in the literature. Although cosine- based loss functions were successful face recognition (Ranjan et al., 2017; Wang et al., 2017), it proved sensitive to hyperparameter settings in these losses. To avoid this problem, we use AdaCos loss function (Zhang al., 2019) that scales the logits adaptively throughout training.
Despite the attractiveness of AdaCos in this context, it is not directly applicable in a language modeling setting due to the additional sequence length dimension, and no prior work explored this application the best of our knowledge. To overcome this, we modify the AdaCos loss function as follows: First, combine the batch and length dimen- sions while ignoring the padding tokens, effectively treating both dimensions as batch dimensions. However, since this change greatly increases the number of batch dimensions, it can lead to numerical issues, even with the log-sum-exp trick. Therefore, we clip the scale value calculated by Ada- Cos to a maximum of 100 to avoid numerical issues. This loss formulation can also be used with conventional embed- dings, as we do in our experiments.
4.3. Projection
Weight tying. In a traditional language modeling setting, since both the embedding and projection matrices are en- tirely composed of learnable parameters, it's not necessary to share them, even though there are many advantages of weight tying (Press& & Wolf, 2016). However, we construct the embedding matrix manually in our method, which makes weight tying a requirement. Furthermore, since per- form our experiments on an encoder-decoder architecture in this paper, we utilize a three-way weight tying approach, whereby the embedding matrices encoder and decoder
4

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalenee
Baseline (Fieed Embeddling)
Proposed Method
3
160
Training sets have the same distribution: sequences length 80, with 20 unique character tokens.
Test samples in this region contain 20 unique characters training), but much longer sequences.
20
Unique Characters
40
120
100
80
160
60
Test samples in this region are limiteed to length s 80 training), but from larger vocabulary. Fixed-embeddingg cannot extrapolate.
120
40
The proposed method adapts nearly-flawless sequences of length vocabulary size up to 160.
140
20
D
160
3
20
40
80 Length
100
140
260
20
60
120
140
160
C
Length
Figure Two annotated heatmaps visualizing the test-set edit distance between prediction and ground truth in copying task with extendable vocabulary. Both heatmaps share the same y-axis. The green box represents the number of unique characters (y-axis) and the maximum length (x-axis) in the training dataset. Each point shows the average test error, except the lower triangular part of each heatmap (gray hatch pattern) corresponding to the impossible combinations of length and unique character counts. The traditional approach (left), using ubiquitously utilized fixed (learned) token embeddings, cannot extrapolate to vocabulary expansions. The proposed method (right) enables generalization to larger vocabulary sizes longer sequence lengths, compared to what is observed during training.
5. Experiments
generalize to larger vocabulary sizes unseen during training.
Experimental setup. We use a transformer encoder- decoder architecture in all experiments. We always use the same embedding size in both encoder and decoder due to weight tying. We use the RoPE (Su et al., 2024) as the positional encoding method in the decoder. In the encoder, we use rre-ppoitional encoding if applicable (logic tasks), RoPE otherwise (copying task). The hyperparameter set- tings are given in Table 4 in Appendix D.
Using edit distance as our evaluation metric, we first as- sess the vocabulary generalization capabilities (Appendix E) Since our method excels in this task, we then explore generalization in both vocabulary size and string length (Ap- pendix E.2), performing a hyperparameter search over the settings of our embedding method (Appendix E.3). Finally, we scale up the vocabulary size and the string lengths to evaluate method (Appendix E.5). Our method exhibits perfect performance in the out-of-distribution domain as shown in Figure 2. We also examine our method's s sensi- tivity to randomness in embeddings (Appendix E.4), and propose using the random embedding with median cross entropy loss as proxy for average performance.
Baselines. We train three types of baseline models with traditional embeddings: the first one on the original dataset, the second one dataset with the ing a larger vocabulary size, and the third one on the original dataset but using data augmentation strategy. Specifically, for the third baseline, the number of interchangeable token embeddings matches that of the test set, and we apply ran- dom alpha-renaming at each forward pass during training. This ensures that the model is exposed to all tokens in the test set, but the number of unique interchangeable tokens the model sees in each sample remains limited in the training set. Note that this is an internal baseline that doesn't 't exist in the literature to the best of our knowledge.
parameters but us-
5.2. LTL Solving
In this section, we train models on the LTLRandom35 dataset from DeepLTL (Hahn et al., 2021) and other syn- thetic datasets created with the same method. To evaluate the correctness of the generated formulae, utilize spot framework version 2. 11.. (Duret-Lutz et al., 2022). We use prcepposiional encoding (Shiv & Quirk, 2019) in the encoder and RoPE (Su et al., 2024) in the decoder. We generate predictions using beam search with beam size = 3.
5.1. Copying with Extendable Vocabulary
We introduce new toy problem designed to evaluate the vocabulary generalization capabilities of our embedding method. We create various training datasets that contain 10 million random strings with a limited vocabulary size. A string is given as input, and the model is expected to produce the input string exactly via autoregressive generation. This embodies helpful toy problem for our method because all tokens are interchangeable, barring the special tokens (start/end). In these experiments, we expect the model to
Baselines. We trained all of the baseline models from scratch. For the first type of baseline, we aimed to repro- duce the results from Hahn et al. (2021). Hence, used the best hyperparameters they reported (Appendix D). Un- like Hahn et al. (2021), we experimented with RoPE (in the decoder) and AdaCos, but did not observe a noteworthy improvement on the validation set. After determining the best baseline model on the validation set, we evaluated on the test split of ITLnandom35 and obtained a correct rate
5

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalenee
Table 2. Evaluation of the baselines, our method, and Illama 3.2 the LandRam dataset. The alpha-renaming baseline was trained using AP embeddings since vocabulary generalization is not evaluated here. First two columns denote the training dataset and the model. Next two columns indicate the ratio of the correct predictions and exact matches on 99,989 test set samples as evaluated by spot. Last three columns display mean alpha-covariance values for varying atomic proposition (AP) counts, evaluated on all alpha-equivalent variants 1000 test samples. The results indicate that our method induces a robust inductive bias for alpha-equivalence.
Training
Evaluation
Dataset
Model
Correct
Exact
3 AP
AP
AP
Normal
Baseline
98.23%
83.23%
96.87%
95.86%
91.80%
Perturbed
Baseline
34. 13%
12.12%
64.93%
57.99%
40.91 %
Perturbed
Rehaa-enn
97.96%
77.66% %
99.55% %
99.49%
98.86% %
Perturbed
Proposed
95.94%
76.45%
97.66%
97.76%
98.29%
Pretrained
Llama 3.2 3B
24.33%
0.34%
68.17%
63.27%
62.34%
of 98.2% against the 98.5% reported by Hahn et al. (2021).
alpha-cquivalent to (x,, y). We define a the alpha- conversion function for the ith input pair such that (x(z) = x² and (3) = y². To compute the alpha- covariance of a model with respect to IP, we generate pre- dictions for each input in IP, obtaining the prediction g' for each x². We define a set that contains the predictions with alpha-conversion undone:
5.2.1. DATASET PERTURBATIONS
To demonstrate that our method creates a helpful inductive bias, we created a perturbed version of the LTLRRndom35 dataset by renaming the APs such that the order of the first AP appearances in the trace is always the same. As the empirical evidence in Table 2 confirms, both our method and naturally immune to these
{a; (Ø') | S i S n). Note that if we defined this set for the ground truth outputs in P. we would get {y) } since - (yy') by definition. The model's sensitivity to alpha-conversions could be quantified by simply [U], but this value may be hard to interpret since it depends on [P]. To normalize this value intuitively, we define the alpha-covariance of a model with respect in Equation 2.
holds for each y'
the alpha-renaming baseline alterations. We train these methods only on the perturbed dataset since training them again on the normal dataset amounts to training with different random samples.
While the original model performs significantly worse un- der perturbation, both alpha-renaming and proposed models match the baseline performance in correctness ratio despite perturbation. This observation suggests that these modifica- tions introduce robust inductive bias that makes the models resistant to perturbations in the data. A minor decrease in the ratio of exact matches is noted, but this may signify less overfitting and a better bias-variance tradeoff in the larger context. Appendix F continues this experiment with limited amount of training samples instead of perturbations.
Intuitively, when alpha-covariance is 1, the model is unaf- fected by all alpha-conversions in P. An alpha-covariance of O indicates that [TU] = [P], i.e., the model's prediction for each alpha-equivalent pair is unique after undoing the alpha- conversion. This is unwanted because alpha-cone conversons should not change the semantic meaning. Thanks to the em- bedding randomization in our method, an alpha-conversion does not necessarily change the embeddings, and conversely, there are multiple ways to embed the same input.
5.2.2. ALPHA-COVARIANCE
Given a vocabulary of n AP tokens and an LTL formula- trace pair containing A APs, it's possible to write "Pa nn/(n - 13)! alpha-cquivalent pairs. Since these are semanti- cally equivalent, we expect the model's predictions be the same after undoing the alpha-conversions for all of them. As there is no metric quantify this in the literature to the best of our knowledge, we develop new metric.
For the proposed method, we generate the random embed- dings once at the start of an evaluation run using the heuristic explained in Appendix E.4. Thus, alpha-conversion in this context are equivalent to shuffling the random embeddings in our method, which amounts to measuring our model's robustness against differences in random embeddings.
Let (x. 4) be an oututt pair for the model, and let = ((x ( y)),.... (x", r) be n input-output pairs
We report the results in Table 2, which demonstrates that our method has positive impact on the alpha-covariancee especially in limited data settings. Since the LTL.Rand dataset was created synthetically, it doesn't 't have any note- worthy biases and even the baseline enjoys a high alpha-
'Using RoPE in the decoder increased the ratio of correct predictions from 97.8% to 98.0% on the validation set. Introducing AdaCos addition to RoPE increased this value to 98.2%.
6

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalenee
Proposed Method (90.76%)
Baseline (41.97%)
Full Vocabulary (92.82%)
Alpha-Renaming (82.71%)
AV count
0.75
0.50
0.25
0.00
20
20 Formula length
20
Formula length
Forulaa length
Formula length
(a) LTL Solving
P Proposed Method (77.70%)
Baseline (37.11%)
Full Vocabulary (84.41%)
Alpha-Renamann (68.96%)
1.00
AV count
0.75
0.50
10-
0.00
10
20
30
10
20
30
10
20
30
10
20
30
Formula length
Formula length
Fomula length
Formula length
(b) Propositional Logic
Figure 3. Heatmaps visualizing the ratio of correct predictions on special test set, for LTL solving (top) and propositional logic (bottom) tasks. brightness of color depends on sample size, with full brightness representing 100 samples. dashed white represents the boundaries of the training dataset. Our model is competitive with the full vocabulary baseline despite being only trained on formulae with at most APs, and outperforms other baselines.
wbb Adacos (81.45%)
w/o fr & AdaCos (81.65%)
w/o fan (29.53%)
1.00
12000
AP count
0.75
0.50
6000
0.25
0.00
10
20
40
50
10
20
50
10
20
30
50
Formule length
ormula length
Formula lenoth
50
Formuls Length
(a) LTL Solving
32000
Formula length 35
Formula length
w/o Adacos (77.52%)
fr S AdaCos (77.91%)
w/o fm (14.129%
1.00
10000
AP court
0.75
0.50
8000
0.25
0.00
10
20
40
50
20
50
10
20
30
50
length
length
(b) Propositional Logic
Figure 4. Scaling behavior of the trace generation using spot.
Figure 5. Heatmaps for the ablation studies. The results reported the in Figure
LTL Solving (21.70%)
Propos iional Logic (30.92%)
0.0100
Optimized
1.00
Nalve
0.0075
COuPt
0.0050
0.50
0.0025
0.25
10
0.00
0.0000
10
20
30 length
40
50
20
40
longth
Unique Vectors
Figure Average runtime cost of generating dimensional unique random vectors from Neighboring Points with different uniqueness checking methods.
Figure 6. Ilama 3.2 heatmaps for the two logic tasks.

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
covariance thanks this. However, when the dataset is perturbed by introducing bias to the order of APs, the baseline struggles heavily with alpha-covariance, whereas our method does not.
excels in out-of-distribttion settings, but trades off some in-distribution performance. Although the full vocabulary baseline performs very similarly to our method, it's impor- tant to note that this region is in-distribution for that model. Overall, these results align with Figure 3(a).
5.2.3. GENERALIZATION
5.3. Assignment Prediction for Propositional Logic
The test dataset for this experiment contains at most 100 formula-trace pairs for each combination of AP count and formula length, whose maximum is 50 instead of 35. We report the results for our model (using Hypercube Vertices, d3 5) and the three baselines in Figure 3(a). The first baseline uses the same training dataset, whereas the second baseline uses a new LTL dataset with 10 APS, which we create using the same method as LTLRandom35, For the third baseline, we train fixed embedding model with 10 APs using the same 5 AP dataset but we shuffle the AP emheddings in each forward pass during training.
To further demonstrate the applicability and generalization capabilities of our method, we evaluate it on a considerably different logical problem: predicting assignments for propo- sitional logic (Appendix C). The experimental setup is based on DeepLTL (Hahn et al., 2021) with minor differences in hyperparameter choices (Appendix D). We use pya i ger (Vazquez-Chanlati & Rabe) to generate datasets and eval- uate predictions. In Appendix G.1, we provide additional details about our experimental setup.
We perform the generalization experiment as in Section 5.2.3 and report the results in Figure 3(b). We observe the same ranking with slightly larger performance gaps. Once more, the proposed method is superior to all approaches that use the same 5 AP training dataset, beaten only by the full vocabulary model which sidesteps the challenge of AP generalization due to its enhanced training dataset.
Discussion. Despite seeing only 5 APs during training, our method performs only slightly worse than the full vocabu- lary baseline, which represents what a waanformer-basee model can do with 10 APs. Our method outperforms both the vanilla and the alpha-renaming baselines by a consid- erable margin, which is significant since the latter is the only other model that can generalize to more APs. Based this, we hypothesize that the proposed stochastic AP embed- dings provide a more explicit enforcement towards learning aabedding-covariin transformations in the model, as op- posed to training with appha-renaming, where the learned embeddings may still carry unwanted token-specific biases. Furthermore, unlike the baseline models, our model does not have to learn the concept of AP from scratch for each AP token thanks to the shared embedding part. This could explain why our method shone against the alpha-renaming baseline in the LTL task where the interchangeable tokens are more complex than the copying task.
We continue propositional logic experiments in Table 3 and Appendix G.2 which focus on alpha-covariance and dataset perturbations respectively. The results of these experiments also align with the LTL experiments.
5.4. Ablation Studies
The hyperparameter search in Appendix E.3 operates on the copying task, and, alongside searching over the embedding hyperparameters, experiments with disabling the normaliza- tion features and AdaCos, thereby constituting an ablation study. For the LTL and propositional logic tasks, we always kept the normalization features and AdaCos enabled in the previous sections. In this section, we evaluate the impac of these features by disabling them on our best-performing models for these two logic tasks. We ablate one aspect at time, except for fjn. which is disabled together with Ada- Cos because AdaCos depends on ffn to function correctly.
Motivation for generalization. The generalization to larger AP counts is important especially when considering the exponential growth of the dataset generation time. In Figure 4, we visualize the growth pattern of the trace checking duration based on increasing formula length and AP count. The times are relative to the fastest trace checking time. The exact times will vary depending on the machine. In our experiments, generating 100000 samples of exact formula length 50 with at most 10 APs took 2 hours and 21 minutes on system with 56 threads.
Figure 5 presents the results, which demonstrate the critical importance of the fin normalization component. Removing fun leads to dramatic performance drops (from 90.76% to 29.53% on LTL, and from 77.70% to 14.12% on proposi- tional logic), confirming that maintaining balance between the common and randomized embedding parts is essential for our method's 's success. The experiments with AdaCos and f indicate task-dependent benefits: they provide sig- nificant improvements on LTL 190.76% vs. 81.45% when AdaCos is removed), while showing negligible impact on propositional logic.
Aopha-covariance. On the same generalization dataset, we evaluate the alpha-covariance performance of these models in Table 3. Note that since 10 APs lead to lot more nam- ing permutations than 5 APs, the alpha-covariance values are remarkably smaller compared Table 2. Unlike the results from Table 2, however, our method outperforms the alpha-renaming approach here. This shows that our method
8

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
Table Mean alpha-covariance values for varying AP counts, evaluated on 1000 test samples, each with 120 random alpha-equivalent variants. The best value for each AP count is highlighted in bold.
Alpha-
Oppa-Covariance
Task
Model
3 AP
4 AP
5 AP
6 AP
AP
8 AP
9 AP
10 AP
Full Vocabulary
54.09%
45.51%
45.23%
42.07%
33.54%
34.47%
32.36%
28.42%
LTL
Jipha-Renaming
50.64%
43.00%
40.95%
37.49%
30.80%
30.30%
28.76%
25.57%
Proposed
54.30%
46.05%
45.64%
41.88%
33.89%
35.29%
33.18%
28.34%
Full Vocabulary
39.77%
30.08%
30.37%
26.64%
20.97%
22.97%
18.80%
17.20%
Propositional
Apha-RRnaming
42.29%
32.36%
33.45%
30.28%
24.91%
26.47%
22.29%
19.83%
Logic
Proposed
43.36%
32.49%
33.65%
30.04%
25.00%
26.63%
21.99%
20.75%
5.5. Comparison with L.Ms
6. Limitations
To contextualize the effectiveness of our proposed approach, we evaluate the performance of a ceneral-purposs, LLM (large language model), specifically, the 3B parameter ver- sion of Llama 3.2 (Grattafiori et al., 2024), on the LTL task. The details about the prompt design, inference parameters, and implementation are provided in Appendix I.
While our method provides an effective framework for en- forcing alpha-equivalence in formal languages, it is not directly applicable to natural language, in which tokens carry semantic and contextual information that is often es- sential for interpretation. For instance, even though variable names like electricity biil 11 and water _bilb 11 may be functionally interchangeable in certain code constructs, they convey distinet meanings that are not preserved under As such, enforcing may reduce interpretability and degrade performance in tasks that rely on linguistic connotations. This represents an intriguing area for future research.
In the last row of Table 2, we report the performance of Llama 3.2 on the test split of LTLRandom35. These re- sults (e.g.. 24.33% correct) are drastically lower than those achieved by our proposed method (95.94%). On proposi- tional logic, Llama 3.2 achieves a slightly better accuracy but much worse alpha-covarian
(Table 8 in Appendix G.2). Additionally, we replicate the setups in Figure 3 using Llama 3.2 on the same datasets and sample sizes. As shown in Figure 6, the resulting accuracies are 21.70% (LTII, solv- ing) and 30.92% (propositional logic), compared 90.76% and 77.70% by method. This striking gap illustrates the limitations of general-purpose L.MSs in highly specialized domains such as LTL solving, even when the model size far exceeds that of our dedicated architectures.
Another limitation is the requirement to manually define the set of interchangeable tokens, which may not be feasible in some settings. Moreover, our method requires training from scratch due to modifications in the embedding architecture, posing challenges for integration with pretrained models.
Although dual-part embedding method demonstrates generalization capabilities, its performance in the LTL solv- ing task decreases slightly for in-distribution data (Table 2). The future work can tackle this issue, which may eventu- ally lead to Pareto improvements in biri-variance tradeoff. Finally, new randomization and normalization methods for our embeddings can be explored.
5.6. Computational Efficiency
We evaluate the computational efficiency of our method in terms of training time, inference speed, and memory us- age (see Appendix H for full details). Our method incurs a modest 13% training overhead compared the baseline in LTL solving task. At inference, embedding preparation takes only 0.0003 seconds and is required just once at the beginning of an evaluation session, making its cost neg- ligible relative to model execution (0.206 seconds for a forward pass and 9.808 seconds for autoregressive gener- ation). Our optimized method for generating unique ran- dom vectors with integer reservoir sampling (Section 4.2) scales efficiently to a large number of vectors unlike the naive approach (Figure 7). While the parameter count of traditional embeddings scales linearly with interchangeable token count, our method's 's parameter count remains constant, as embeddings are shared across interchangeable tokens.
7. Conclusion
A central goal in machine learning is to generalize to out- of-distribution samples, for which the model design and its inductive biases play a vital role. In this work, we tackle the challenge of generalizing to larger vocabulary sizes unseen during training and creating an inductive bias for alpha-equivalence. We also contribute the alpha-covariance metric for measuring the model consistency against alpha- equivalent inputs. These contributions embody foundation for learning extensible vocabularies for interchangeable to- kens, which is especially useful for formal reasoning tasks in which -lpha-equivalence naturally arises
9

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
Acknowledgments
Grattafiori, A., Dubey, A., Jauhri, A., Pandey, A., Kadian, A., Al-Dahle, A., Letman, A., Mathur, A., Schelten, A., Vaughan, A., et al. The llama 3 herd of models. arXiv preprint arXiv:2407.21783, 2024.
The numerical calculations were partially performed at TÜBÍTAK TRUBA, MareNostrums, METU ImageLab, and METU ROMER resources. This project was supported in Dr. Cin-
part by the project METU ADEE-312-2222--111 bis is supported by the "Young Scientist Awards Program (BAGEP)" of Science Academy, Türkiye.
Hahn, C., Schmitt, F., Kreber, U., Rabe, M. N., and Finkbeiner, B. Teaching temporal logics neural net- works. In 9th International Conference Learning Representations, ICLR 2021, Viriual Event, Austria, May 3-7, 2021, 2021.
Impact Statement
This paper presents work whose goal advance the field of Machine Learning. There are many potential societal consequences of our work, none which we feel must be specifically highlighted here.
Han, J. M., Rute, J. M., Wu, Y., Ayers, E. W., and Polu, S. Proof artifact co-training for theorem proving with language models. ArXiv, abs/2102.06203, 2021.
Kamienny, P.-A., d' Ascoli, S., Lample, G., and Charton, F. End-to-end symbolic regression with transformers. ArXiv, abs/2204. 10532, 2022.
References
Conversion (Chapter 2). In Barendregt, H. P. (ed.), The Lambda Calculus, volume 103 of Studies in Logic and the Foundations of Mathematics, pp. 22-49. 1984.
Lample, G. and Charton, F. Deep learning for symbolic mathematics. ArXiv, abs/1912.01412, 2019.
Li, J., Yao, Y., Pu, G., Zhang, L.., and He, J. Aalta: an Itl satisfiability checker over infinite/finite traces. In Pro- ceedings of the 22nd ACM SIGSOFT International Sym- posium on Foundations of Software Engineering, FSE 2014, pp. 731-734, New York, NY, USA, 2014.
Abbe, E., Bengio, S., Lotfi, A., and Rizk, K. Generalization on the unseen, logic reasoning and degree curriculum. In Proceedings of the 40th International Conference on Ma- chine Learning, volume 202 of Proceedings of Machine Learning Research, pp. 31 11-60,255 23 29 Jul 2023.
Liu, B., Ash, J. T., Goel, S., Krishnamurthy, A., and Zhang, C. Transformers learn shortcuts to automata. 2023.
Azerbayev, Z., Schoelkopf, H. Paster, K., Santos, M. D., McAleer, S. M., Jiang, A. Q. Deng, J., Biderman, S., and Welleck, S. Llemma: An open language model for mathematics. ArXiv, abs//3100100 10631, 2023.
Morazzoni, I., Scotti, V., and Tedesco, R. Def2vec: Ex- tensible word embeddings from dictionary definitions. International Conference on Natural Language and Speech Processing, 2023.
Baier, C. and Katoen, J.-P. Principles of model checking. 2008.
Clarke, E. M., Henzinger, T. A., Veith, H., and Bloem, R. Handbook of model checking. In Cambridge Interna- tional Law Journal, 2018.
Pnueli, A. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Prov- idence, Rhode Island, USA, 31 October November 1977, pp. 46-57, 1977.
Dargan, S., Kumar, M., Ayyagari, M. R., and Kumar, G. A Survey of Deep Learning and Its Applications: A New Paradigm to Machine Learning, Archives of Com- putational Methods in Engineering, 27(4):107 September 2020. ISSN 1886-1788 1784.
Press, O. and Wolf, L. Using the output embedding to improve language models. In Conference of the European Chapter of the Association for Computational Linguisties, 2016.
Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., and Lauko, H. From Spot 2.0 to Spot 2.10: What's new? In Proceedings of the 34th International Conference Computer Aided Verification (C)V'22), volume 13372 of Lecture Notes in Computer Science, pp. 774-177, August 2022.
Rabe, M. N., Lee, D., Bansal, K., and Szegedy, C. Mathe- matical reasoning via self-supervised skip-tree training. arXiv: Learning, 2020.
A. G., Schlchuber-Caisee
Ranjan, R., Castillo, C. D., and Chellappa, R. L2-
constrained softmax loss for discriminative face verifica- tion, 2017.
Frieder, S., Pinchetti, L., Griffiths, R.-R., Salvatori, T., Lukasiewicz, T., Petersen, P.. Chevalier, A., and Berner, J. Mathematical capabilities of chatgpt. ArXiv, abs/2301. 13867, 2023.
Sanh, V., Webson, A., Raffel, C., Bach, S. H., Sutawika, L., Alyafeai, Z., Chaffin, A., Stiegler, A., Raja, A., Dey, M., Bari, M. S., Xu, C., Thakker, U., Sharma, S. S., Szezechla, E., Kim, T., Chhablani, G., Nayak, N. V.,
10

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
Datta, D., Chang, J., Jiang, M. T.-J., Wang. H., Manica, M., Shen, S., Yong. Z.-X.,, Pandey, H., Bawden, R., Wang. T., Neeraj. T., Rozen, J., Sharma, A., drea Santilli, A.., Févry, T., Fries, J. A., Teehan, R., Scao, T. L., Bider- man, S., Gao, I.., Wolf, T., and Rush, A. M. Multitask prompted training enables zero-shot task generalization. In International Conference on Learning Representations, 2022. URL https: / apii semanticseni Ttt:/ooppusID:27421111
Yang, K., Swope, A. M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A. Leandojo: Theorem proving with retrieval-augmennte language models. ArXiv, 1es/2306.11626,, 2023.
Zhang, X., Zhao, R., Qiao, Y., Wang, X., and Li, H. Adacos: Adaptively scaling cosine logits for effectively learning deep face representations. 2019 IEEE/CVF Conference Computer Vision and Pattern Recognition (CVPR), PP- 10815-10824, 2019.
Shiv, V. L. and Quirk, C. Novel positional encodings to enable tree-based transformers. In NeurlPS 2019, De- cember 2019.
Su. J., Ahmed, M., Lu, Y., Pan, S., Bo, W., and Liu, Y. Roformer: Enhanced transformer with rotary po- sition embedding. Neurocomput. 568(C), February 2024. ISSN 0925-2312.
doi: 10.1016/j.neucom. 2023.127063. URL httpp://il //oii wwt./0...100.. j J.neucom.200 2023 222.2222........
Tang, X., Zheng. Z., Li, J., Meng, F., Zhu, S.-C., Liang, Y., and Zhang, M. Large language models are in-context semantic reasoners rather than symbolic reasoners. ArXiv, abs/2305.14825, 2023.
Vastl, M., Kulhánek, J., Kubalík, J., Derner, E., and Babuška, Symformer: End-to-end symbolic regression using transformer-based architecture, 2022.
Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A. N., Kaiser, L. u., and Polosukhin. I. Atten- tion is all you need. In Advances in Neural Information
Processing Systems, volume 30, 2017.
Vazauez-Chanlatte, M. and Rabe, M. py-aiger. URL https:// com/mvcisback/ pyraiger.
Wang, F., Xiang, X., Cheng. J., and Yuille, Normface:
L2 hypersphere embedding for face verification. In Pro- ceedings the 25th ACM international conference Multimedia, MM '1, October 2017.
Wei, S., Chen, X., Yang, X., Cao, S., and Zhang, X. A component-baseee vocabulary-extensit sign language gesture recognition framework. Sensors (Basel, Switzer- land), 16, 2016.
Welleck, S., Liu, J., Lu, X., Hajishirzi, H., and Choi, Y. Naturalprover: Grounded mathematical proof generation with language models. ArXiv, abs/2205.12911 2022.
Wu, Z., Qiu, L., Ross, A., Akyürek, E., Chen, B., Wang, B., Kim, N., Andreas, J., and Kim, Y. Reasoning or reciting? exploring the capabilities and limitations of language models through counterfactual tasks. In North American Chapter of the Association for Computational Linguistics, 2023.

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
A. Preliminary: Language models
The autoregressive language modeling or sequence modeling in a broader sense- goal is to predict the next token given the past tokens- was revolutionized by the transformer architecture (Vaswani et al., 2017), replacing the step-by-step processing of recurrent neural networks (RNNs) with a parallelizable attention mechanism. At its core lies the attention mechanism, which computes three vectors query, key, and value from input embeddings. This mechanism allows the model to weigh the importance of different tokens, enabling it to capture long-range dependencies efficiently. In self-attention, these vectors come from the same sequence, while in cross-attention, key and value vectors come from a different sequence, as in encoder-decoder setups. The transformer consists of an encoder with self-attention and feed-forward layers, and a decoder that adds coss-attentionn to incorporate the encoder's output. Since attention lacks an inherent sense of token order, positional encodings are added to input embeddings to provide sequence structure. During training, attention masking ensures causality in predictions, preventing future tokens from being considered when predicting the next one.
B. Temporal logic overview
Linear Temporal Logic (LTL) extends propositional logic by introducing the ability to reason about the evolution of propositions over time (Pnueli, 1977). The syntax of LTI,, defined over a finite set of atomic propositions P, is given in Equation 3, where T represents True, p E P an atomic proposition, - the negation operator, A the conjunction operator, X and U the temporal operators next and until respectively.
= T
pl
XΦ
Up2
(3)
Specifically:
X holds at time if and only if é holds at the next time step, i.e., at time t + 1.
Φ1 Uø² means that Φ2 must hold at some future time t2, and Φ1 holds at every time step from the current time i up to but not necessarily including t2.
For instance, the formula XXa specifies that a must hold at the third time step. Similarly, the formula TUa requires that a holds at some point in the future. Finally, as a more complex example, the formula Xb A aUe asserts that b holds the second time step, holds some future time, and holds at all preceding time steps.
An LTL formula is evaluated over a trace, which represents sequence of truth values for atomic propositions over time. In this work, as in DeepLTL (Hahn et al., 2021), we consider symbolic traces of infinite length. These traces are expressed in what is known as a lasso form, denoted und, where is a finite prefix, and v is finite sequence that repeats indefinitely.
symbolic trace represents all traces that satisfy the propositional formulae at the respective time steps. For example, the symbolic trace a, a -b, (c)² describes all traces in which holds at the first two time steps. does not hold at the second time step, and holds at every step from the third onward. This symbolic trace satisfies the formulae TUc and X-b a UC, but it violates the formula XX1 since b is guaranteed to hold the third time step. Symbolic traces, such this one, can be underspecified, meaning that certain propositions (e.g., a and b) may take arbitrary values at some time steps.
The LTL solving problem involves identifying a symbolic trace in lasso form wv that satisfies a given input formula ø. We approach this as an autoregressive language modeling task: given an LTL formula and a partially generated symbolic trace, the model predicts the probabilities for the next token the trace.
For compatibility with the dataset from DeepLTL (Hahn et al., 2021), both our traces and formulae are represented in Polish (prefix) notation, where operators precede their operands. For instance, A b is written as &ab, which avoids the need for parentheses to resolve ambiguities.
As described earlier, we assume that traces are infinite and represented in lasso form wo Alongside atomic propositions, constants (True: 1 and False: 0), and logical operators, we use special symbols in the notation: ";" is a position delimiter, and "(" and ")" enclose the repeating period v. For example, the string "a; &ab; (b)" represents the symbolic trace a, A b, (b)
12

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalenee
C. Propositional Logic
Unlike LTL (Appendix B), propositional logic does not feature any temporal operators, but we include the derived operators for equivalence (++) and exclusive or (o) alongside the basic negation (-), conjunction (A), and disjunction (V). This leads the syntax given in Equation 4, defined over a finite set of atomic propositions where p P atomic proposition.
Φ = T p
- Φ1
A 02 01 V 02
01 + 02 | 02
(4)
In assignment prediction problem for propositional logic, the goal is to determine Boolean assignment for every atomic proposition p P such that the given formula is satisfied. We allow the assignments be partial, e.g.. as 1, valid assignment for the formula V b, so is
which allows b to take any value.
To encode the assignments for the neural network, an alternating sequence of atomic propositions and values is used. For example, alb0 represents the assignment a and = 0. To verify the outputs of the neural network and to generate datasets, pyaiger was used (Vazquez-Chann Chanlatte Rabe).
D. Hyperparameters
The constant hyperparameter choices for all experiments are given in Table 4. These hyperparameters are kept constant within an experiment. The hyperparameters for the logic tasks are taken from DeepLTL (Hahn et al., 2021). For the LTL task, we used the same hyperparameters. On the other hand, for the propositional logic task, we had to make some changes to adapt them to our updated architecture. Firstly, since we utilize weight sharing, we cannot separate the embedding dimensions of encoder and decoder. As a result, instead having an embedding dimension of 128 for the encoder and 64 for the decoder, we use 128 for both. However, since there are 6 attention heads, we round up to 132.
Table 4. Hyperparameter choices.
Experiment
Embedding
Layers
Heads
FC size
Batch Size
Train Steps
Copy (Sections E. and E.2)
64
2
4
64
512
20K
Copy (Section E.5)
128
6
8
128
512
20K
LTL (Section 5.2)
128
8
8
1024
768
52K
Propositional Logic (Section 5.3)
132
6
6
512
1024
50K
E. Copying Task Experiments
Evaluation method. We generate the predictions using greedy sampling in the copying task. We use the edit distance between the prediction and the ground truth as our evaluation metric. To generate the evaluation datasets (validation and test splits), we create 100 samples for each possible combination of unique character count and string length, starting from minimum of Consequently, the total evaluation dataset is arranged in matrix in which the rows represent unique character count the string and the columns represent the string length. This matrix upper triangular since the unique character count cannot exceed the string length. For random embeddings, average. To evaluate up to the string length of 30 in this setup, 10 x 100 x 406 = 406000 predictions are required, where 406 is the number of upper triangular elements in a 28 x 28 matrix. To minimize the impact of random factors, we train each model three times and report the results only for the best.
repeat the evaluation 10 times and report the
E.1. Generalization to larger vocabularies
We create dataset consisting of 10 million strings whose lengths vary between and 30 with at most 5 unique characters. We evaluate the models on strings up to length 30 with at most 30 unique characters. Out of 27 models we trained with dual-part embeddings, 20 of them achieve an average edit distance of 0.0, i.c., no error. The worst model's 's average edit distance is 1.0. For comparison, an output sequence of length 30 can have a maximum edit distance of 30.
13

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalenee
E.2. Generalization to larger vocabularies and lengths
We create dataset consisting of 10 million strings whose lengths vary between and 10 with most 5 unique characters. We evaluate on the same validation set before, expecting the model to generalize to both longer lengths and larger vocabulary sizes. In the next subsection, perform hyperparameter search over random embedding methods, d3 values, and whether Jbn, fnn AdaCos are enabled.
E.3. Hy perpaaaaaeeerr Search
On the smaller copying task, we train multiple models that different random embedding methods (Section 4.2) with different dæ values. While altering dæ. we keep the total number of embedding dimensions da + da constant. We train each model at least times with different seeds and report the results for the best one in Tables 5 (proposed method) and 6 (baselines).
Table Mean edit distance for various models using proposed method. The numbers in the header row represents d, for each random embedding method. In the first column, enabled normalization features listed. AC refers AdaCos, which can only be enabled when fyn is used.
Enabled
Normal Distribution
Neighboring Points
Hypercube Vertiees
Features
2
4
8
16
32
4
6
8
16
32
5
8
16
32
Jon + Jnn + AC
13.6
5.4
4.6
8.1
8.1
1.9
13.0
2.2
1.0
2.1
2.8
0.4
7.5
8,4
3.9
S5a AC
7.6
13.1
4.6
2.2
5.2
8.7
11.5
2.8
2.9
2.2
0.5
3.7
3.2
4.2
4.1
Jbn + fyn ffo
13.7
10.6
8.3
3.8
11.8
11.9
5.7
3.7
7.4
8.3
2.2
13.1
21.5
19.4
20,9
15.4
10.6
8.2
3.7
10.1
8.1
12.3
6.4
13.4
9.9
2.5
1.7
12.5
2.1
12.8
fon
10.6
16.6
11.8
8.2
5.8
3.0
0.6
7.8
14.3
12.8
13.8
19.4
22.9
16.5
11.6
12.6
12.5
9.0
12.5
3.7
9.5
5.9
13.5
12.7
9.6
8.6
15.9
16.6
Table Mcan edit distance for various baseline models. In the first column, enabled normalization features are listed. AC refers AdaCos, which can only be enabled when fto is used. Note that fon is not applicable for baseline models. The results for the first type of baseline are omitted since cannot generalize to larger vocabularies. The second baseline was trained on dataset with vocabulary size of 30. The third baseline uses the same limited vocabulary dataset like the proposed method, but uses alpha-renaming data augmentation.
Enabled
Baseline 2nd Type
Baseline 3rd Type
Features
fin AC
6.1
1.9
fmn
4.9
11.3
5.5
12.9
The results Tables and exhibit high variance with no clear patterns that indicate which methods are better. Therefore. perform analysis based correlation coefficients between these hyperparameters and the edit distance using the results from all 277 models we've trained (not including the baseline models). For this analysis, we assume that the value of Boolcan properties (such as fon. ffn and AdaCos) are 0 or 1. The correlation coefficients are as follows:
N.D.
N.P.
H.V.
dg
fon
frn
AdaCos
0.02
-0.14
0.11
0.01
0.10
-0.29
-0.41
First three columns are the random embedding methods listed in Table 1, the fourth column is dg, and the last three columns represent whether the given feature is enabled. Accordingly, the best random embedding method is "Neighboring Points" since it's the only one that correlates negatively with edit distance. The correlation observed for d, is negligible. Introducing fon increases the edit distance, but the statistical significance is not ideal (p-value 0.04). Both ffn and AdaCos loss have a positive and statistically significant impact on edit distance, with p-values smaller than 10
We determine the best model for the proposed method and the baseline on the validation set, evaluate them on the test set and visualize the results Figure 8. Since the baseline model cannot process larger vocabularies, we assume that the prediction
14

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
empty if the unique character count exceeds the training set's vocabulary, hence the edit distance equals length in that area. Our best model trained on limited length uses Hypercube Vertices with dæ set to 6 and f AdaCos enabled. It achieves mean edit distance of 0.38 on the test set. The first baseline's ' mean edit distance is 0.51 (calculated up to unique characters, only for this model). The second and third baselines' mean edit distances are 4.93 and 1.85 respectively. However, the significance of this difference highly questionable, as these models exhibit high variance across different training runs.
2nd Baseline
3rd Baseline Alpha Raaha-Renmiing
Proposed Method
Baseline
Full Vocabulary
30
6
Unique Characters
9
15
15
18
21
10
5
27
30
12
18 Length
15
21
24
27
30
12
15 Length
18
21
24
27
30
3
12
15 Length
18
21
24
27
30
3
6
9
12
15
18
21
24
27
30
Length
Figure 8. Edit distance heatmaps test set. The first and second healmaps are the proposed and baseline (first type) models respectively. trained on strings up to length 10 and vocabulary size 5. third heatmap is the second baseline, which uses new training dataset with larger vocabulary. The last heatmap is the third baseline that uses the same dataset the proposed method but incorporates alpha-renaming in training. The difference hetween the two baselines that the alpha-renaming baseline is not exposed to more than 5 unique characters per sample. The lower triangular part of each heatmap (gray hatch pattern) represents the impossible combinations of length and unique character count. The green box represents the number of unique characters (y-axis) and the maximum length (x-axis in the training dataset. Note that all heatmaps share the same y-axis.
E.4. Sensitivity to randomness in embeddings
We analyze the impact the randomization that the proposed method performs on embeddings. The minimum, mean, and maximum edit distance (on test set) obtained by ten different embedding randomizations the second model in Figure are 0.25, 0.38, 0.55 respectively, with sample standard deviation of 0.09. The pooled standard deviation the edit distance across all 277 models evaluated on the validation set is 1.73. However, our best models are more resilient against randomness: this value is 0.74 for top 10% models.
To reduce the computational cost of evaluation in other experiments (All LTL experiments and Section E.5), we generate 10 random embeddings, sort them by their cross entropy loss on the evaluated dataset, and use the median one. We find that this serves as decent proxy for the average performance. Across the validation set evaluations of all 277 models, the percent difference in edit distance between this median method and the real mean is 1.4% on average (meaning that the result from the median method is worse), and 9.1 % if we consider the absolute differences.
E,5. Scaling up
We increase the length of the strings from 5-10 to 20-80, and vocabulary size from 5 to 20. We create the evaluation sets by generating 20 samples for each combination of unique character count and string length. The mean edit distance of our best model 0.0. The heatmap given Figure 2. All baselines also attain perfect performance this task on the vocabulary sizes they support. Therefore, only the first type of baseline is shown in Figure 2.
F. LTL Experiment with Limited Dataset
This is continuation of the experiment from Section 5.2.1. Table 7 contains evaluations the baseline, the alpha-renaming model, and the proposed model trained with a severely limited number of samples: 80,000 instead of 799,909. We kept the number of epochs constant, and result, the number of training steps were also divided by ten (approximately).
15

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
The result of limiting the number of training samples is similar to the dataset perturbation, albeit much less pronounced for the baseline model. Unlike in the perturbation experiment, where the baseline model's performance plummets, all models trained on the reduced dataset maintain similar correctness ratios. The biggest difference is observed in the alpha-covariance values, particularly in the 5 AP category, whose ranking aligns with the perturbation experiment.
Since L.L.Random35 synthetic dataset, it exhibits minimal inherent bias, even when the dataset size is limited. Consequently, limiting the dataset size has a smaller effect than introducing perturbations. Furthermore, since the alpha- renaming model was trained using 5 AP embeddings in this experiment, it loses vocabulary generalization capability unlike our proposed method. Training the alpha-renaming baseline with more APs would require learning a new embedding for each AP, which would reduce its performance.
Table Evaluation the baselines and our method trained on different versions of Random335. The same results from Table are shown for casier comparison. The alpha-renaming baseline was trained using AP embeddings since vocabulary generalization is not evaluated here. First two columns denote the training dataset and the model. Next two columns indicate the ratio the correct predictions and exact matches 99, 989 test set samples evaluated by spot. Last three columns display mean alpha- covar-cne values for varying atomic proposition (AP) counts, evaluated on all dipha-cquivalens variants of 1000 test samples.
Training
Evaluation
Alpha-Cors Covariance
Dataset
Model
Correct
Exact
3 AP
4 AP
5 AP
Normal
Baseline
98.23%
83.23%
96.87%
95.86%
91.80%
Perturbed
Baseline
34.13%
12.12%
64.93%
57.99%
40.91%
Perturbed
Alpha-Renaming
97.96% %
77.66 %
99.55%
99.49 %
98.86%
Perturbed
Proposed
95.94%
76.45%
97.66%
97.76%
98.29%
Limited
Baseline
87.47%
63.61 %
94.37%
91.70%
85.64%
Limited
Alha-RRenamng
89.50 %
64.15% %
99.02%
98.67 %
97.82%
Limited
Proposed
87.32%
59.04%
97. 97.94%
96.12%
94.34%
G. Propositional Logic Experiments
This section gives more details about the experimental setup of the propositional logic task and continues the experiments.
G.1. Experimental Setup
We use PropRandom35 from DeepLTL (Hahn et al., 2021) as our main 5 AP dataset, and create other datasets using the same approach. In particular, propositional logic formulae are generated randomly, with negation (-), conjunction (A), and disjunction (V) operators having equal weight. Equivalence (+>) and exclusive (@) operators each have half as much weight since they are derived operators. The corresponding assignment is generated by querying the pyaiger's SAT solver for minimal unsatisfiable core of the negated formula.
As in the LTL experiments, we use a transformer encoder-decoder architecture with three-way weight tying (Press & Wolf, 2016). The positional encoding method is tree-positional encoding (Shiv & Quirk, 2019) for the encoder and RoPE (Su et al., 2024) for the decoder. Predictions are generated using beam search with a beam size of 3.
Since the network outputs the assignments as a sequence (Appendix C), the same assignment can be encoded in multiple ways by changing the order. For example, both alb0 and b0al represent the same set of assignments which can be written as ((a, 1), (b, }}} in set notation. We consider such pairs exact matches in the propositional logic experiments. If the predicted assignment does not exactly match the ground truth, we use pyaiger to evaluate the correctness.
and 0,
G.2. Dataset Perturbations
In this section, we repeat the dataset perturbation experiment (Section 5.2. for the propositional logic task. The perturbation is introduced in a similar manner by renaming the APs such that the order of the first AP appearances in the label (sequence denoting the Boolean assignment) is always the same. As shown in Table 8, the experimental results once again confirm that our method introduces a robust inductive bias for alpha-equivalence.
16

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
Table Evaluation of the baselines, our method, and Llama 3.2 the PropRandom33 dataset. The alpha-renaming bascline was trained using 5 AP embeddings since vocabulary generalization is not evaluated here. First two columns denote the training dataset and the model. Next two columns indicate the ratio of correct predictions exact matches on 100,000 test set samples as evaluated by pyaiger. Last three columns display mean alpha-covariance values for varying atomic proposition (AP) counts, evaluated on all alpha-equivalent variants 1000 test samples.
Training
Evaluation
Alpha-Cove Covariance
Dataset
Model
Correct
Exact
AP
4 AP
AP
Normal
Baseline
95.62%
57.94%
95.70%
93.69%
76.02%
Perturbed
Baseline
41.57%
9.04%
14.96%
16.85%
10.65%
Perturbed
Apha-Renaming
93.85%
57.24%
99.56%
99.60%
93.23%
Perturbed
Proposed
93.25%
56.45%
99.23%
99.42%
92.98%
Pretrained
Llama 3.2 3B
29.03%
1.56%
50.75%
27.96%
11.25%
H. Computational Efficiency Details
To evaluate the practical applicability of our method, we analyze its computational overhead compared to baseline approaches. We report training times, inference speeds, and memory requirements across different experimental settings.
Training efficiency. We measured training durations for models trained on NVIDIA H100 GPUs using identical hyperpa- rameter settings. In LTL solving task, the average training times were as follows:
Baseline (traditional embeddings): 2 hours 12 minutes
Alpha-renaming baseline: 2 hours 33 minutes
Proposed method: 2 hours 29 minutes
The proposed method introduces minimal training overhead compared to the baseline, with only 13% increase in training time. This modest overhead stems from the additional embedding preparation steps required during training.
Inference performance. We conducted a runtime analysis using our best-performing LTL model on NVIDIA A4000 hardware. The model uses Hypercube Vertices randomization with uniqueness checking enabled, evaluated with batch size 768 and beam search (beam size = 3). In this setup, a forward pass takes 0.206 seconds, and autoregressive generation 9.808 seconds. On the other hand, the embedding preparation time is measured at 0.0003 seconds, which is negligible compared model execution. Importantly, during inference, embeddings need only be generated once the start of the evaluation session, making the amortized cost even smaller for batch processing.
Memory overhead. Our method reduces the total parameter count compared to traditional approaches since only one common embedding is learned for all interchangeable tokens, regardless of their quantity. The memory overhead comes primarily from constructing the embedding matrix during runtime, which requires temporary storage for the randomized components. However, this additional memory requirement on the same order of magnitude the embedding matrix itself, which represents a small fraction of total model parameters in transformer architectures.
The parameter efficiency of our method scales favorably with vocabulary size. Unlike traditional approaches that require learning separate embeddings for each token (thereby scaling linearly with the vocabulary size), our method's parameter count remains constant regardless of the number of interchangeable tokens. However, two factors require consideration for very large vocabularies:
1. Sampling set size: In discrete random generation methods, the sampling set is naturally bounded (Table 1). However, the sampling set grows exponentially with the number of dimensions, ensuring sufficient diversity even for large vocabularies.
2. Uniqueness checking: For vocabularies with hundreds of thousands of tokens, uniqueness verification becomes computationally expensive, but the probability of collisions decreases exponentially with increasing embedding dimensions.
17

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
I. LLM Setup
use 3B-parameter version Llama 3.2 (Grattafiori et al., 2024), quantized with Q4_K__, and run using Ollama 0.4.7 our LLM backend. We first experimented with greedy sampling (by setting top-k=1) since Ollama does not support beam search. However, found that the default sampling options (top-k=40 and top-p=0.9) yielded better results. Therefore, these default settings for all experiments.
Unlike our specialized models, which operate on prefix (Polish) notation, we prompt the LLM using infix notation for input formulas (and output traces in the LTL task), as this format is more prevalent in natural language and more familiar to general-purpose LLMs. To output the assignments in the propositional logic task, we use JSON format, and constrain the LLM's output using a JSON schema. The input prompts the LTL and propositional logic tasks are given in Listing and Listing 2, respectively. For each sample, the " [formula) substring in the prompt is replaced by the input formula, and the prompt given user message to the LLM.
We set the random seed to 42 for each sample. Although the reason behind this choice is reproducability, it also seems to improve alpha-covariance. For example, the alpha-covariance values reported for Llama 3.2 in Table 2 are 68.17%, 63.27%, 62.34% for to 5 APs, respectively, which decrease to 41. 1194%, 43.10% 44.62% when the random seed is no longer fixed.
Listing LLM Prompt for the LTL solving task. Your task is to generate a satisfying trace for a given LIL (Linear Temporal Logic) formula.
Lowercase letters denote the atomic propositions. The output trace should be in lassc form composed of parts: the prefix part and the cycle part.
Timesteps in the trace should be separated by semicolons, and the cycle part should be enclosed in curly braces, preceeded by the keyword "cycle".
remporal operaters:
x: Next operator
U: Until operator
Logical operators:
11 a: AND operator
12 I: OR operator
13 !: NOT operator
The output trace is symbolic trace, which means that the logical operators are allowed, but not temporal operators.
15
16 Constants:
17 0: False
1: True
19 Note that other numbers are invalid.
20
21 Example 1
Formula: (((a Xa) U xXb) cycle!(1))
Trace: 1;
24
25 Example 2
26 Formula: !c U X(1 U b)
Trace: 1; b; cycle((1))
28
29 Example 3
30 Formula: XIx! (b & xb)
Trace: 1; 1; b; by cycle((1)) 12
33 Example
34 Formula: (11 D !c)
35 Trace: cyclellcl1
37 Your Turn
38 Formula: (formula)
39 Please generate the corresponding trace. Output the trace only.
18

---

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalenee
Listing 2. LLM Prompt for the propositional logie task.
Your task is to generate an assignment that satisfies a given proposi propositional tional logic formula. Lowercase letters denote the atomic propositions. The output is JSON object representing the assignment.
Logical operators (ordered from highest precedence to :
:: NOT operator
&: AND operater
operater
xor: Exclusive OR operator
10 <->: logical equivalence operator (biconditiona
11
12 Constants:
D: False
14 1: True
15 Note that other numbers are invalid.
16
Example 1
18 Formula: !a
c)
19 Assignment: "a": false }
20
Example 2
Formula: ! (a <-> (!a !e))
23
Assignment: "a": true, "e": true
24
25 Example 3
Formula: (!a <-> !o d)
27 Assignment: "a"; true, "c": true, "d"; false }
28
29 Example
30 Formula: ! (a | !!!d b & d))
Assignment: "a"; false, "d": false
32
33 Your Turn
34 Formula: (formula)
Please generate an assignment that satisfies this formula. Cutput the assignment only, in JSON format.
19


Reviews:
[{"review_id": "uC3Oct2ig7", "reviewer": "Reviewer_u7Gr", "summary": "The paper proposes a method for handling interchangeable tokens—like bound variables—in language models by splitting token embeddings into a shared semantic part and a unique random part. This improves generalisation to unseen vocabularies and supports alpha-equivalence. Evaluated on copying tasks, LTL solving, and propositional logic, the approach shows improved robustness and consistency, particularly under vocabulary shifts.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We kindly thank the reviewer for their positive feedback.\n\n> If I understand correctly, the proposed techniques are designed for problems—like LTL and propositional logic—where the grammar is clear or simple enough to reliably identify bound variables. How well do you think these techniques would generalise to settings where that’s not the case—for example, natural language tasks without well-defined grammar, or programming languages where the abstract syntax tree isn’t readily available?\n\nIt is correct that the method we proposed in this paper needs bound variables to be identified. As the reviewer noted, the situations in which this is not possible can be divided into two categories.\n\n**1\\. Natural language**\n\nWe believe that applying alpha-equivalence in natural language settings requires different considerations. Let us demonstrate this through an example that involves programming with natural language variable names.\n\nConsider the functions `get_total_bill(electricity_bill, water_bill) = electricity_bill + water_bill` and `get_end_time(start_time, duration) = start_time + duration`. Although these two functions perform the same operation, the additional meaning conveyed through the variable names may be relevant in a larger context. Therefore, alpha-equivalence does not hold in natural language statements in a strict sense since these variable names are not truly interchangeable. A function like `get_end_time(start_time, water_bill) = start_time + water_bill` would be nonsensical despite being functionally equivalent to aforementioned examples.\n\nIn addition, each word carries connotations in addition to the primary, literal meaning. For instance, many programmers use the variable name `i` for iterating over indices. Although renaming this variable would result in a functionally equivalent code, it may confuse an LLM.\n\nTo summarize, since our method depends on randomizing the discernable parts of the interchangeable tokens, a trade-off arises between enforcing alpha-equivalence and preserving semantics/connotations in natural language contexts. As a result, application to natural language—albeit beyond the scope of this paper—is an interesting direction for future work as we noted in the conclusion section.\n\n**2\\. The abstract syntax tree (AST) isn’t readily available**\n\nWe thank the reviewer for highlighting this interesting point. Since our focus in this work is formal languages, we believe it’s reasonable to assume that AST can be parsed as needed. In addition, in many formal languages, identifying the bound variables does not require parsing the full AST either. For example, our implementation actually does not depend on AST being available to detect interchangeable tokens because the set of AP (atomic proposition) tokens is predetermined. Similarly, if an alternative preprocessing approach can identify the bound variables in other languages, AST may not be needed.", "claims_and_evidence": "Yes, both full vocabulary and alpha-renaming are natural approaches to address the challenge of extended vocabularies in the context of alpha-equivalence. The fact that the proposed method performs competitively with these strategies—despite being trained on a limited vocabulary—is impressive and clearly highlights its value.", "methods_and_evaluation_criteria": "Overall, it’s very good. It would be even more interesting to see the proposed method validated on a real-world programming task where alpha-equivalence naturally occurs—but I’m already quite satisfied with the current experimental setup.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "Looks good to me.", "relation_to_broader_scientific_literature": "Bound variables and alpha-equivalence are common in real-world mathematical reasoning and programming tasks. I fully appreciate the value of this paper in addressing challenges related to unseen variables.", "essential_references_not_discussed": "No to the best of my knowledge.", "other_strengths_and_weaknesses": "- The paper is well written, easy to follow, and with illustrative figure/experiment to validate its hypothesis\n- I really appreciate the introduction of alpha-covariance, which quantifies the model's ability to tackle alpha-conversions.", "other_comments_or_suggestions": "N/A", "questions_for_authors": "If I understand correctly, the proposed techniques are designed for problems—like LTL and propositional logic—where the grammar is clear or simple enough to reliably identify bound variables. How well do you think these techniques would generalise to settings where that’s not the case—for example, natural language tasks without well-defined grammar, or programming languages where the abstract syntax tree isn’t readily available?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "1ScWwNrEGy", "reviewer": "Reviewer_d1BV", "summary": "The authors propose an interesting token embedding technique to handle alpha-equivalent programs—those that share the same semantic meaning but differ in surface representation. By employing a dual-part token representation, the embedding effectively captures both semantic consistency and token distinguishability. Compared to the baseline, which relies on data augmentation with alpha renaming, this approach demonstrates improved generalizability in reasoning outcomes.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We kindly thank the reviewer for their comments.\n\n> Does the formal language include natural elements, such as comments and textual descriptions? If so, could the embedding approach lead to representational conflicts when switching between these contexts?\n\nThe applications we considered in this paper do not include natural language comments or descriptions.\n\n> Alpha-covariance appears to be defined exclusively for LTL formulas. Is it a highly specialized metric that applies only to LTL programs?\n\nNo, alpha-covariance is not specific to the LTL domain. It is applicable in any domain where alpha-equivalence is relevant. Most prominently, this includes formal languages where user-defined variables are present, such as programming languages. For example, we could use alpha-covariance to measure how sensitive a model is to renaming bound variables in a Python programming task.\n\n> To strengthen its impact, it would be valuable to demonstrate its effectiveness on a real-world LTL dataset that includes human annotations and comments.\n\nSince our method randomizes the discernable parts of the interchangeable tokens to enforce alpha-equivalence, applying our method as-is in a natural language setting would remove the discerning semantics from the variable names. This is an important trade-off as we elaborated further in our discussion with Reviewer u7Gr. As our focus in this work was formal languages, we left this direction for future work.\n\n> Handling domain shift in evaluation: In the current setup, the baseline model is trained on a perturbed dataset but tested on the original test set. Why not apply an actual alpha-conversion step as a preprocessing step during testing to mitigate domain shift and ensure a more direct evaluation of robustness?\n\nFirstly, we would like to emphasize that only in one experiment the baseline model was trained on a perturbed dataset. Since the purpose of this experiment is to measure the generalization capabilities, introducing a perturbation allows us to see how models perform when the training dataset is biased.\n\nIn the rest of the experiments, the baselines were not subjected to any perturbations during training.\n\nApplying alpha-conversion as a preprocessing step during testing, as suggested by the reviewer, is performed in alpha-covariance experiments.\n\n> Comparison with general-purpose code language models: How do existing large-scale code models, such as Codex, perform on these tasks? Evaluating their performance could provide a stronger baseline and contextualize the effectiveness of the proposed approach.\n\nWe thank the reviewer for this suggestion.\n\nWe evaluated Llama 3.2 (3B ollama version) on the LTL task. In the prompt, a brief description of the task and several examples were given. The LLM is asked to generate the output trace only. Unlike our models, the input formulas and the output traces are encoded in infix notation instead of prefix (Polish) notation since general-purpose LLMs are more familiar with infix notation due to its popularity in natural language.\n\n**Results on LTLRandom35 Test Split (over 10000 samples):**\n\n* Correct: 25.3%  \n* Alpha Covariance 3, 4, 5 AP: 87.83%, 83.48%, 86.69%. (All permutations of 100 samples for each AP)\n\nThese results should be compared to those in Table 2, cf. Proposed \\- Correct: 95.94%.  \n   \nAs a larger example, we also evaluate Llama 3.2 using the same dataset and sample size as in Fig. 3a from the paper. We cannot include images in this rebuttal, but the overall accuracy is 21.38%, cf. 92.37% (Proposed). Although Llama 3.2 is a small model by LLM standards, its size still dwarfs all dedicated models we evaluated in the manuscript. Despite this, as a general-purpose model, it performs much worse than the dedicated models since LTL is a highly specialized domain. Even though LLM performance could be improved by using larger models and/or various CoT techniques, we hope that these results help put the results from the paper into context.\n\nAfter the rebuttal period, we will update the paper according to this discussion.", "claims_and_evidence": "**Claim1**. Identify the challenge of generalizing to larger vocabularies in (formal) language modeling tasks and define an experimental protocol to systematically study this problem.\n\n**Question**: Does the formal language include natural elements, such as comments and textual descriptions? If so, could the embedding approach lead to representational conflicts when switching between these contexts?\n\n**Claim2**. Propose alpha-covariance, a novel metric for measuring robustness against alpha-conversions.\n\n**Question**: Alpha-covariance appears to be defined exclusively for LTL formulas. Is it a highly specialized metric that applies only to LTL programs?\n\n\n**Claim 3:** Introduce a dual-part embedding method to enhance vocabulary generalization and improve alpha-covariance.\n\nThis claim is well supported.\n\n**Claim 4:** Verify the proposed method thoroughly on three tasks: copying with extendable vocabulary, solving LTL formulae, and predicting assignments for propositional logic.\n\n**Question:** The applicability of this embedding technique seems limited to synthetic datasets, particularly those derived from PropRandom35 in DeepLTL. To strengthen its impact, it would be valuable to demonstrate its effectiveness on a real-world LTL dataset that includes human annotations and comments.", "methods_and_evaluation_criteria": "The dual embedding method is conceptually sound, but I believe there are two key aspects that the evaluation has not sufficiently addressed:\n\n1. Handling domain shift in evaluation:\nIn the current setup, the baseline model is trained on a perturbed dataset but tested on the original test set. Why not apply an actual alpha-conversion step as a preprocessing step during testing to mitigate domain shift and ensure a more direct evaluation of robustness?\n\n2. Comparison with general-purpose code language models:\nHow do existing large-scale code models, such as Codex, perform on these tasks? Evaluating their performance could provide a stronger baseline and contextualize the effectiveness of the proposed approach.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "See Methods And Evaluation Criteria and Claims And Evidence", "relation_to_broader_scientific_literature": "This work is generally related to the field of programming model.", "essential_references_not_discussed": "[1] Finnie-Ansley, James, et al. \"The robots are coming: Exploring the implications of openai codex on introductory programming.\" Proceedings of the 24th Australasian computing education conference. 2022.", "other_strengths_and_weaknesses": "The paper is clearly written and easy to follow.", "other_comments_or_suggestions": "N/A", "questions_for_authors": "See Methods And Evaluation Criteria and Claims And Evidence", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "EOr1wgaS2R", "reviewer": "Reviewer_Yaj6", "summary": "The paper introduces a novel method for handling interchangeable(semantically equivalent yet distinct) tokens in a language model. The proposed approach uses a dual-part token embedding strategy consisting of a shared semantic component and a randomized component to ensure distinguishability. The paper also introduces a new metric- alpha covariance to evaluate robustness to alpha-equivalent transformations(where renaming bound variables preserves meaning). The proposed approach is evaluated on three tasks and is shown to to generalize better than the baseline methods.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We kindly thank the reviewer for their detailed analysis.\n\n> **The method generalizes better than data augmentation**: This claim needs stronger justification as the the alpha-renaming method performs better than the proposed method in Table 2 and a deeper analysis is required to justify this.\n\nWe would like to emphasize that the alpha-renaming baseline in Table 2 was trained using only 5 APs instead of 10 (as in Fig. 3\\) since the purpose of this experiment was to evaluate alpha-covariance rather than generalization. In other words, all models in Table 2 were trained and evaluated on in-distribution data. Therefore, we believe we can conclude that although alpha-renaming achieves better performance on in-distribution data, the proposed method generalizes better to out-of-distribution data, as seen in Fig. 3\\.\n\n> The random embedding approach is critical to success: Proper ablation studies are required to make this claim stronger\n\nFirstly, we note that in Appendix E.3, alongside the hyperparameter search over embedding hyperparameters, we performed ablation studies on the copying task by disabling the normalization features and AdaCos.\n\nHere, we perform a similar experiment on two logic tasks. We use the best hyperparameters that we found and used in Fig. 3\\. We train each model multiple times and report the test-split results for the model that performs the best in the validation set. The values we report in this section correspond to the overall accuracy values reported in Fig. 3\\. We ablate one aspect at a time, except for $f_{fn}$. Because AdaCos requires $f_{fn}$ to function correctly.\n\n**LTL task**\n\n* Proposed Model (Fig. 3a): 92.37%  \n* Without AdaCos: 84.69%  \n* Without $f_{fn}$ & AdaCos: 84.04%  \n* Without $f_{bn}$: 32.27%\n\n**Propositional logic task**\n\n* Proposed Model (Fig. 3b): 80.72%  \n* Without AdaCos: 81.13%  \n* Without $f_{fn}$ & AdaCos: 80.41%  \n* Without $f_{bn}$: 15.05%\n\nThe results indicate that $f_{bn}$ is absolutely necessary for both tasks. This is intuitive because it keeps the balance between the common and randomized parts of the embedding. $f_{fn}$ is less important but still helpful. The performance of AdaCos varies depending on the task. On LTL, ablating AdaCos decreases the accuracy from 92.37% to 84.69%. However, on propositional logic, AdaCos does not make a clear difference in accuracy.\n\n> Can you add details on memory and time overhead?\n\nPlease see our discussion with Reviewer xcub.\n\n> Can you discuss the scalability tradeoffs as you scale to larger vocabularies beyond a few hundred thousand tokens.\n\nUnlike other approaches, our method only needs to learn a single common part for all interchangeable tokens, even if there are thousands of them. However, the hyperparameter choices regarding the randomized embedding part requires some special considerations. Notable scalability concerns include:\n\n1. Sampling set size of the random generation method: As outlined in Table 1, using a discrete random generation method leads to a limited sampling set size. However, since it grows exponentially with the number of embedding dimensions, this can be addressed by simply increasing the dimensions of the random embeddings. Nevertheless, larger embedding dimensions may call for an overall increase in model size.  \n2. Ensuring the uniqueness of the random embeddings: Increasing the number of embedding dimensions makes uniqueness checks harder (see line 190). But at the same time, due to the increased sampling set size, the probability of generating the same embedding decreases to the point where it’s essentially negligible.\n\n> Does this approach work for larger models like GPT-4?\n\nIn principle, the proposed approach doesn’t have a limitation that disallows us from using it on larger models. But there are several aspects that need to be considered:\n\n1. Natural language: As discussed in our response to Reviewer u7Gr, natural languages don’t conform to alpha-equivalence, which leads to a trade-off between enforcing alpha-equivalence and preserving variable name semantics.  \n2. Identifying interchangeable tokens: Our method requires interchangeable tokens (variables) to be identified in advance since their embeddings are handled in a special way.  \n3. Training from scratch: Since our method changes the architecture of the embeddings, it requires training the whole model from scratch. However, future work may potentially address this.\n\nAfter the rebuttal period, we will update the paper according to this discussion.", "claims_and_evidence": "The paper makes the following claims:\nClaims with sufficient support:\n1. **Language models struggle with interchangeable tokens and alpha-equivalence** : Experiments shown in Table3 supports the claim\n2. **The proposed dual-embedding strategy helps improve generalization to larger vocabularies**: Results in Table 2 and Figure 2 support the claim.\n3. **The model introduces an inductive bias that makes it robust to data perturbations** : Results in Table 2 support this.\n\nClaims that require further justification:\n4. **The method generalizes better than data augmentation**: This claim needs stronger justification as the the alpha-renaming method performs better than the proposed method in Table 2 and a deeper analysis is required to justify this.\n5. ** The random embedding approach is critical to success** : Proper ablation studies are required to make this claim stronger\n6. **The proposed approach is computationally efficient**: A runtime analysis is required to compare with standard embeddings", "methods_and_evaluation_criteria": "Yes, the overall framework makes sense, however there is room for improvement:\n1. The proposed approach is evaluated on three tasks which are relevant to the problem. However, it would be good to add a real world dataset in addition to these synthetic datasets.\n2. The paper proposes a new metric alpha-covariance which is relevant for the problem at hand. However, it should also talk about memory and time overheads of the proposed approach to baselines.", "theoretical_claims": "No", "experimental_designs_or_analyses": "No", "relation_to_broader_scientific_literature": "The paper has two key contributions:\n1. Dual-embedding strategy to scale to unseen tokens. This is one of the ways to expand the vocabulary in specific settings such as logic and reasoning with alpha-equivalent representations. This extends vocabulary without retraining, enabling systematic generalization.\n2. Alpha-covariance: A new metric to measure robustness to alpha-equivalence: This provides a new way to measure symbolic consistency.", "essential_references_not_discussed": "NA", "other_strengths_and_weaknesses": "Strengths:\n1. The paper is well-written and easy to follow.\n2. There are extensive experiments on 3 datasets to support the claims.\n\nWeaknesses:\n1. There are no results on large-scale language models to see if the proposed approach works for GPT-4 like larger models.\n2. The paper evaluates on synthetic datasets but it raises concerns whether this proposed approach generalizes to real-world applications.\n3. The paper does not discuss about the scalability tradeoffs, specifically as we scale to extremely large vocabularies.", "other_comments_or_suggestions": "Section 3: Line 94: V* is not defined\nSection 3: V_i is not defined\nTypo: Section 4.2 Line 159: need make sure -> need to make sure\nTypo: Abstract Line 37: toward-> towards", "questions_for_authors": "1. Can you add details on memory and time overhead?\n2. Can you discuss the scalability tradeoffs as you scale to larger vocabularies beyond a few hundred thousand tokens.\n3. Does this approach work for larger models like GPT-4?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "yJ4QVYb6nV", "reviewer": "Reviewer_xcub", "summary": "The paper introduces a way to handling interchangeable tokens in neural networks, particularly for tasks involving formal logic and symbolic reasoning. The proposed method employs a token embedding strategy that combines a shared component for semantic consistency and a randomized component for token differentiation. The authors also define a metric called alpha-covariance to measure robustness against alpha-equivalent transformations. The method is evaluated on three tasks: copying with an extendable vocabulary, linear temporal logic (LTL) solving, and propositional logic assignment prediction. Results show improved generalization to unseen tokens and an inductive bias favoring alpha-equivalence.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We kindly thank the reviewer for their constructive criticism.\n\n> The embedding matrix is constructed with a fixed number of interchangeable tokens, which suggests that the set of interchangeable tokens must be predetermined before training.\n\nThis is the case for the alpha-renaming baseline, but not exactly true for our proposed method. The embeddings we propose are composed of two parts: a learnable common part, and a random part. Thanks to the random part, we can generate as many embeddings for the interchangeable tokens as needed, both in training and inference. The only limitation here is that when a discrete random generation method is used, the sampling set for the random part is naturally limited (Table 1 in the submission). However, since the sampling set grows exponentially as the number of dimensions increases, this is not a problem in practice.\n\n> The structure of symbolic expressions significantly differs from natural language expressions. This potentially limits the model’s applicability to tasks involving human-readable variables.  \n>  \n> It would be interesting to explore whether this approach generalizes to broader NLP tasks beyond symbolic reasoning.\n\nWe agree that applying these ideas to natural language expressions requires vastly different considerations and therefore, left beyond the scope of this paper. Please also refer to our discussion with Reviewer u7Gr for more information.\n\n> It would be useful to report computational efficiency metrics (e.g., training time, inference speed).\n\nWe have used a variety of hardware for training. But among the models that we trained using NVIDIA H100, the average training durations are approximately as follows:\n\n1. **Baseline:** 2 hours 12 minutes  \n2. **Alpha-renaming Baseline:** 2 hours 33 minutes  \n3. **Proposed method:** 2 hours 29 minutes.\n\nWe performed a simple benchmark to analyze the runtime performance of our best LTL model using NVIDIA RTX A4000 (randomization method is “Hypercube Vertices”, with uniqueness checking enabled):\n\n- **Preparing embeddings:** 0.0003 seconds  \n- **Forward pass:** 0.206 seconds  \n- **Autoregressive generation:** 9.808 seconds\n\nWe used a batch size of 768 in both forward pass and autoregressive generation, as noted in Table 4\\. For autoregressive generation, we used beam search with a beam size of 3\\. These were the settings we used in all LTL experiments.\n\nNote that as our method does not alter the internal architecture of the model, the only additional requirement is preparing the embeddings.\n\nAs the benchmark results indicate, the extra computational cost introduced by our method is negligible compared to running the model. Furthermore, during inference, it is sufficient to generate the embeddings once at the start.\n\n**Memory overhead:** Our method does not increase the parameter count of the model. On the contrary, model parameters are actually reduced since only one common embedding is learned for all interchangeable tokens. Constructing the embedding matrix may require some extra memory (e.g., for generating the randomized part) but it’s in the same order of magnitude as the embedding matrix, which is quite small compared to the rest of the model parameters.\n\n> Is it necessary to explicitly define the set of interchangeable tokens before training, or can the model learn to infer interchangeable tokens dynamically during the training process?\n\nThe set of interchangeable tokens must be identified in advance. The model currently cannot learn which tokens are interchangeable.\n\n> Would the proposed method still be effective if applied to tasks with human-readable variable names instead of abstract symbolic tokens?\n\nSince enforcing alpha-equivalence using our method would remove the word meanings from interchangeable tokens (only discerning property for interchangeable token embeddings is the randomized part), there is a trade-off between exploiting alpha-equivalence and reasoning from natural language semantics. We have also elaborated on this in our discussion with Reviewer u7Gr.\n\nOvercoming the said trade-off is an interesting research direction as noted in the conclusion section of our submission.\n\n----\n\nAfter the rebuttal period, we will update our paper according to this discussion.", "claims_and_evidence": "* Traditional language models fail to recognize alpha-equivalence.\n    - Evidence: Experiments on symbolic reasoning tasks demonstrate poor generalization with traditional embedding methods.\n\n* The proposed dual-part embedding enhances a model’s ability to handle interchangeable tokens.\n    - Evidence: Evaluations on copying, LTL solving, and propositional logic tasks show performance improvement", "methods_and_evaluation_criteria": "The authors adopt a Transformer encoder-decoder architecture with RoPE positional encoding.\n\nEvaluation metrics include accuracy, edit distance, and alpha-covariance.\n\nThe proposed model is compared against learned embeddings and an alpha-renaming-based baseline.", "theoretical_claims": "No theoretical claim was made in this work.", "experimental_designs_or_analyses": "* Experiments cover three tasks. Tests evaluate both in-distribution and out-of-distribution generalization. \n* There is an ablation on hyperparameter search to explore the impact of different embedding structures.", "relation_to_broader_scientific_literature": "No direct relation to broader scientific literature.", "essential_references_not_discussed": "The paper covers relevant literature on neural-symbolic reasoning and transformer-based formal logic models.", "other_strengths_and_weaknesses": "**Strengths**\n\n* The method is well-motivated with clear formalization.\n\n* Comprehensive experimental validation across multiple tasks.\n\n* Strong empirical results demonstrating out-of-distribution generalization.\n\n**Weakness**\n\n* The embedding matrix is constructed with a fixed number of interchangeable tokens, which suggests that the set of interchangeable tokens must be predetermined before training.\n\n* The structure of symbolic expressions significantly differs from natural language expressions. This potentially limits the model’s applicability to tasks involving human-readable variables.", "other_comments_or_suggestions": "* It would be interesting to explore whether this approach generalizes to broader NLP tasks beyond symbolic reasoning.\n\n* It would be useful to report computational efficiency metrics (e.g., training time, inference speed).", "questions_for_authors": "* Is it necessary to explicitly define the set of interchangeable tokens before training, or can the model learn to infer interchangeable tokens dynamically during the training process?\n\n* Would the proposed method still be effective if applied to tasks with human-readable variable names instead of abstract symbolic tokens?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: The reviewers all agree on the utility of the proposed method for encoding interchangeable tokens within a language model. Identified strengths include:
* The paper is well written and easy to follow.
* The alpha-covariance metric  is appropriate for evaluating robustness to renaming of interchangeable tokens.
* The claim that existing language models struggle with interchangeable tokens and alpha-equivalence, is clear and supported by experimental results.
* The proposed dual-embedding strategy is shown to improve generalization to larger vocabularies.
* Training on full vocabulary and alpha-renaming are natural approaches to address the challenge of extended vocabularies in the context of alpha-equivalence and hence appropriate baselines. The proposed method, given it's limitations, performs well against these baselines in experiments.

The reviewers raise some questions and limitations including:
* A number of questions about how this method can be extended to more naturalistic data settings, including those without a well-defined grammar/syntax.
* The claim that the proposed method generalizes better than data augmentation: needs stronger justification as the the alpha-renaming method performs better than the proposed method in Table 2 and the work would benefit from a deeper analysis of this.
* The claim that the random embedding approach is critical to success would benefit from proper ablation studies
* A runtime analysis to compare with standard approaches would strengthen the paper.

There is sufficient approval among reviewers and agreement on the benefits to warrant acceptance.
Decision: Accept (poster)