Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning
Authors: Marco Sälzer, Eric Alsmann, Martin Lange
ICLR 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (tr SAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that tr SAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where tr SAT is decidable and establish corresponding complexity bounds. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning. |
| Researcher Affiliation | Academia | Marco S alzer University of Kaiserslautern-Landau, RPTU Kaiserslautern, Germany EMAIL Eric Alsmann Theoretical Computer Science / Formal Methods University of Kassel, Germany EMAIL Martin Lange Theoretical Computer Science / Formal Methods University of Kassel, Germany EMAIL |
| Pseudocode | No | The paper describes theoretical constructions and proofs (e.g., in Section 4 and 5, and Appendix B and C) but does not include any clearly labeled pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not contain any explicit statements about the release of source code, nor does it provide links to any code repositories or mention code in supplementary materials. |
| Open Datasets | No | The paper is theoretical, analyzing the complexity of transformer encoder satisfiability. It references 'tiling problems' (Appendix A) as a theoretical tool for proofs, not as empirical datasets used in experiments. There is no mention of actual datasets, links, DOIs, or citations to public data used for empirical evaluation. |
| Dataset Splits | No | The paper is theoretical and does not conduct experiments involving datasets. Therefore, there is no discussion of dataset splits for training, validation, or testing. |
| Hardware Specification | No | The paper is a theoretical work on the complexity of transformer encoder satisfiability. It does not describe any experiments that would require specific hardware, and thus no hardware specifications are mentioned. |
| Software Dependencies | No | The paper is theoretical and focuses on computational complexity and formal reasoning. It does not describe any implemented systems or experiments that would require listing specific software dependencies with version numbers. |
| Experiment Setup | No | The paper is theoretical and focuses on computability and complexity results. It does not describe any experimental setup, training configurations, or hyperparameter values. |