Why Are Linear RNNs More Parallelizable?
该论文通过建立线性 RNN 与非线性 RNN 与标准复杂度类（如、和）之间的紧密联系，从理论层面揭示了线性 RNN 之所以能像 Transformer 一样高效并行化，是因为其可被建模为对数深度算术电路，而非线性 RNN 因能解决或完全问题而存在根本性的并行化障碍。
💻 Category
cs.FL
28 篇论文
2-Coloring Cycles in One Round
本文展示了由大语言模型主导发现并已在 Lean 4 中形式化证明的结论：存在一种单轮随机分布式算法可将循环图的单色边期望比例降至 0.24118 以下，同时证明了该比例无法低于 0.23879，从而显著改进了此前 0.25 和 0.2 的上下界。
Reachability in VASS Extended with Integer Counters
本文研究了扩展了整数计数器的 VASS（VASS+Z）的可达性问题，证明了当固定 N 计数器数量时，1-VASS+Z 是 NP 完全的，d-VASS+Z 的复杂度上界为 ，且整数计数器的引入显著降低了使问题呈现 PSPACE 难和 TOWER 难所需的 N 计数器维度。
Algebraic Characterization of Reversible First Degree Cellular Automata over
本文针对有限元胞自动机，通过建立仅含三个代数条件的充要判据，实现了在常数时间内对任意规模一维三邻域态一阶元胞自动机可逆性的判定与规则合成。
Computational Complexity of Alignments
本文研究了不同类 Petri 网中计算对齐的算法复杂度，证明了该问题在安全 Petri 网等广泛类别中是 PSPACE 完全或 NP 完全的，但在活且安全的 S-系统中可在多项式时间内求解。
History-Deterministic Büchi Automata are Succinct
该论文通过构造一个仅含 65 个状态的历史确定性 Büchi 自动机，并结合理论推导与计算机辅助证明，解决了该领域悬置十余年的难题，证实了此类自动机在状态数量上严格优于任何等价的确定性 Büchi 自动机。
Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
本文详细阐述了利用 Uppaal 工具对分布式中间件 CARE 进行形式化建模、基于随机定时自动机网络的属性验证以及从抽象模型生成具体测试用例的全过程，旨在通过形式化方法提升该开源应用的可靠性。
SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification
本文提出了名为 SpotIt 的新评估流程，利用形式化等价验证引擎主动搜索能区分生成查询与真实答案的数据库，以克服现有基于测试的 Text-to-SQL 评估方法因偶然匹配而高估模型性能的局限性。