Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence

## Abstract

Abstract We propose a novel approach for learning interchangeable tokens in language models to obtain an extendable vocabulary that can generalize to new tokens. Our method is designed to address alpha-equivalence, the principle that renaming bound variables in a syntactic expression preserves semantics. This property arises in many formal languages such as temporal logics, in which all proposition symbols represent the same concept but are distinguishable from each other. To handle such tokens, we develop a dual-part embedding approach. The first part is shared across all interchangeable tokens, thereby enforcing that they represent the same core concept. The second part is randomly generated for each token, which enables distinguishability. We evaluate our method in a Transformer encoder-decoder model on two tasks: solving linear temporal logic formulae and copying with extendable vocabulary. Our method demonstrates promising generalization capabilities in addition to introducing a favorable inductive bias for alpha-equivalence.

## 1 Introduction

Following the deep learning revolution that affected numerous application areas (Dargan et al., ),
recent developments in the literature demonstrate that deep learning based approaches also perform well in neurosymbolic reasoning tasks, such as theorem proving (Han et al., ) and mathematical reasoning (Rabe et al., ).
The formal reasoning capabilities of deep learning models were questioned up until recently, but Liu et al. () demonstrated the ability of Transformer models (Vaswani et al., ) to learn shortcuts to automata.
Of particular interest is the generalization ability of such models to unseen, out-of-distribution data (Sanh et al., ), which makes them particularly attractive for logical reasoning (Abbe et al., ).

Another application area within formal reasoning is linear-time temporal logic (LTL), which constitutes a framework for reasoning about how logical propositions change over time (Pnueli, ) and is heavily utilized by the formal verification community (Clarke et al., ; Baier and Katoen, ).
Through the use of temporal operators, LTL formulae can specify, for example, that a proposition $p$ must hold at all time steps ($\mathbf{G}p$), or at least one time step ($\mathbf{F}p$).
LTL formulae operate on traces, which describe how the propositions 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 dominated by the methods that use classical algorithms, such as spot (Duret-Lutz et al., ) and aalta (Li et al., ).
However, following the success of Transformer models on end-to-end symbolic integration (Lample and Charton, ), Hahn et al. () attacked the LTL solving problem using the same approach and developed DeepLTL.
The capability of DeepLTL models to generalize beyond the maximum formula length seen during training is especially noteworthy, and it was made possible thanks to tree-positional encoding (Shiv and Quirk, ).

However, generalization to longer formula lengths is not the only concern.
In particular, each LTL formula features a set of atomic propositions (henceforth APs), and it’s desirable 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 distinguishable from each other.
This situation arises in many other application areas, such as mathematical expressions and lambda calculus (alp, ), where renaming the bound variables does not change the meaning.
This phenomenon is described as alpha-equivalence, a concept closely tied to interchangeable tokens.

In this paper, we propose a novel approach for representing 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 a randomized part.
The learnable part is shared across all interchangeable tokens, and the model must depend on the randomized part to differentiate these tokens.
We use the weight tying technique (Press and Wolf, ) to share the same token embeddings with the final projection matrix, which calculates the logits (i.e., next-token probabilities before softmax).

We use our embedding method in a Transformer endocer-decoder model and evaluate it on two tasks: copying with an extendable vocabulary and solving LTL formulae.
For the second task, we use datasets of LTL formula-trace pairs generated by spot (Duret-Lutz et al., ), a library for LTL manipulation and model checking using conventional algorithms.
Overall, our method demonstrates generalization capabilities to larger vocabulary sizes as briefly shown in Figure 1, and also combine well with positional encodings that exhibit length generalization.
Furthermore, we perform experiments with dataset perturbation to demonstrate that our approach introduces a helpful inductive bias for learning alpha-equivalence.

## 2 Related Work

##### Language modeling and formal reasoning

The transformer architecture (Vaswani et al., ), now ubiquitous in modern deep learning, was initially proposed as a generative model to translate between natural languages autoregressively.
This led to many successful attempts to frame formal reasoning tasks as language modeling problems, such as symbolic integration (Lample and Charton, ), symbolic regression (Kamienny et al., ; Vastl et al., ), LTL solving (Hahn et al., ), and many more.
Further developments shifted the field towards large language models (LLMs), e.g.,
by prompting a model pre-trained on a gigantic scale (Frieder et al., ),
by enhancing the prompt with retrieved references for proof generation (Welleck et al., ; Yang et al., ),
by training an LLM on a specialized dataset for mathematics (Azerbayev et al., ).
However, the reasoning abilities of LLMs were questioned by (Tang et al., ), who showed that LLMs struggle with symbolic reasoning when semantics are decoupled, and by others (Wu et al., ).

##### Extensible vocabulary

Efforts to create an extensible vocabulary for neural networks are scarce in the broader machine learning community, let alone the formal reasoning literature.
Morazzoni et al. () exploited dictionary definitions to create extensible word embeddings.
Wei et al. () proposed a vocabulary-extensible sign language recognition framework by using a 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.

## 3 Preliminary: Language models

The autoregressive language modeling or sequence modeling in a broader sense—whose goal is to predict the next token given the past tokens—was revolutionized by the transformer architecture (Vaswani et al., ), 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 cross-attention 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.

## 4 Proposed Method

Figure: Figure 2: Visual structure of the embedding matrix in the proposed method.
Refer to caption: x2.png

To address the problem of learning semantically equivalent but distinguishable (alpha-equivalent) tokens, our method employs two ideas:
sharing some part of the embeddings between such tokens to convey their semantic equivalence;
and assigning a unique randomly-generated vector to the rest of the embedding for each interchangeable token, allowing the model to distinguish between them.
The number of shared and randomly-generated dimensions are denoted by $d_{\alpha}$ and $d_{\beta}$ respectively.
The sum of these two yields the total number of embedding dimensions in the model, denoted by $d_{\text{model}}=d_{\alpha}+d_{\beta}$.
For non-interchangeable tokens, $d_{\alpha}$ dimensions contain separate learnable parameters and $d_{\beta}$ dimensions are set to 0 0.
The structure of the embedding matrix is visualized in Figure 2.

### 4.1 Embedding matrix

##### Construction of the embedding matrix

For a vocabulary with $n$ regular tokens and $m$ interchangeable tokens,
${\bm{L}}\in{\mathbb{R}}^{n\times d_{\alpha}}$ represents the matrix of learnable embeddings for regular tokens,
${\bm{\alpha}}\in{\mathbb{R}}^{1\times d_{\alpha}}$ the shared learnable embedding for interchangeable tokens,
and ${\bm{\beta}}_{i}\in{\mathbb{R}}^{1\times d_{\beta}}$ the randomly-generated embedding for the $i$th interchangeable token where $1\leq i\leq m$.
Note that ${\bm{\alpha}}$ and ${\bm{\beta}}_{i}$ are row vectors.
A zero matrix of size $i\times j$ is represented by $\bm{0}^{i,j}$.
In addition, we define two row-based L2 normalization functions $f_{bn}({\bm{X}})$ and $f_{fn}({\bm{X}})$ that divide each row ${\bm{X}}_{i,:}$ by its L2 norm $||{\bm{X}}_{i,:}||$.
These two functions are identical but can be disabled independently from each other, hence the separation.

Finally, the overall structure of the embedding matrix ${\bm{U}}$ is shown in Equation 1.
In this construction, the interchangeable tokens are assumed to come after the regular tokens.
Note that it’s also possible to support multiple sets of different interchangeable tokens via a trivial extension.

$$ ${\bm{U}}=f_{fn}(\begin{bmatrix}f_{bn}({\bm{L}})&&\bm{0}^{n,d_{\beta}}\\ f_{bn}({\bm{\alpha}})&&f_{bn}({\bm{\beta}}_{1})\\ f_{bn}({\bm{\alpha}})&&f_{bn}({\bm{\beta}}_{2})\\ &\vdots&\\ f_{bn}({\bm{\alpha}})&&f_{bn}({\bm{\beta}}_{m})\\ \end{bmatrix})$ (1) $$

During training, the embedding matrix must be reconstructed in each forward pass with resampled random vectors ${\bm{\beta}}_{1}$ to ${\bm{\beta}}_{m}$.
Resampling ${\bm{\beta}}_{i}$ for $1\leq i\leq m$ during training prevents the model from adapting to the idiosyncracies of a particular random generation and forces it to distinguish between interchangeable tokens regardless of the contents of ${\bm{\beta}}_{i}$.
During inference, it’s created once at the start and remains the same since the autoregressive generation involves multiple forward passes on the same input.

##### Normalization

There are several concerns that warrant the heavy use of normalization while constructing ${\bm{U}}$, as seen in Equation 1.
Firstly, $d_{\alpha}$ dimensions and $d_{\beta}$ dimensions should not overwhelm each other in terms of magnitude.
Normalizing ${\bm{\alpha}}$ and ${\bm{\beta}}_{i}$ separately addresses this issue.
The magnitude of the concatenated embedding is another concern, which is handled by the final normalization.
The normalization of ${\bm{L}}$ is redundant (since the final normalization does the same operation after the concatenation with zeros) but kept in Equation 1 for readability.

### 4.2 Random embedding generation

This section will explain how the distinguishing part of the interchangeable token embeddings, ${\bm{\beta}}_{i},1\leq i\leq m$, are created.
To this end, we developed 3 methods to generate random vectors.
Table 1 provides a summary at a glance.
The first method simply samples the standard normal distribution for each dimension.
The second one uses the neighboring grid points around the origin, which correspond to the 8 directions in 2D.
For each interchangeable token, a 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.

**Table 1: Comparison of random vector generation methods.**
| Method | Normal Distribution | Neighboring Points | Hypercube Vertices |
| --- | --- | --- | --- |
| Formula | ${\textnormal{a}}_{i}\sim\mathcal{N}(0,1)$ | ${\textnormal{a}}_{i}\in\{-1,0,1\}$ | ${\textnormal{a}}_{i}\in\{-1,1\}$ |
|  | $|{\mathbf{a}}_{i}|\neq 0$ |  |  |
| Size for $n$-dims | Continuous | $3^{n}-1$ | $2^{n}$ |
| Sample Visualization |  |  |  |

In the normal distribution method, we don’t have any additional constraints to ensure distinguishability between vectors.
However, in other two methods, we need make sure that each interchangeable token gets assigned to a unique vector since the sampling set is finite.
To achieve this quickly and space-efficiently, we define a mapping from integers to possible vectors.
The unique vectors are generated by sampling $m$ unique random integers (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 of possible vectors.
In the hypercube vertices method, we map the binary digits of an integer in $[0,2^{d_{\beta}})$ to $\{-1,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 $i_{z}=(3^{d_{\beta}}-1)/2$.
Therefore, we define our domain as the integers in $[0,3^{d_{\beta}}-1)$ and add $1$ to the integer $i$ before converting it if $i\geq i_{z}$.

Integer mapping approach for generating unique vectors works well for up to 32 dimensions, 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 size of the sampling set grows exponentially, rendering the probability of drawing the same sample negligible.

### 4.3 Projection

##### Weight tying

In a traditional language modeling setting, since both the embedding and projection matrices are entirely composed of learnable parameters, it’s not necessary to share them, even though there are many advantages of weight tying (Press and Wolf, ).
However, we construct the embedding matrix manually in our method, which makes weight tying a requirement.
Furthermore, since we perform our experiments on an encoder-decoder architecture in this paper, we utilize a three-way weight tying approach, whereby the embedding matrices of encoder and decoder are tied in addition to the final projection matrix.
Three-way weight tying is particularly appropriate for our problem domain since many tokens are shared between the LTL formulae and traces.

##### Feature normalization

Given the output of the last layer before the final projection ${\bm{v}}$ (henceforth called feature vector), instead of directly applying the final projection as in ${\bm{U}}{\bm{v}}$, we apply L2 normalization to the feature vector ${\bm{v}}$ before passing it through the final projection: ${\bm{U}}f_{fn}({\bm{v}})$.
This matrix multiplication constitutes taking a dot product with each row.
Since ${\bm{a}}\cdot{\bm{b}}=|{\bm{a}}||{\bm{b}}|cos(\theta)$ where $\theta$ is the angle between ${\bm{a}}$ and ${\bm{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 in face recognition (Ranjan et al., ; Wang et al., ), it proved sensitive to hyperparameter settings in these losses.
To avoid this problem, we use AdaCos loss function (Zhang et al., ) that scales the logits adaptively throughout training.

To adapt the AdaCos loss function to our use case, we make the following modifications:
Since the language modeling problem involves a sequence length dimension in addition to the batch dimension, we combine these two dimensions 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 log semiring.
Therefore, we clamp the scale value calculated by AdaCos to a maximum of 100 to avoid numerical issues.

## 5 Experiments

##### 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., ) as the positional encoding method in both encoder and decoder unless otherwise noted.
The hyperparameter settings are as follows:

**Table 2: Hyperparameter choices.**
| Experiment | Embedding | Layers | Heads | FC size | Batch Size | Train Steps |
| --- | --- | --- | --- | --- | --- | --- |
| Copy | 64 | 2 | 4 | 64 | 512 | 20K |
| Copy (Big) | 128 | 6 | 8 | 128 | 512 | 20K |
| LTL | 128 | 8 | 8 | 1024 | 768 | 52K |

### 5.1 Copying with Extendable Vocabulary

We introduce a 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.
The string is given to the model as input, and the next-token probabilities predicted by the model are expected to align with the input string exactly.
This embodies a 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 generalize to larger vocabulary sizes unseen during training.
We generate the predictions using greedy sampling in this subsection.

##### Evaluation method

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 a minimum of 3.
Consequently, the total evaluation dataset is arranged in a matrix in which the rows represent unique character count in the string and the columns represent the string length.
This matrix is upper triangular since the unique character count cannot exceed the string length.
For random embeddings, we repeat the evaluation 10 times and report the average.
To evaluate up to the string length of 30 in this setup, $10\times 100\times 406=406000$ predictions are required, where $406$ is the number of upper triangular elements in a $28\times 28$ matrix.
To minimize the impact of random factors, we train each model three times and report the results only for the best.

#### 5.1.1 Generalization to larger vocabularies

We create a dataset consisting of 10 million strings whose lengths vary between 3 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.e., no error (Figure 3, left).
The worst model’s average edit distance is 1.0.
For comparison, an output sequence of length 30 can have a maximum edit distance of 30.

#### 5.1.2 Generalization to larger vocabularies and lengths

We create a dataset consisting of 10 million strings whose lengths vary between 5 and 10 with at most 5 unique characters.
We evaluate on the same validation set as before, expecting the model to generalize to both longer lengths and larger vocabulary sizes.

##### Comparison

We train multiple models that use different random embedding methods (Section 4.2) with different $d_{\beta}$ values.
While altering $d_{\beta}$, we keep the total number of embedding dimensions $d_{\alpha}+d_{\beta}$ constant.
We train two kinds of baseline models with fixed embeddings: the first one on the same dataset, and second one on a dataset with the same parameters but using a vocabulary size of 30.
We use two baselines because the first type of baseline cannot even take strings with larger vocabularies as input.
We train each model at least 3 times with different seeds and report the results for the best one in Table 3.

**Table 3: Mean edit distance for various models. The numbers in the header row represents $d_{\beta}$ for each random embedding method. In the first column, enabled normalization features are listed. AC refers to AdaCos, which can only be enabled when $f_{fn}$ is used. The last row represents the baseline models trained on a vocabulary size (VS) of 30.**
| Enabled | Normal Distribution | Neighboring Points | Hypercube Vertices | Baseline |  |  |  |  |  |  |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| Features | 2 | 4 | 8 | 16 | 32 | 4 | 6 | 8 | 16 | 32 | 5 | 6 | 8 | 16 | 32 | VS=30 |
| $f_{bn}$ + $f_{fn}$ + 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 | 6.1 |
| $f_{fn}$ + 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 | 6.1 |
| $f_{bn}$ + $f_{fn}$ | 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 | 4.9 |
| $f_{fn}$ | 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 | 4.9 |
| $f_{bn}$ | 10.6 | 16.6 | 11.8 | 6.9 | 8.2 | 5.8 | 3.0 | 0.6 | 7.8 | 14.3 | 12.8 | 13.8 | 19.4 | 22.9 | 11.6 | 5.5 |
| - | 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 | 5.5 |

The results in Table 3 exhibit high variance with no clear patterns that indicate which methods are better.
Therefore, we perform an analysis based on 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 Boolean properties (such as $f_{bn}$, $f_{fn}$ and AdaCos) are 0 or 1.
The correlation coefficients are as follows:

| N.D. | N.P. | H.V. | $d_{\beta}$ | $f_{bn}$ | $f_{fn}$ | AdaCos |
| --- | --- | --- | --- | --- | --- | --- |
| 0.02 | -0.14 | 0.11 | 0.01 | 0.10 | -0.29 | -0.41 |

First three columns are the random embedding methods as listed in Table 1, the fourth column is $d_{\beta}$, 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_{\beta}$ is negligible.
Introducing $f_{bn}$ increases the edit distance, but the statistical significance is not ideal (p-value 0.04).
Both $f_{fn}$ and AdaCos loss have a positive and statistically significant impact on edit distance, with p-values smaller than $10^{-6}$.

We determine the best model for the proposed method and the baseline on this validation set, evaluate them on the test set and visualize the results in figure 3.
Since the baseline model cannot process larger vocabularies, we assume that the prediction is 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 H.V. $d_{\beta}=6$ with $f_{fn}$ + AdaCos, and achieves a mean edit distance of 0.38 on the test set.
The first baseline’s mean edit distance is 0.51 (calculated up to 5 unique characters, only for this model), and the second baseline’s mean edit distance is 4.93.

Figure: Figure 3: Edit distance heatmaps on test set. The leftmost one is the proposed model trained on strings up to length 30 and vocabulary size 5, which achieves a perfect result (mean edit distance = 0). The center-left and center-right are the proposed and baseline models respectively, trained on the same vocabulary size with a limited length of 10. The rightmost model is the second baseline trained with an increased vocabulary size of 30. The lower triangular part of each heatmap (hatched gray) represents the impossible combinations of length and unique character count, and the green box is the boundaries of the training dataset.
Refer to caption: extracted/5946621/figures/cpy-heat/quadruple.png

#### 5.1.3 Sensitivity to randomness in embeddings

We analyze the impact of 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 of the second model in figure 3 are 0.25, 0.38, 0.55 respectively, with a sample standard deviation of 0.09.
The pooled standard deviation of 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 the next experiments, 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 a 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.

#### 5.1.4 Scaling up

We increase the length of the strings from 5-10 to 20-80, and vocabulary size from 5 to 20.
The hyperparameters are as in the “Copy (Big)” row of Table 2.
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 is 0.0.
The heatmap is given in Figure 1.
Both baselines also attain perfect performance in this task on their training vocabulary sizes.

### 5.2 LTL Solving

In this section, we train models on the LTLRandom35 dataset from DeepLTL (Hahn et al., ) and other synthetic datasets created with the same method.
To evaluate the correctness of the generated formulae, we utilize spot framework version 2.11.6 (Duret-Lutz et al., ).
We use tree-positional encoding (Shiv and Quirk, ) in the encoder and RoPE (Su et al., ) in the decoder.
We generate predictions using beam search with a beam size of 3 in this section.

#### 5.2.1 Dataset Perturbations

To demonstrate that our method creates a helpful inductive bias, we created a perturbed version of the LTLRandom35 dataset.
In particular, we rename the APs such that the order of the first AP appearances in the trace is always the same.
Our method is naturally immune to these alterations because of the randomness we introduce in embedding matrix.
We provide an empirical proof in Table 4.
We train our method only on the perturbed dataset since training it again on the normal dataset amounts to training with different random samples.

**Table 4: Evaluation of the baseline and our method trained on different versions of the LTLRandom35 dataset. First two columns denote the model and the training dataset. Next column indicates the ratio of the correct predictions as evaluated by spot, followed by the ratio of exact matches. Last three columns display alpha-robustness values for varying atomic proposition (AP) counts. Results indicate that our method induces a robust inductive bias for alpha-equivalence.**
| Training |  | Evaluation | Alpha-Covariance |  |  |  |
| --- | --- | --- | --- | --- | --- | --- |
| Dataset | Model | Correct | Exact | 3 AP | 4 AP | 5 AP |
| Normal | Baseline | 97.96% | 83.52% | 97.24% | 95.86% | 91.84% |
| Perturbed | Baseline | 34.10% | 11.88% | 62.72% | 58.17% | 37.22% |
| Perturbed | Proposed | 95.85% | 76.78% | 98.71% | 97.95% | 97.63% |
| Limited | Baseline | 87.58% | 64.06% | 93.56% | 89.81% | 82.73% |
| Limited | Proposed | 87.62% | 59.81% | 97.05% | 95.57% | 92.57% |

While the original model performs significantly worse under perturbation,
the new model matches the baseline performance in terms of correctness ratio despite perturbation.
This observation suggests that our modification introduced a robust inductive bias that makes the model 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.

Table 4 also contains evaluations of the baseline and the new model trained with a severely limited number of samples: 80,000 instead of 799,909.
Although both models perform similarly under this setting, they react differently to alpha-equivalent variations of the same input-output pairs, which we will discuss next.

#### 5.2.2 Alpha-Covariance

Given a vocabulary of size $n$ and an LTL formula and trace pair containing $k$ APs, it’s possible to write ${}^{n}\!P_{k}=n!/(n-k)!$ alpha-equivalent pairs by changing the order of the APs.
Creating an alpha-equivalent permutation like this is termed alpha-conversion.
Since all such pairs are semantically equivalent, we expect the model’s predictions to be the same after undoing the alpha-conversions for all of them.

To quantify this, we develop a metric called alpha-covariance, which measures the model’s covariance to various alpha-conversions of the same input-output pair.
Let $({\bm{x}},{\bm{y}})$ be an input-output pair for the model, and let ${\mathbb{P}}=\{({\bm{x}}^{1},{\bm{y}}^{1}),\ldots,({\bm{x}}^{n},{\bm{y}}^{n})\}$ be $n$ input-output pairs alpha-equivalent to $({\bm{x}},{\bm{y}})$.
We define $\alpha_{i}$ as the alpha-conversion function for the $i$th input-output pair such that $\alpha_{i}({\bm{x}})={\bm{x}}^{i}$ and $\alpha_{i}({\bm{y}})={\bm{y}}^{i}$.
To compute the alpha-covariance of a model with respect to ${\mathbb{P}}$, we generate predictions for each input in ${\mathbb{P}}$,
obtaining the prediction $\hat{{\bm{y}}}^{i}$ for each $x^{i}$.
We define a set that contains the predictions with alpha-conversion undone: ${\mathbb{U}}=\{\alpha_{i}^{-1}(\hat{{\bm{y}}}^{i})\mid 1\leq i\leq n\}$.
Note that if we defined this set for the ground truth outputs in ${\mathbb{P}}$, we would get $\{{\bm{y}}\}$ since $\alpha_{i}^{-1}({\bm{y}}^{i})={\bm{y}}$ holds for each ${\bm{y}}^{i}$ by definition.
The alpha-covariance of this model with respect to ${\mathbb{P}}$ is given by Equation 2.

$$ $1-\frac{|{\mathbb{U}}|-1}{n-1}$ (2) $$

Intuitively, when alpha-covariance is $1$, the model is unaffected by all alpha-conversions in ${\mathbb{P}}$.
An alpha-covariance of 0 0 indicates that $|{\mathbb{U}}|=n$, i.e., the model’s prediction for each alpha-equivalent pair is unique after undoing the alpha-conversion.
This is unwanted because alpha-conversions should not change the semantic meaning.
Thanks to the embedding randomization in our method, an alpha-conversion does not necessarily change the embeddings, and conversely, there are multiple ways to embed the same input due to randomness.

To compute alpha-covariance for a given vocabulary size, we generate all alpha-equivalent input-output pairs and get the model’s predictions for all of them.
We report the results in Table 4, which demonstrates that our method has a positive impact on the alpha-covariance, especially in limited data settings.
Since the LTLRandom35 dataset was created synthetically, it doesn’t have any noteworthy biases and even the baseline enjoys a high alpha-covariance thanks to this.
However, when the dataset is perturbed by introducing a bias to the order of APs, the baseline struggles heavily with alpha-covariance, whereas our method does not.

#### 5.2.3 Generalization

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 H.V., $d_{\alpha}=5$) and the two baselines that use fixed embeddings in figure 4.
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.

Figure: Figure 4: Heatmap visualizing the ratio of correct predictions on a special test set. The brightness of the color depends on the sample size, with full brightness representing 100 samples. The dashed white box 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 5 APs.
Refer to caption: extracted/5946621/figures/ltl-heatmap.png

The generalization to larger AP counts is important especially when considering the exponential growth of the dataset generation time.
In Figure 5, 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 a system with 56 threads.

Figure: Figure 5: Scaling behavior of the trace generation using spot.
Refer to caption: extracted/5946621/figures/tracegenscaling.png

## 6 Conclusion

The primary difference between machine learning and numerical optimization is the intention to generalize to out-of-distribution samples, for which the network architecture and its inductive biases play a vital role.
In this work, we addressed the challenge of generalizing to larger vocabulary sizes unseen during training and creating an inductive bias for alpha-equivalence.
We also contributed the alpha-covariance metric for measuring the model’s consistency against alpha-equivalent inputs.
These contributions embody a foundation for learning extensible vocabularies for interchangeable tokens, which is especially useful for formal reasoning tasks in which alpha-equivalence naturally arises.
Although our dual-part embedding method demonstrates generalization capabilities, its performance in the LTL solving task decreases slightly in in-distribution data (Table 4).
The future work can also tackle this issue, which may eventually lead to Pareto improvements in bias-variance tradeoff.
Finally, new randomization and/or normalization methods can be explored.

## Appendix A Appendix

### A.1 Temporal logic overview

Linear Temporal Logic (LTL) extends propositional logic by introducing the ability to reason about the evolution of propositions over time [Pnueli, ].
The syntax of LTL, defined over a finite set of atomic propositions $P$, is as follows:
The syntax of LTL, defined over a finite set of atomic propositions $P$, is given in Equation 3,
where $\mathbf{T}$ represents True, $p\in P$ an atomic proposition, $\neg$ the negation operator, $\wedge$ the conjunction operator,
$\mathbf{X}$ and $\mathbf{U}$ the temporal operators next and until respectively.

$$ $\phi:=\mathbf{T}\mid p\mid\neg\phi\mid\phi_{1}\wedge\phi_{2}\mid\mathbf{X}\phi \mid\phi_{1}\mathbf{U}\phi_{2}$ (3) $$

Specifically:

- •
$\mathbf{X}\phi$ holds at time $t$ if and only if $\phi$ holds at the next time step, i.e., at time $t+1$.
- •
$\phi_{1}\mathbf{U}\phi_{2}$ means that $\phi_{2}$ must hold at some future time $t_{2}$, and $\phi_{1}$ holds at every time step $t$ from the current time $t_{1}$ up to but not necessarily including $t_{2}$.

For instance, the formula $\mathbf{X}\mathbf{X}a$ specifies that $a$ must hold at the third time step. Similarly, the formula $\mathbf{T}\mathbf{U}a$ requires that $a$ holds at some point in the future.
Finally, as a more complex example, the formula $\mathbf{X}b\wedge a\mathbf{U}c$ asserts that $b$ holds at the second time step, $c$ holds at some future time, and $a$ holds at all preceding time steps.

An LTL formula is evaluated over a trace, which represents a sequence of truth values for atomic propositions over time.
In this work, as in DeepLTL [Hahn et al., ], we consider symbolic traces of infinite length.
These traces are expressed in what is known as a lasso form, denoted $uv^{\omega}$, where $u$ is a finite prefix, and $v$ is a finite sequence that repeats indefinitely.

A symbolic trace represents all traces that satisfy the propositional formulae at the respective time steps. For example, the symbolic trace $a,a\wedge\neg b,(c)^{\omega}$ describes all traces in which $a$ holds at the first two time steps, $b$ does not hold at the second time step, and $c$ holds at every step from the third onward.
This symbolic trace satisfies the formulae $\mathbf{T}\mathbf{U}c$ and $\mathbf{X}\neg b\wedge a\mathbf{U}c$, but it violates the formula $\mathbf{X}\mathbf{X}b$ since $b$ is not guaranteed to hold at the third time step.
Symbolic traces, such as 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 $uv^{\omega}$ that satisfies a given input formula $\phi$.
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 in the trace.

For compatibility with the dataset from DeepLTL [Hahn et al., ], both our traces and formulae are represented in Polish (prefix) notation, where operators precede their operands. For instance, $a\wedge 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 $uv^{\omega}$. 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\wedge b,(b)^{\omega}$.

## Peer Reviews

confidence: 3
contribution: 2
initial_rating: 3
presentation: 1
questions: - How significant are the empirical results (please see under weaknesses for details)
- Are there any real-world cases that could be evaluated for showing the value of the alpha-equivalence and the significance of the proposed methods as well as limitations or trade-offs.
soundness: 2
strengths: - Generalizing representations to new tokens to represent the alpha equivalence seems like a relevant and significant problem in the domain of LTL
- The method seems to be intuitive and scalable as shown by the experiments
summary: The paper presents an approach to create embeddings for LTL (Linear-time Temporal Logic). The main challenge that is addressed is to represent tokens during inference that are not seen during training. The idea is to represent interchangeable tokens during inference instead of learning the representations during training. A part of the embedding is used to represent the similarities and tie tokens together and a second randomized part distinguishes between interchangeable tokens. Experiments are performed with large vocabularies showing that the proposed approach can learn representations for interchangeable tokens more accurately.
weaknesses: - Most of the contribution is based on empirical results, since the novelty of the algorithmic contribution itself is perhaps not as strong (e.g. generating the random embeddings). Given this, it felt like the experiments were not particularly strong and also presented in a way that is a little hard to follow. Specifically, the first experiment is synthetically designed with random strings. Further, it is not compared to any other method but only on variants of the same approach, so it is hard to judge whether the results are significant or not. The second dataset seems like an existing benchmark and it is not clear what the “baseline” is in the case. Also, there is a perturbed and limited dataset which again is not very clear as to what is the difference is between the two. Regarding the metric, it seems to introduce a new metric, but there is very little context to justify the metric, for e.g. are there other types of metrics, what are the trade-offs etc. In general, there should a bit more discussion on this.
- Regarding the method itself, the randomization may introduce a lot of variance, so how would this variance be accounted for in the results presented? 
- I was not sure what N.D., H.V. ,etc. were showing in one of the tables
- The presentation could be improved with some examples and real-world motivation of LTL and relating them with the empirical results

---

confidence: 5
contribution: 2
initial_rating: 3
presentation: 3
questions: Please see the "weaknesses" section above -- I would be particular interested in hearing the authors response to comparisons against alternative approaches such as DeBruin indices or alpha-renaming-as-part-of-training.
soundness: 2
strengths: The issue of alpha-equivalence, and of extensible vocabularies in general, has been underexplored in the literature, and the author's proposed solution seems principled and well-designed.  The authors describe their technique clearly, and cite the relevant literature.

Experimentally, the most interesting results of the paper by far are the generalization results.  The authors proposed solution generalizes to longer sequences and longer vocabulary in the synthetic copying task, and to longer formulae using more variables for the LTL task, whereas the baselines do not.  IMO, these generalization results are important.
summary: Most formal languages, including the lambda calculus, include bound variables, e.g. the variable $X$ in $\forall$ X. human($X$) $\implies$  mammal($X$).  Terms in such languages are held to be equivalent under renaming of bound variables, a principle known as alpha-equivalence.  E.g. we can rename $X$ to $Y$ in the above expression without changing its meaning.  However, even though the actual name does not matter, an LLM which does logical reasoning must still be able to distinguish between different names, e.g. the variables $X$ and $Y$ refer to distinct entities in $\forall X,Y$. parent_of($X$, $Y$) $\implies$ child_of($Y$, $X$).  

The authors propose a novel embedding scheme for handling variables that are subject to alpha-renaming.  For each such variable, one part of the embedding is a normal learned embedding meaning "variable", while the second part is randomly generated for each training example, but is consistent across all uses of that variable within the example.  I.e. the embedding of $X$ is partially random, but all occurrences of $X$ within the training example use the same embedding for $X$.

The authors test their scheme on a synthetic copying task, and on a synthetic LTL (temporal logic) task involving randomly generated formulae.
weaknesses: Unfortunately, most of the authors experiments were not very convincing to me.  The copying task is essentially a unit test; it merely shows that the embeddings are working as intended.  The LTL perturbation task deliberately trains the baseline model in such a way that it is forced to operate out-of-distribution, so there's no surprise that the baseline does poorly.
Some of the other tests, such as different randomization schemes, seem uninteresting and/or irrelevant to me. 

Most importantly, both of the main tasks were entirely synthetic, which means that the variable names had no actual meaning.  In real-world human-written code or logical proofs, names typically do have meaning.  Meaningful names are a double-edged sword.  On the one hand, they may prevent the model from recognizing certain equivalences.  On the other hand, they can also guide the model in reasoning about the proof or code; a variable named "grocery_list", for example, encodes a lot of information about how that variable is likely to be used.  Names are certainly crucial for human reasoning; typical code-obfuscation techniques work by renaming all the variables, which prevents humans from understanding the code.  

To really demonstrate that the author's technique is effective in practice, I would want to see it evaluated on something other than a toy synthetic dataset, such as a code-repair task for actual human-written code.  Unfortunately, the authors do not even bother writing a discussion section about the pros & cons of erasing names from LLM input; the paper would be stronger if it at least had that.

In the short term, a way to improve the paper would be to compare the technique against other alternatives.  For example, DeBruijn indices are another common way of encoding formulae, which eliminate the need for alpha-renaming.

Another potential comparison would be to use a conventional subword vocabulary for variable names, but to train the baseline model on formulae that have already undergone random alpha-renaming of variables, so that the baseline model is robust against renaming -- that would be a more interesting result than the contrived perturbation experiment in this paper.  

Although it would require training a larger model, a good way to show the importance of alpha-equivalence in practice would be to train a conventional model on human-written proofs or code, and then show that the conventional model can be forced to make unsound logical deductions if the variables are renamed.  

Overall, I would say that this is promising work, but publication at this point is perhaps premature.

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 3
questions: Please address the comments above.
soundness: 3
strengths: The dual-part embedding approach is thoughtfully designed. It enforces shared semantics with a learnable component while introducing a random vector for differentiation. This elegantly handles alpha-equivalence, enabling the model to generalize across renamed and unseen variables.

The relevance of their work is understated, as this approach can potentially improve many neuro-symbolic systems. Alpha-equivalence/bounded variables are a core concept of formal languages. This approach can easily transfer to all neuro-symbolic tasks that combine formal languages and language models.

The paper’s structure is clear; the reader is well-guided through the method and experiments. The experiments are thorough and include an extensive ablation study. The trace copying and generation tasks clearly show the effectiveness of this approach.
summary: The paper proposes a novel embedding strategy for language models, specifically addressing the challenge of alpha-equivalence in formal languages. The authors introduce a dual-part embedding that combines a learned embedding that is shared between all alpha-equivalent tokens with a random component. The random component allows distinction between different variables without tying the variable symbol to the embedding. This creates an embedding technique that is agnostic to the naming of variables and enables the model to generalize to more (alpha-equivalent) variables easily. The authors evaluate on a toy task (trace copying) to empirically show the effectiveness of their approach. A second evaluation is performed on the trace generation task (from LTL specifications) to show its applicability in more complex tasks. Their results show that such an embedding indeed makes the model robust to renaming and shows the ability to handle more atomic propositions without additional training data.
weaknesses: While the experiments are extensive, it would help if the paper clarified the specific contributions of each experiment to the overall findings. The following is more detailed and specific feedback on the individual experiments.

__Baseline__. All experiments (Table 4, Figure 1, and Figure 4) mention a baseline approach. The authors should clarify how this baseline is created and how it relates to related work (Hahn et al.). I assume the authors replicated experiments from Hahn et al., but it would be beneficial if the authors would clarify where and how the replication's performance compares to the related work.

__Training Steps__. The authors do not provide the training time, hardware, number of epochs/steps, etc., for any of the experiments and baselines. Comparing the training epochs/steps of their approach to the baseline would be especially important to assess the effectiveness of their approach.

__Hyperparameter Search__.The ablation study on hyperparameter choices (5.1.2) shows thoroughness and dedication. However, the authors themselves note that the results (Table 4) are inconclusive on which hyperparameter choice is the best because of the high variance. They then extensively cross-test the correlation coefficient to see which hyperparameter choices have a positive effect. Contrary to the findings of these extensive experiments, the authors fall back to Table 4 to declare their best model (which partly contradicts the correlation coefficients). Despite the extensive experiments, this feels inconclusive and inconsistent. To improve clarity, it might be beneficial to move the ablation details to the appendix and present the “best” model configuration in the main text, leaving more space to highlight the generalization to additional APs on the trace copying task.

__Immunity to Renaming__. The phrase “empirical proof” (line 398) is misleading since empirical experiments provide evidence rather than proof. Additionally, if understood correctly, the embedding of a variable/token does not depend on the actual variable symbol/token. Therefore, for example, the model cannot distinguish whether a variable is named a or b, only that they are different. This means that the model is - by construction - immune to variable renaming. If the model is - by construction - immune to variable renaming (during training and evaluation), there is no necessity to empirically validate this property. On the contrary, the Alpha-Covariance results on the “Limited” experiment (proposed model) seem to invalidate this property as the Alpha-Covariance seems to degrade with more AP. Can the authors comment on this observation? 

Instead, focusing on other non-obvious generalization aspects would further strengthen the experimental section:

__AP Generalization__. The most important experiment is the generalization to more APs (5.1.2 and 5.2.3). The paper's main contribution is showing that the proposed embedding improves generalization to more APs, especially on a non-trivial task (5.2.3). However, the comparison with the baseline model might be biased. While it does show that the proposed model generalizes, they don’t fully establish that the baseline model can’t generalize in this way. The experiment instead shows that Transformers cannot generalize to unseen tokens, which is a well-known fact. A more balanced comparison could involve ensuring that all 30 (or 10) APs appear in the baseline’s training set. Note that this does not imply that the dataset would contain samples exceeding 5 APs, only that all tokens are seen during training. Since the authors admit that the baseline model performs better on in-distribution evaluation, the outcome of such an experiment is open. 

__Minor Details__:
 - Adding axis legends for edit distance in the heatmaps (Figures 1, 3, 4) and labeling subfigures (e.g., a), b), c)) would improve understanding and make the experiments easier to reference. Placing Figure 1 in the evaluation section, where it has more context, might also enhance the flow as the Figure is hard to understand without the necessary context of the evaluation section.
 - The grey area in Figure 3 represents impossible data points, and the green box (boundaries of the training dataset) overlaps this region. If these data points cannot exist, perhaps the green box boundaries could be adjusted to prevent visual confusion.

__Summary__. Overall, this paper introduces a well-motivated and potentially impactful approach, and it’s clear that substantial engineering effort went into the experiments. However, the experiments do not sufficiently showcase the advantage over the baseline. This does not imply that the results are not good enough but rather that comparisons to the baselines need to be chosen more carefully. Furthermore, a second application from a different formal language domain than LTL would strongly improve the paper’s relevance in the area.

---

confidence: 3
contribution: 1
initial_rating: 3
presentation: 1
questions: - Formally state the problem in the paper and provide useful examples to illustrate the problem and the intended use cases.

In Sec. 4. the authors refer to the addressed problem as “learning semantically equivalent but distinguishable (alpha-equivalent) token”. However, this problem is actually not precisely defined elsewhere. As we said before, the usual concept of alpha-conversion does not seem to apply for the intended applications foreseen in the paper.

- Justify and explain the need for partitioning the set of tokens.

In Sec. 4.1. the paper presents an embedding matrix where tokens are partitioned into so-called “regular” or “not-interchangeable”, and “interchangeable” ones. The notion of regular token is only used in this section. For the experiments in Sec. 5.1. all tokens are considered interchangeable. No mention at all of any partition of tokens in the case of LTL, though it seems there is none.

- Clarify whether the embedding has the size of the largest expected vocabulary.

The experiments in Sec. 5. (summarized in Table 3) talk about d_beta which is the number of columns of the embedding for the randomly generated part, but there is no specification of the numbers n and m corresponding to the number of regular and interchangeable tokens. The description of the experiments talk about “unique characters” but it is not clear whether they are randomly generated or fixed, or if the training and evaluation sets of characters intersect or not.

The text in L. 275 “next-token predicted probabilities … are expected to align with the input string exactly” is misleading. What do you mean by “align”. In the description of the experiments in Sec. 5.1. it looks like the number of rows of the embedding is the size of the largest expected vocabulary V’, while the transformer is only trained on symbols from V. This is not clearly stated before.

- Justify the evaluation metric in Sec. 5.1.

The evaluation metric “edit distance” is not justified. Since the validation strings are randomly generated and all tokens are interchangeable, while a token different from the one in the validation string would be considered an edit error? Also, I found Figure 3 (as well as Fig. 1 in the introduction) difficult to understand.

- Clarify questions on the perturbed dataset and baseline model of Sec. 5.2.

The experiments on LTL satisfiability are not clear (Sec. 5.2.1, Table 4). 

First, the way the perturbation of the dataset is carried out is very roughly described. Do you rename both input formulas and output traces? Renaming cannot be just random since you have to preserve satisfiability and the validity of the output. Please explain.

Also, I don’t understand why fixing the order of the first occurrence is useful. Please clarify .

The text suggests it is not a model trained by the authors for the purpose of this paper. So, first of all: where does it come from? is it a model publicly available? Also, how is it capable of dealing with propositions which are not in the original set of AP? Or, are you considering the same set of AP? 

The experiments in 5.2.1 and 5.2.3. do not seem to partition the tokens into regular and interchangeable. Please clarify.

- Clarify questions about alpha-covariance.

Sec. 5.2.2. Pg. 9. L 445-450 seems to suggest that there is some relation between the alpha-covariance metric and semantic correctness. It is not clear to me that the experiments in Table 4 evidence that. Please clarify.

Other questions and comments

Pg. 1. Starting Section 1 with a figure is distracting. Also, it is not related at all with the introduction and hard to understand. I think those figures do not help to clarify what is going on.

Pg. 1. The introduction gives the impression that there is no other path to solving the stated problem of satisfiability of LTL modulo alpha-conversion with Transformers than the one proposed by the paper. For instance, it could be possible to just apply a renaming to the Transformer’s alphabet before-hand. Please comment on this.

Pg. 2. endocer -> encoder

Pg. 4. Line 167. Why is it trivial to support multiple sets of different interchangeable tokens and what would be the need for such kind of embedding? Please clarify.

Pg. 5. Line 254. What do you mean by log smearing?

Pg. 5. Line 255. “clamp the scale value..”. I think bound/clip would be preferable.

Pg. 7. Line 324. Why f_bn, f_fn and AdaCos are boolean properties?

Pg. 8. Line 396. I think “empirical evidence” is more appropriate than “empirical proof”.
soundness: 1
strengths: The main strength of the paper is to put the eye on a problem scarcely studied, namely how could language models be effectively used in vocabularies different from the one they were trained with.
summary: The subject of the paper is studying a method for using transformers trained to solve a task T on vocabulary V in order to solve the same task on a vocabulary V’ different from V (possibly of larger cardinality).
weaknesses: The main argument put forward by the authors is that this is needed for dealing with linear temporal logic (LTL) satisfiability where a transformer is trained to output traces that satisfy the formula given as input (the empty trace meaning the formula is not satisfiable). The argument here is that unknown propositional symbols out of vocabulary V used to trained the transformer can be used in formulas at prediction time. The other “abstract” application mentioned is copying with an extendable vocabulary. However, this problem is not related to any concrete one that actually requires handling an a priori unknown vocabulary.

The rationale behind the first application is that propositional symbols not in V could actually be replaced by  others in V without changing satisfiability. This is called interchangeability in the paper. However, this concept is not formally defined but loosely presented in the introduction. Moreover, the paper states that is the same as alpha-conversion. This statement is at least cumbersome since alpha-conversion applies in the case of bound variables, but there are no quantifiers in LTL, nor in the extendable vocabulary case. For LTL, it seems to be renaming under some constraints, but not alpha-conversion. For the second application, it is not even clear where renaming occurs. 

The introduction suggests that the vocabulary V' used at evaluation time is unknown at training time. However, the experiments make clear that the method requires fixing the size of the expected vocabulary at training time as well as the translation from input symbols to tokens. This is never explicitly said in the paper. 

Overall:
- The paper lacks a precise definition and formalization of the problem it intends to solve.
- The experiments are not sufficiently well presented and analyzed.

Meta-review: The authors propose a method for creating embeddings for linear-time temporal logics (LTL) where a challenge is that tokens that were not encountered during training may need to be used during inference. The authors propose interchangeable tokens where some part represents similarities between such interchangeable tokens and a second random part which uniquely identifies them. There is very little theory in the paper and the reviewers agree that substantial more empirical evaluation is necessary.

Decision: Reject