Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916628324679680 |
|---|---|
| author | Sälzer, Marco Alsmann, Eric Lange, Martin |
| author_facet | Sälzer, Marco Alsmann, Eric Lange, Martin |
| contents | We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that trSAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where trSAT is decidable and establish corresponding complexity bounds. Beyond trivial cases, we find that quantized TE, those restricted by fixed-width arithmetic, lead to the decidability of trSAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where trSAT is NEXPTIME-hard and others where it is solvable in NEXPTIME for quantized TE. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_18548 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning Sälzer, Marco Alsmann, Eric Lange, Martin Logic in Computer Science Artificial Intelligence Computational Complexity Machine Learning We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that trSAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where trSAT is decidable and establish corresponding complexity bounds. Beyond trivial cases, we find that quantized TE, those restricted by fixed-width arithmetic, lead to the decidability of trSAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where trSAT is NEXPTIME-hard and others where it is solvable in NEXPTIME for quantized TE. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning. |
| title | Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning |
| topic | Logic in Computer Science Artificial Intelligence Computational Complexity Machine Learning |
| url | https://arxiv.org/abs/2405.18548 |