BriefGPT.xyz
May, 2024
编码器-只有Transformer的形式推理的计算复杂性
The Computational Complexity of Formal Reasoning for Encoder-Only Transformers
HTML
PDF
Marco Sälzer, Eric Alsmann, Martin Lange
TL;DR
研究了编码器-只有变压器 (EOT) 的形式化推理的挑战和可能性，发现 EOT 的满足性问题 (SAT) 是不可判定的，但限定了注意力能力的量化 EOT 可以在 NEXPTIME 内解决 SAT 问题。
Abstract
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
→