State Space Models 中形式推理的计算复杂度（扩展摘要）

基于摘要分析。本文研究 State Space Models 的可满足性问题（ssmSAT），主要对象是语言建模中作为 transformer 替代方案的递归架构。核心贡献是刻画该问题在一般情形与若干具有实践动机的限制下的可判定性和计算复杂度，而非提出新的模型训练方法或报告任务性能提升。 作者报告，ssmSAT 在一般情形下不可判定；在上下文长度有界的条件下，该问题为 NP-complete。若模型被量化，即算术运算限制为固定字宽，可满足性仍然可判定，但不意味着求解高效：作者报告，依赖具体编码方式，相关情形可为 PSPACE-complete，或其复杂度处于 PSPACE 与 EXPSPACE 之间，后者与字宽的编码方式有关。这些结论不能脱离对应限制直接推广到所有 State Space Models。 技术阅读重点是“可判定”与“实际可验证”的区别：限制上下文长度或使用固定字宽算术可以改变判定问题的理论性质，但较高的复杂度仍可能限制通用验证程序的可扩展性。摘要未给出 ssmSAT 的精确定义、模型允许的运算、待满足性质的表达方式，以及归约和复杂度证明，因此上述边界的适用范围尚需全文验证；也不能据此断言某个具体模型无法验证。 作者讨论了这些结果对语言建模中 State Space Models 验证的潜在影响。材料没有提供 EEG/BCI 实验或明确的神经信号任务对应关系，不据此推导解码性能、跨被试泛化或部署安全性收益。已有 EEG 相关工作尚未检索确认。全文证明、限制条件及任何实证评估信息尚未验证。