Characterizing neural networks in terms of better-understood formal systems has the potential to yield new insights into the power and limitations of these networks. Doing so for transformers remains an active area of research. Bhattamishra and others have shown that transformer encoders are at least as expressive as a certain kind of counter machine, while Merrill and Sabharwal have shown that fixed-precision transformer encoders recognize only languages in uniform $TC^0$. We connect and strengthen these results by identifying a variant of first-order logic with counting quantifiers that is simultaneously an upper bound for fixed-precision transformer encoders and a lower bound for transformer encoders. This brings us much closer than before to an exact characterization of the languages that transformer encoders recognize.

翻译：用更易理解的规范系统来描述神经网络，有望揭示这些网络的能力和局限性。针对Transformer的这一研究仍是一个活跃领域。Bhattamishra等人已证明Transformer编码器至少与某种计数器具有相同表达能力，而Merrill和Sabharwal则论证了固定精度Transformer编码器仅能识别均匀$TC^0$中的语言。我们通过识别一种带计数量词的一阶逻辑变体，将其同时作为固定精度Transformer编码器的上界和常规Transformer编码器的下界，从而关联并加强了上述结论。这使得我们比以往更接近精确刻画Transformer编码器可识别的语言。