证明状态空间模型的可满足性问题在一般情况下不可判定，但受限条件下可解。
The Computational Complexity of Satisfiability in State Space Models
- 分析状态空间模型的可满足性问题，分情况研究其计算复杂度
- 有上下文长度限制时，问题为NP完全或NEXPTIME，量化模型下为PSPACE或EXPSPACE
- 结果为验证基于SSM的语言模型提供理论基础，适合形式化推理研究者
我们分析了状态空间模型（SSM）的可满足性问题ssmSAT，该问题判断输入序列能否使模型进入接受状态。发现ssmSAT在一般情况下不可判定，体现了SSM的强大计算能力。针对实际应用，我们识别出两个自然约束：当上下文长度有界时，若输入长度以单位制表示，ssmSAT为NP完全；若以二进制表示，则为NEXPTIME（且是PSPACE-hard）。对于固定位宽算术下的量化SSM，ssmSAT为PSPACE完全或EXPSPACE，取决于位宽编码方式。这些结论适用于对角门控SSM，并推广至时不变SSM。本研究首次建立SSM形式推理的复杂性图景，揭示了验证基于SSM语言模型的根本限制与可能性。
原文摘要 · Abstract (English)
We analyse the complexity of the satisfiability problem ssmSAT for State Space Models (SSM), which asks whether an input sequence can lead the model to an accepting configuration. We find that ssmSAT is undecidable in general, reflecting the computational power of SSM. Motivated by practical settings, we identify two natural restrictions under which ssmSAT becomes decidable and establish corresponding complexity bounds. First, for SSM with bounded context length, ssmSAT is NP-complete when the input length is given in unary and in NEXPTIME (and PSPACE-hard) when the input length is given in binary. Second, for quantised SSM operating over fixed-width arithmetic, ssmSAT is PSPACE-complete resp. in EXPSPACE depending on the bit-width encoding. While these results hold for diagonal gated SSM we also establish complexity bounds for time-invariant SSM. Our results establish a first complexity landscape for formal reasoning in SSM and highlight fundamental limits and opportunities for the verification of SSM-based language models.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。