Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence

We thank the reviewer for their thorough analysis. We understand if our paper was difficult to follow due to the lack of a formal problem definition. We have addressed this in the revised version.

We admit that our usage of the term “alpha-conversion” is somewhat unconventional in the LTL context since there are no bound variables. However, we preferred this term because the underlying principle (renaming variables does not alter meaning) is essentially the same. Although there are no bound variables in LTL, for a given formula-trace pair, the atomic propositions (APs) can be considered “bound” to the pair. Because renaming an AP in both the formula and the trace (provided that there is no name collision) retains the same relationship between them.

...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.

We now briefly clarify this topic in the newly added problem definition text. In principle, the proposed approach does not impose any restrictions about the size of the expected vocabulary. However, in practice, the maximum vocabulary size changes as a function of the number of embedding dimensions. Therefore, the expected size of the largest vocabulary needs to be considered (coarsely) while setting the hyperparameters.

The experiments in Sec. 5. (summarized in Table 3) ..., but there is no specification of the numbers n and m corresponding to the number of regular and interchangeable tokens.

Since all tokens are interchangeable in the copy task, the number of unique characters is equal to the number of interchangeable tokens. The text specifies the number of unique characters for these experiments.

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.

For each dataset, the set of unique characters is fixed. The strings are randomly generated from this set. We could not understand the comment regarding randomly generating the set of unique characters. We will be happy to clarify, if needed, if the reviewer can elaborate their concern.

The training vocabulary is a subset of the evaluation vocabulary, as explained in the new problem definition. However, the particular characters are not important for the proposed method, e.g., the set of interchangeable tokens could be changed from {a, b, c} to {d, e, f} but this wouldn’t necessarily affect the embeddings (apart from the effects of randomness).

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 model’s predicted probability distribution for the token at the $i$th position, the character at the $i$th position in the input sequence must have the highest probability. We have rewritten this sentence as follows for clarity: “A string is given as input, and the model is expected to produce the input string exactly via autoregressive generation.” Since we use greedy sampling in this section, these statements are equivalent.

The evaluation metric “edit distance” is not justified.

Two tokens are considered interchangeable if swapping them with each other in both the input and the output results in a semantically equivalent input-output pair. For example, suppose that the input string is “abc” in the copying task. The output is also expected to be “abc”. Since all tokens are interchangeable in this task, the input-output pair (“abc”, “abc”) is considered to be “alpha-equivalent” to (“def”, “def”), or any other pair that contains a string with three unique letters. (Note that none of the letters have any special meaning for the purpose of copying; they just need to be replicated as-is.) However, if the model outputs “def” in response to “abc”, this is considered incorrect, because both the input and the output must be transformed in the same way for alpha-equivalence. We hope that this explanation clarifies the justification of using the edit distance as an evaluation metric.

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.

Yes, in each input-output pair, APs in both the formula and the trace are renamed in the same way. This applies to all “alpha-conversions” in the paper. This ensures that the transformed pair is still a valid sample, even if the renaming is random. Note that the names of the APs are arbitrary. As long as the renaming does not introduce any name collisions, it cannot break the validity of the sample.

I don’t understand why fixing the order of the first occurrence is useful.

Fixing the order of the first occurrence introduces a perturbation into the dataset. After training the models on this dataset, we evaluate them on unperturbed samples, which are now out-of-distribution for the models. Since the baseline model overfits to the idiosyncrasies of the perturbed training dataset, its performance plummets on unperturbed samples. However, due to the construction of our embeddings, our model maintains the same performance as if it were trained on unperturbed samples, thereby demonstrating that our method introduces a robust inductive bias.

The text suggests it is not a model trained by the authors for the purpose of this paper. ... is it a model publicly available? Also, how is it capable of dealing with propositions which are not in the original set of AP?

We trained all baseline models from scratch for the purposes of this paper. To explain this, we added a paragraph after the first paragraph in the “LTL Solving” subsection.

The set of APs in the alpha-covariance experiment remains the same in training and evaluation because vocabulary generalization is not the focus of that experiment.

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

The example in the newly added problem definition section demonstrates how the tokens are partitioned in the LTL solving task.

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.

It was not our intention to make this suggestion. The referenced paragraph does not mention “semantic correctness”. Perhaps there is some confusion here, we will be happy to address any misunderstandings if the reviewer could explain the source of this impression.

The paragraph claims that if renaming APs in the input leads to a different output (in the sense that the output is still different after undoing the renaming), then this is an unwanted behavior. Because the semantic meaning of the output should not change depending on how the APs in the input are named, as the names are arbitrary.

Starting Section 1 with a figure is distracting.

We moved this figure to the experiment section where it has more relevance.

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.

We did not make this claim. Could you please specify which part of the text gave this impression?

For instance, it could be possible to just apply a renaming to the Transformer’s alphabet before-hand.

We are not sure about what this suggestion means. But we added a new baseline that uses alpha-renaming as data augmentation during training, which may be what the reviewer was referring to. Otherwise, please clarify.

Why is it trivial to support multiple sets of different interchangeable tokens and what would be the need for such kind of embedding?

We hope that the new problem definition section makes it easier to see why this is trivial: Instead of having a single $\mathbb{V}_i$ set, we would have multiple disjoint sets of interchangeable tokens. Each of these sets would have a different shared embedding part. Although this change is straightforward to implement, it was not our intention to claim that training such a model may not pose any unforeseen challenges. To clarify our position, we replaced the word “support” with “implement”.

Here’s an example demonstrating when multiple sets of interchangeable tokens could be helpful: In a programming language, both constants and variables can be renamed, but there are subtle differences between these two concepts (e.g., the value of a constant cannot be altered). Thus, there can be two sets of interchangeable tokens: one for constants, and the other one for variables.

What do you mean by log smearing?

Log semiring refers to the practice of performing operations in the logarithmic domain for better numerical stability. For example, multiplication is equivalent to addition in the logarithmic domain. However, in this part of the text, the particular application we were referring to is better known as the log-sum-exp trick, which is not strictly limited to log semiring despite being an application of it. To improve clarity, we replaced “log semiring” with “log-sum-exp trick”.

Why f_bn, f_fn and AdaCos are boolean properties?

These properties denote whether the corresponding normalization or loss function is enabled. This is mentioned in the caption of the hyperparameter search table (Table 3 in the original manuscript and Table 4 in the revision).

We thank the reviewer for their extensive list of suggestions regarding typos and word choices. We’ve taken these into consideration and updated the text accordingly.

We thank the reviewer for their elaborate comments.

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.

We have trained several models to replicate the results from Hahn et al. (2021). We used the best hyperparameters they report, but we also experimented with the following changes: Using RoPE for positional encoding instead of sinusoidal positional encodings in the decoder. This increased the correct rate from 97.8% to 98.0% on the validation set. Using the AdaCos loss function and feature normalization $f_{fn}$. The correct rate on the validation set increased to 98.2% when combined with RoPE. After determining the best baseline model on the validation set, we evaluated it on the test split of LTLRandom35 and obtained a 98.2% correct rate against the 98.5% reported by Hahn et al. (2021).

To explain this in the paper, we added a paragraph after the first paragraph in the “LTL Solving” subsection (page 8, line 378).

The authors do not provide the training time, hardware, number of epochs/steps, etc., for any of the experiments and baselines.

We provided the batch size and training steps in Table 3 (Table 2 in the original manuscript) for all experiments. The training steps are the same for all models within the same experiment. The hardware used in the experiments was varied, and as a result, the training times are not directly comparable. However, we used the same hardware (single NVIDIA H100) for the models that were trained on the perturbed dataset (Table 2). The baseline model took 2 hours 10 minutes, and our model took 2 hours 11 minutes. This demonstrates that the overhead of our method is negligible.

Hyperparameter search. We agree that our hyperparameter search exhibits high variance despite our efforts. As the reviewer suggested, we moved this section to Appendix and only presented the best models in the main text.

Immunity to renaming. In accordance with the reviewer’s suggestion, we renamed “empirical proof” to “empirical evidence”. As they mentioned, our method can be considered “immune to renaming” by construction in the sense that changing a variable name does not necessarily change its embedding. However, due to randomness, different variables—and perhaps even the same variable across different runs—will have different embeddings.

In the alpha-covariance experiment, we generate a random embedding for each AP token once at the start, and then observe the output of the model for each renaming permutation. Thus, alpha-conversions in this experiment are equivalent to shuffling the random embeddings in our method. As a result, the alpha-covariance experiment measures our model’s robustness against differences in random embeddings. We have added this explanation to the revised text (the second last paragraph in Alpha-Covariance section, lines 448-452).

AP Generalization Baseline. We have added the baseline that the reviewer recommended to the generalization experiments (Sections 5.1.2, 5.1.4, 5.2.3). We observe that our method outperforms this baseline on the LTL solving task. We added a new paragraph (on page 10) to discuss the results.

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.

In each of these figures, all heatmaps share the same y-axis. Consequently, in the original manuscript, we showed the y-axis legend only for the leftmost heatmap. This allows us to place the heatmaps closer to each other for easier comparison. In the revision, we have either added the axis legends or clarified that the y-axis is shared in the caption for all heatmap figures.

We appreciate the suggestion, but we did consider adding subfigure labels upon the suggestion but ended up avoiding them for simplicity, as each heatmap already has a title.

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.

We have applied this change in the revision.

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.

The y-axis of the green box represents the number of unique characters in the dataset. Therefore, although it overlaps the impossible region, it represents that the dataset features 30 unique characters across different samples. We have updated the explanation in the figure’s caption to clarify.

We appreciate the insights provided by the reviewer.

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.

We agree that the LTL perturbation experiment was designed to showcase the strengths of our method. However, we believe that it’s important to empirically demonstrate that our method induces a favorable inductive bias for alpha-equivalence. Technically, the proposed model is also forced to operate on out-of-distribution samples in this experiment if we treat the model as a black-box. However, the construction of embeddings in our model allows it to process the biased samples in the same way that it processes unbiased samples.

The difference between our method and traditional embeddings can be likened to the difference between convolutional neural networks (CNNs) and multi-layer perceptrons (MLPs). Anything that can be learned by a CNN can also be learned by an MLP, but CNNs present an inductive bias for translation invariance, similarly to how our method promotes alpha-covariance. Moreover, CNNs can operate on inputs larger than the training samples, resembling the vocabulary generalization capabilities of our method. To empirically verify the inductive bias of CNNs, an experimenter could remove all translation variance in the training set (similarly to the perturbed dataset in our experiment), and evaluate the models on translated samples. This is the core idea behind our LTL perturbation experiment. Clearly, however, this CNN analogy has its limits: Since our method incorporates randomness, alpha-covariance is not fully guaranteed by construction; different random embeddings can lead to different outputs. That’s why the LTL perturbation experiment is potentially more intriguing than its CNN counterpart.

I would want to see it evaluated on something other than a toy synthetic dataset.

Although our first experiment task (copying with extendable vocabulary) involves a toy dataset, the second task (LTL solving) is far from being a toy example despite the fact that the dataset is synthetic. LTL solving is an important problem in the literature, and the current SOTA seems to be DeepLTL (Hahn et al, 2021), which our paper builds on. In particular, DeepLTL can solve problems on which the classical solvers time out. Hahn et al. (2021) propose another dataset (LTLPattern126) for the same task that—instead of being synthetically generated—is created from real LTL formula-trace patterns found within the literature. We would be delighted to present experimental results on this dataset as well. But unfortunately, it was not released publicly.

Meaningful variable names

The reviewer’s remarks about meaningful variable names are insightful and we agree that this will be an important consideration for future applications of our method. However, there are many applications in which meaningful variable names are not available, with one such example being the presented LTL solving problem. Even the previously mentioned LTLPattern126 dataset does not feature meaningful variable names. Since our applications do not involve meaningful variable names, we consider this to be beyond the scope of our paper. But we agree that this is an interesting direction for future work. Thus, in the revision, we have mentioned this idea in the conclusion.

DeBruijn indices

DeBruijn indices present a natural way to represent bound variables in lambda calculus without explicitly naming them. However, it is not directly applicable to the tasks we considered in the experiments section. Since DeBruijn indices depend on the structure of lambda calculus, adapting DeBruijn indices to our tasks is not straightforward. Furthermore, DeBruijn indices do not address vocabulary generalization, which was our primary motivation.

Alpha-Renaming Baseline

We have added the reviewer's suggestion as a baseline in Sections 5.1.2, 5.1.4, 5.2.3 (also see the “Baselines” paragraph on page 5, line 250). We have also added a paragraph to discuss the results (page 10, line 486).

Human-written proofs or code

We thank the reviewer for this suggestion. While training a model on human-written proofs or code to demonstrate the impact of alpha-equivalence is clearly an interesting idea, it is beyond the scope of our current work. Our focus was on tasks where human-written variable names are unavailable, such as the LTL solving task. Training a model on human-written data would require not only a shift in focus but also substantially more computational resources due to the scale and complexity of such datasets. We appreciate the reviewer highlighting this direction and agree that it represents an intriguing area for future research.

References

Hahn, Christopher, et al. Teaching Temporal Logics to Neural Networks. arXiv:2003.04218, arXiv, 18 Feb. 2021. arXiv.org, https://doi.org/10.48550/arXiv.2003.04218.

Regarding the method itself, the randomization may introduce a lot of variance, so how would this variance be accounted for in the results presented?

1. In Section 5.1, we repeat the evaluation 10 times and report the average, as explained in the “Evaluation method” paragraph.
2. Section 5.1.3 “Sensitivity to randomness in embeddings” is dedicated to investigating this question.
3. In the alpha-covariance experiment (Section 5.2.2), we generate the embeddings once at the start for our method. This means that the alpha-conversions in this experiment are equivalent to shuffling the random embeddings in our method. Therefore, the alpha-covariance measures our model’s robustness against differences in random embeddings.

I was not sure what N.D., H.V. ,etc. were showing in one of the tables

The table that the reviewer is referring to is an in-text table at the top of page 7 in the original manuscript. The explanation for these acronyms can be found in line 330 in the original paper, immediately after the table. However, this table is now in the appendix after the revisions.

The presentation could be improved with some examples and real-world motivation of LTL and relating them with the empirical results

The newly added problem definition in the revised manuscript now features examples.

How significant are the empirical results (please see under weaknesses for details)

We think that our experiments successfully demonstrate the following:

1. Our embeddings can generalize to larger vocabulary sizes. This is seen in Sections 5.1.1, 5.1.2, 5.1.4, and 5.2.3. The significance of the result is more pronounced in larger experiments, such as the bigger copy task and the LTL solving task.
2. Our embeddings create an inductive bias for learning alpha-equivalence (Sections 5.2.1 and 5.2.2). Specifically, our model maintains a good performance despite the perturbation while the performance of the baseline model plummets under perturbation. This indicates that our method introduced a robust inductive bias.

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.

We would like to highlight that the LTL solving application is a real, important problem in the formal verification literature. DeepLTL (Hahn et al., 2021), which is the method that we build on in the LTL solving subsection, is able to solve formulae on which the classical solvers time out.

The value of alpha-equivalence can be intuitively understood in formal languages such as LTL: Since renaming the APs does not alter the meaning, changing the names of the atomic propositions (APs) in the input should not affect the model’s output in an ideal world.

The concept of alpha-equivalence can be likened to translation in the vision domain. Translation invariance is desired in applications where the location of the object within the image does not matter. Likewise, alpha-covariance is desired when interchangeable tokens exist in a language modeling problem. Similarly to how convolutional neural networks (CNNs) introduce an inductive bias for translation invariance, our method facilitates learning alpha-covariance.

Regarding the tradeoffs, in the conclusion section, we highlighted how the performance on in-distribution samples decreases slightly in our method (line 510 in the original manuscript, line 529 in revision), as the results in Table 2 indicate. We think this is an example of the well-known bias-variance tradeoff.

We thank the reviewer for their feedback.

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).

To the best of our knowledge, no other work in the literature attempts to create an extensible embedding for interchangeable tokens, and our dual-part embedding method is novel, as far as we are aware. If the reviewer is aware of any prior work that aligns with this approach or presents similar contributions, we would be grateful if they could provide references to help us better position our work within the existing literature.

Although generating random embeddings is a popular technique for initialization, it constitutes only a part of our method and is used for a different purpose. Furthermore, generating the random part in our embeddings entails special considerations that led us to propose several random generation methods.

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.

Copying task is an important synthetic problem for autoregressive models because many real-life tasks involve copying as a subtask, e.g., when asked to fix a bug in a given code snippet, an LLM must copy most of the input as-is, and only alter the faulty part. The transformer models are better than many other models in this task (Jelassi et al., 2024) since the attention mechanism has access to the full context. As a result, we only considered transformer-based models as baselines.

The second dataset seems like an existing benchmark and it is not clear what the “baseline” is in the case.

We have added a paragraph in Section 5 and another in Section 5.2 to explain the baselines. This dataset is not a benchmark. We apply our embeddings to DeepLTL (Hahn et al., 2021), which approaches the LTL solving problem using a language modeling perspective.

Also, there is a perturbed and limited dataset which again is not very clear as to what is the difference is between the two.

We kindly refer to the following parts in the first submitted manuscript:

1. Lines 395-397 (lines 387-392 in the revision): “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.”
2. Lines 421-422 (lines 415-418 in the revision): “Table 4 (Table 2 in the revision) also contains evaluations of the baseline and the new model trained with a severely limited number of samples: 80,000 instead of 799,909.”

We would be more than happy to explain further if the reviewer can please specify the unclear aspects.

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.

We are not aware of any other metric to measure a model’s robustness to alpha-conversions. The proposed metric is straightforward: It simply counts the variation in the outputs of the model corresponding to the alpha-equivalent pairs and normalizes this value to [0, 1] range (since the total number of alpha-equivalent pairs depends on AP count), with 1 being the most desirable value.

In the revision, we have updated the “Alpha-Covariance” section to emphasize that there is no other metric available (to the best of our knowledge) and provide more justification (e.g., line 433: “The model's sensitivity to alpha-conversions could be quantified by simply $|\mathbb{U}|$, but this value may be hard to interpret since it depends on $|\mathbb{P}|$.”). Please keep in mind that both the original submission (page 9, lines 445-450) and the revision (page 9, lines 441-446) features an intuitive explanation about the metric.

References

Hahn, Christopher, et al. Teaching Temporal Logics to Neural Networks. arXiv:2003.04218, arXiv, 18 Feb. 2021. arXiv.org, https://doi.org/10.48550/arXiv.2003.04218.

Jelassi, Samy, et al. Repeat After Me: Transformers Are Better than State Space Models at Copying. arXiv:2402.01032, arXiv, 3 June 2024. arXiv.org, https://doi.org/10.48550/arXiv.2402.01032.

Following the insightful discussion with the reviewers, we made another revision to improve the experiments and emphasize our contributions.

Updates:

1. We added the alpha-renaming baseline to the dataset perturbation experiment (Table 2, Section 5.2.1). As noted by Reviewers xSvQ and wK8E, this new baseline constitutes a better comparison for our model.
2. To complement the previous point, we evaluated the alpha-covariance performance of the models in the LTL generalization section up to 10 APs (Table 3, Section 5.2.3). We commented on these results (page 10, line 508).
3. We moved the limited dataset experiment from Section 5.2.1 to appendix (Appendix A.4) since its results are very similar to the perturbation experiment. Furthermore, presenting these together in Section 5.2.1 has previously led to some confusion, as our discussion with Reviewer BxyR shows.
4. We updated the abstract and the introduction section to highlight the alpha-renaming baseline and alpha-covariance, with the intention of communicating our contributions better.
5. We did some minor fixes to improve writing.

Overall, this update aims to improve the relevance of alpha-covariance by providing a better baseline and investigating alpha-covariance under out-of-distribution settings. We believe that these additions have significantly improved the paper, and we are grateful for the valuable suggestions and feedback provided by reviewers. We now believe that all major concerns raised in the reviews have been addressed.