FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
本文提出了名为 FATE 的新基准系列（包含 FATE-H 和 FATE-X），旨在填补大型语言模型在竞赛数学与研究级抽象代数形式化证明之间的能力鸿沟，评估结果显示当前最先进模型在该领域表现极差，且其将自然语言推理转化为形式化证明的能力远弱于推理本身。
💻 Category
cs.FL
28 篇论文
Complexity of Linear Subsequences of -Automatic Sequences
该论文通过构建识别基本关系的-自动机并分析其状态复杂度，建立了-自动序列内部序列的子词复杂度与线性子序列状态复杂度之间的联系，解决了 Zantema 和 Bosma 关于最高位优先格式下线性子序列的未决问题，并探讨了利用 Büchi 算术构造相关自动机及执行序列操作时的状态与时间复杂度。
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
本文提出了一种结合语法引导合成（SyGuS）与扩展了谓词和函数更新的时序流逻辑（TSL）的新方法，通过从执行轨迹中挖掘数据转换与时序规范，实现了比被动学习基线更鲁棒且样本效率更高的反应式程序合成。
Randomise Alone, Reach as a Team
本文研究了对手存在下、玩家间无共享随机源且彼此独立的并发图博弈，证明了阈值判定问题属于实数存在理论（）且为 NP 难，几乎必然可达性判定为 NP 完全，并提出了适用于此类分布随机化场景的 IRATL 逻辑及相应求解算法。
Forgetting Event Order in Higher-Dimensional Automata
本文提出了一种基于区间 ipomset 的与事件顺序无关的高维自动机（HDA）语义，通过证明传统 ST 迹与区间 ipomset 的精确对应及结构上的范畴同构，消除了 HDA 中的事件顺序人为限制，从而为并发模型提供了统一且无偏的基础。
Turn Complexity of Context-free Languages, Pushdown Automata and One-Counter Automata
本文证明了无法判定上下文无关语言、下推自动机及单计数器自动机中接受字符串所需的最小转折数是否有界，揭示了有限转折下推自动机与有限转折单计数器自动机之间存在非递归的代价差异，并确立了基于转折数（包括次线性增长）的无限严格复杂度层级。
Context-Free Trees
本文研究了由穆勒和舒普提出的真正上下文自由树，证明了它们可用多边非确定性有限自动机进行有限状态描述，并确立了确定性情形下（无论是否带根）的同构问题是 NL 完全问题。
New properties of the -representation of integers
该论文利用 Walnut 定理证明器和 ChatGPT 5 等工具，证明了关于整数-表示（其中为黄金分割比）的若干新性质，并解决了 Kimberling 于 2012 年提出的猜想。
The Generation-Recognition Asymmetry: Six Dimensions of a Fundamental Divide in Formal Language Theory
本文首次将形式语言理论中生成与识别的不对称性统一为一个包含计算复杂度、歧义性、方向性、信息可用性、语法推断和时间性六个维度的多维现象，并指出这种不对称性源于识别始终受限于给定输入而生成未必受限，进而探讨了其在自然语言处理及大语言模型中的意义。
The complexity of finite smooth words over binary alphabets
本文证明了平滑词的因子均为有限平滑词，并在二元字母表上推进了关于其复杂度渐近行为的猜想，具体包括在偶数字母表上证明了该猜想、在任意二元字母表上确立了复杂度下界，以及改进了奇数字母表上的已知上界。
Formally Verified Linear-Time Invertible Lexing
本文介绍了 ZipLex，这是一个基于 Stainless 验证器构建的已验证框架，它通过结合新的令牌序列抽象、Huet 拉链及验证过的哈希表等优化技术，实现了兼具线性时间复杂度、最长匹配语义以及词法分析与打印互为逆运算特性的可逆词法分析。
Marking Data-Informativity and Data-Driven Supervisory Control of Discrete-Event Systems
本文针对模型未知的离散事件系统，提出了“标记数据信息性”这一新概念及其验证算法，并进一步定义了受限标记数据信息性与标记可信息化，从而在数据驱动框架下解决了满足给定规范的非阻塞标记监督控制设计问题。
Attention Meets Reachability: Structural Equivalence and Efficiency in Grammar-Constrained LLM Decoding
该论文通过引入结构歧义成本（SAC）和证明引擎无关的下界，揭示了语法等价性并不保证解码效率，并提出了基于可达性预言机的语法约束解码理论框架，以优化大语言模型在上下文无关语法约束下的解码性能与成本。
Warm Starting State-Space Models with Automata Learning
该论文证明了 Moore 机可精确实现为状态空间模型，并发现虽然纯数据驱动的状态空间模型在恢复符号结构时效率低下，但通过利用自动机学习进行符号化初始化，可显著提升模型在复杂系统中的训练速度与最终精度。
Online Monitoring of Metric Temporal Logic using Sequential Networks
本文提出了一种基于时序网络的统一在线监控框架，通过利用未来时间标记技术将度量时序逻辑（MTL）规范高效地转换为离散和稠密时间下的时序网络，从而在性能与可扩展性上优于现有方法。
Module checking of pushdown multi-agent systems
本文研究了推多代理系统（PMS）的模块检查问题，证明了针对 ATL 规范的检查是 2EXPTIME 完全的，而针对 ATL* 规范的检查则是 4EXPTIME 完全的，后者比前两者在计算复杂度上高出指数级，是少数具有初等但超过三重指数时间复杂度的自然判定问题之一。
The Expansion Problem for Infinite Trees
本文研究了无限树的拉姆齐型定理及相关组合工具，并将其应用于树代数的扩张问题。
Risk-Aware Autonomous Driving with Linear Temporal Logic Specifications
本文提出了一种基于线性时序逻辑（LTL）的风险感知自动驾驶方法，通过将包含事件时序与严重程度的 LTL 规范转化为线性规划问题，实现了在 Carla 仿真中平衡碰撞风险与交通违规等多类风险的类人驾驶策略合成。
On a sequence of Kimberling and its relationship to the Tribonacci word
本文利用 Walnut 定理证明器验证了 Clark Kimberling 关于特定二进制序列的猜想，揭示了该序列与无限 Tribonacci 词的关联，并确定了其子词复杂度和临界指数。
Classification of Local Optimization Problems in Directed Cycles
该论文针对有向环上的局部优化问题，在确定性和本地随机化 LOCAL 模型中给出了完整的分布式计算复杂度分类，证明了其复杂度必然属于 、 或 中的某一类，并提出了能够自动判定复杂度类别及合成最优分布式算法的高效元算法。