We investigate challenges and possibilities of formal reasoning for encoder-only transformers (EOT), meaning sound and complete methods for verifying or interpreting behaviour. In detail, we condense related formal reasoning tasks in the form of a naturally occurring satisfiability problem (SAT). We find that SAT is undecidable if we consider EOT, commonly considered in the expressiveness community. Furthermore, we identify practical scenarios where SAT is decidable and establish corresponding complexity bounds. Besides trivial cases, we find that quantized EOT, namely those restricted by some fixed-width arithmetic, lead to the decidability of SAT due to their limited attention capabilities. However, the problem remains difficult, as we establish those scenarios where SAT is NEXPTIME-hard and those where we can show that it is solvable in NEXPTIME for quantized EOT. To complement our theoretical results, we put our findings and their implications in the overall perspective of formal reasoning.

翻译：本研究探讨了仅编码器Transformer（EOT）形式化推理面临的挑战与可能性，即验证或解释其行为的可靠且完备的方法。具体而言，我们将相关的形式化推理任务归纳为一种自然产生的可满足性问题（SAT）。研究发现，若考虑表达能力研究领域通常探讨的EOT模型，其SAT问题是不可判定的。此外，我们识别了SAT可判定的实际场景，并建立了相应的复杂性界限。除平凡情况外，我们发现量化EOT——即受限于某种固定宽度算术运算的模型——因其有限的注意力机制导致SAT具有可判定性。然而，该问题依然具有较高难度：我们证明了量化EOT的SAT问题在特定场景下具有NEXPTIME难度，而在另一些场景中可被证明能在NEXPTIME内求解。为补充理论结果，我们将研究发现及其意义置于形式化推理的整体研究视野中进行综合评述。