核心发现
方法论
论文提出双部token embedding：不可交换token使用可学习向量；可交换token由共享向量α与随机向量βi拼接而成，维度为dα+dβ。训练时每次前向传播重新采样βi，推理时固定一次。嵌入与输出投影采用三路weight tying，并对嵌入和特征向量做L2归一化，使用改造后的AdaCos损失。
关键结果
- 在复制任务中，训练数据为1000万条、序列长度不超过80、最多20个字符；固定嵌入无法外推新字符，而双部方法可近乎无误地处理长度和词表规模达到160的分布外组合。
- 在LTLRandom35上，Proposed模型正确率95.94%、精确匹配率76.45%；扰动数据下仍保持接近正常基线的正确率，并在3、4、5个AP上的alpha-covariance分别为97.66%、97.76%、98.29%。
- Alpha-renaming增强基线的LTL正确率为97.96%，但其alpha-covariance为99.55%、99.49%、98.86%；Proposed略低，却无需为测试词表显式学习独立嵌入，并能生成未见token表示。
研究意义
研究把形式语言中的变量重命名问题转化为可测量、可训练的表示学习问题。它解决了传统模型只能识别训练词表、难以保持符号置换一致性的长期痛点，为LTL、命题逻辑、λ演算和程序分析提供更系统的泛化机制。对工业验证系统而言，新增原子命题不再必然要求重新训练词表层。
技术贡献
核心贡献包括alpha-covariance指标、可扩展的双部嵌入矩阵，以及与Transformer encoder-decoder兼容的训练方案。随机部分不是简单噪声增强：它在保持语义共享的同时提供token身份，训练期重采样迫使模型学习与具体随机样本无关的区分规则。论文还将AdaCos改造成适合序列建模的形式，合并batch与长度维度并将尺度裁剪到100。
新颖性
多数模型为每个符号分配独立参数，alpha-renaming通常只作为数据增强。本文首次系统定义可交换token的词表扩展任务，并提出同时满足“语义相同、身份可辨”的结构化嵌入；相较仅暴露更多token的增强方法，它把置换鲁棒性直接编码进表示生成过程。
局限性
- 随机向量的离散生成集合规模随dβ指数增长；邻近点和超立方体方法在超过32维时难以进行整数映射与reservoir sampling。
- 实验主要集中于合成复制、LTL和命题逻辑，尚未证明该机制能处理自然语言中更复杂、非严格可交换的实体与上下文语义。
- alpha-covariance衡量输出一致性，不等同于逻辑正确性；模型仍可能对所有变体稳定地产生错误答案。
未来方向
未来可研究多类可交换token、连续或哈希式随机编码、更大规模语言模型及真实程序和证明数据。还应建立同时衡量正确率、精确匹配、置换鲁棒性与计算成本的统一基准，并分析dα、dβ和随机生成器对容量及泛化边界的影响。
AI 总览摘要
现代Transformer能够完成定理证明、符号积分和LTL求解，但其词表通常是固定的：训练时未出现的新原子命题或变量无法直接表示。更深层的问题是，形式逻辑中的绑定变量可以改名而不改变意义，即alpha-equivalence；普通嵌入却把每个符号当作完全独立的对象。
Işık、Cinbis与Gol提出Interchangeable Token Embeddings，将可交换token表示拆成共享可学习部分α和随机区分部分βi。α传递“它们属于同一语义类别”，βi保留身份差异；训练时重新采样βi，推理时固定随机码。模型采用Transformer encoder-decoder、RoPE或tree-positional encoding、三路weight tying和改造AdaCos损失，并以alpha-covariance评估改名鲁棒性。
结果显示，复制任务中双部嵌入可将训练范围最多20个字符、长度80外推至词表和长度160。LTLRandom35上正确率95.94%、精确匹配76.45%；在3至5个原子命题上的alpha-covariance为97.66%至98.29%。方法仍受随机空间、合成数据和指标局限，但为可扩展形式语言模型提供了清晰的工程起点。
深度分析
研究背景
Transformer已用于符号积分、回归和LTL求解。Hahn等人借助tree-positional encoding展示了长度泛化；传统工具如spot和aalta则依赖经典算法。然而，模型通常把每个原子命题视为固定词表项，无法接受训练后新增符号。λ演算、数学表达式和逻辑变量也存在同样的alpha-equivalence现象。
核心问题
设V=Vi∪Vn，其中Vi为可交换token，Vn为不可交换token。任意只置换Vi的双射f都应将输入a和输出b同步变换为语义等价的a′、b′。目标是在训练词表V上学习后，支持更大的V′，并对所有这类alpha-renaming保持正确且一致的预测。
核心创新
论文有三项创新。第一，定义可交换token的词表扩展实验协议。第二，提出alpha-covariance，将所有改名样本的预测逆变换后集合化，测量模型是否保持同一答案。第三，设计共享α加随机βi的嵌入结构，使语义相同与身份可辨同时成立，区别于单纯固定嵌入或alpha-renaming数据增强。
方法详解
- �� 嵌入构造：不可交换token使用L∈R^(n×dα)，可交换token共享α∈R^(1×dα)，并拼接βi∈R^(1×dβ)，总维度dmodel=dα+dβ。
- �� 随机生成：支持Normal Distribution、Neighboring Points（{-1,0,1}）和Hypercube Vertices（{-1,1}）；有限集合用reservoir sampling保证唯一性。
- �� 训练机制：每次forward重采样βi，避免模型记忆某次随机码；推理开始时生成并固定。
- �� 投影与损失：encoder、decoder和最终投影三路weight tying；嵌入及特征向量L2归一化，采用序列版AdaCos，尺度上限为100。
- �� 编码器使用逻辑任务的tree-positional encoding，复制任务使用RoPE；解码采用RoPE。
实验设计
实验统一使用Transformer encoder-decoder。任务包括1000万样本的可扩展词表复制、DeepLTL的LTLRandom35及同法合成数据、命题逻辑赋值预测。基线包括原始固定嵌入、扩大词表训练、alpha-renaming增强。LTL使用spot 2.11.6验证，beam size为3，并报告correct、exact match和alpha-covariance。
结果分析
复制实验中固定嵌入不能外推新字符，Proposed在长度与词表规模160附近几乎完美。LTLRandom35上普通基线为98.23% correct、83.23% exact；扰动后降至34.13%、12.12%。Alpha-renaming为97.96%、77.66%，Proposed为95.94%、76.45%，但后者在扰动下保持稳健。Llama 3.2 3B仅24.33% correct、0.34% exact。
应用场景
该方法适合LTL验证中新增原子命题、命题逻辑赋值、程序变量重命名、λ演算和形式证明生成。前提是token类别可预先标注，且同类token确实满足置换语义。工程上可减少为扩展词表而重新训练嵌入层的需要，并与现有Transformer及位置编码结合。
局限与展望
方法假设可交换关系是明确且严格的；自然语言实体通常受上下文、指代和世界知识影响，不能直接套用。离散随机集合随维度指数增长，连续高维采样又难以保证绝对唯一。实验主要是合成或形式数据，规模和模型类型有限。未来应测试真实代码、证明语料、多类token及更大型模型，并优化随机编码和鲁棒性指标。
通俗解读 非专业人士也能看懂
把模型想成一家工厂。普通词表给每种零件制作一块固定模具：见过的零件能加工，没见过的新零件没有模具。更麻烦的是，有些零件虽然名字不同、颜色不同，功能却完全一样；如果工厂只记名字，就会误以为它们不同。
论文的方法给同类零件两层标签。第一层是共享标签，告诉机器“这些零件属于同一种功能”；第二层是临时编号，让机器仍能分清这是第一个、第二个还是第三个零件。训练时不断更换临时编号，工厂就不能死记某个编号，而必须真正学会按功能和位置工作。
因此，未来出现新零件时，只需生成新编号，不必重新制作整套模具。复制实验表明，训练最多20种字符、长度80后，系统还能处理规模接近160的组合。它也能理解逻辑中把变量改名并不会改变答案。
简单解释 像给14岁少年讲一样
想象你在玩一个解谜游戏，地图上有几个角色：A、B、C。游戏真正关心的是“哪个角色做了什么”，而不是角色名字本身。如果把A改叫Z，只要所有地方一起改，谜题答案就不该变化。普通AI却可能把每个名字当成完全不同的技能卡，所以没见过Z就不会玩。
这篇论文给AI设计了两层卡片。第一层是“同类标志”，告诉AI A、B、C都是可互换角色；第二层是随机身份码，让AI知道当前到底是A还是B。训练时不断换身份码，AI不能背答案，只能学习角色之间的关系。
研究者还让AI做复制字符串、解决LTL时间逻辑和命题逻辑题。复制任务里，训练只见过最多20种字符和长度80，但新方法能处理接近160的字符种类和长度。LTL任务中，它的正确率达到95.94%，而且把变量改名后仍能保持相近答案。
当然，它不是万能的。随机编号太多时会占用空间，实验也主要是人工生成的逻辑数据。下一步要看看它能否帮助程序分析、数学证明，甚至更复杂的语言模型。
术语表
Interchangeable Token Embedding（可交换Token嵌入）
为语义等价但身份不同的token构造共享与区分两部分表示。它允许模型扩展同类token而不为每个新token学习完整参数。
论文的核心方法。
Alpha-equivalence（Alpha等价）
绑定变量改名后，表达式含义保持不变的关系。关键是相关输入和输出必须同步重命名。
用于定义任务与鲁棒性。
Alpha-covariance（Alpha协变性）
将不同改名样本的预测逆变换后，检查它们是否一致的指标。数值越高表示对alpha-conversion越稳定。
论文提出的评估指标。
Tree-positional encoding（树位置编码）
利用语法树位置表示结构关系，而非只使用线性位置。它帮助逻辑模型泛化到更长公式。
LTL和命题逻辑编码器使用。
AdaCos
一种自适应调整余弦分类logit尺度的损失方法。论文将其改造成适合序列建模并将尺度裁剪为100。
用于归一化嵌入训练。
开放问题 这项研究留下的未解疑问
- 1 尚不清楚共享随机结构能否迁移到自然语言实体，因为自然语言中的“可交换”常依赖上下文而非严格语义定律。
- 2 如何在超高维随机空间中低成本保证唯一性，并建立词表容量与dβ之间的理论界限，仍缺少分析。
应用场景
近期应用
LTL验证系统
验证工具可将原子命题作为可交换token，在新增系统变量时直接生成嵌入。结合spot检查输出，可减少因扩展词表而重新训练模型的需求。
程序变量与形式证明
代码分析或证明生成模型可对变量重命名保持行为一致。前提是变量作用域和绑定关系已被可靠解析，并同步变换输入输出。
远期愿景
系统化神经符号推理
未来模型可同时扩展符号集合、泛化序列长度并保持置换一致性，形成更适合数学、验证和程序合成的神经符号基础设施。
原文摘要
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