arXiv cs.AI· Chih-Duo Hong, Hongjian Jiang, Anthony W. Lin, Oliver Markgraf, Julian Parsert, Tony Tan·· 12 小时前AI 评分18
有序数据序列上确定性寄存器自动机（DRA）的合成与验证
Synthesis and Verification of Register Automata over Data Sequences (Technical Report)
AI 导读
研究针对有序数据序列的确定性寄存器自动机（DRA）合成与验证，提出局部搜索合成流程与精确鲁棒性检查器，在寄存器数固定时检查器为多项式时间、对该数量的依赖为指数级。
正文 · AI 翻译
摘要：数据序列，例如时间序列、轨迹和传感器流，是定义在大型或无限数据域上的词。它们的性质往往取决于不同位置值之间的比较，而有限自动机无法直接表达这一点。我们研究有序数据序列上确定性寄存器自动机（DRA）的合成与验证。DRA 将有限控制与用于记忆数据值的寄存器相结合，为定量序列语言提供紧凑的符号描述。我们的技术核心是一种局部搜索合成过程以及针对 DRA 的精确鲁棒性检查器。我们将字母表理论固定为带有有理保护常量的有序有理数 $(\Q;<,=)$，并使用非负仿射累加器代价。对于固定数量的 DRA 寄存器，检查器在多项式时间内运行；其对该数量的依赖是指数级的。它将鲁棒性归约为可覆盖性，进而归约为最短路径问题。由于搜索范围覆盖 $\Q^+$，它会产生变长见证，并且对于 RAA 可定义的比对代价（如 DTW），会探索一个没有先验长度界的反例空间。作为一个应用，我们使用学习到的 DRA 作为被查询神经序列分类器的可解释替代模型。一个可能近似正确（PAC）验证循环会细化被拒绝的候选，在发现时返回分类器真正的非鲁棒性见证，并且仅在接受替代模型时为其保真度和局部稳定性提供统计保证。我们在 $\textsc{RAExc}$ 中实现了该框架，从而能够合成可解释自动机并验证其鲁棒性。我们在基准语言和序列化 MNIST 上评估了该方法，展示了高准确率，同时验证了所学自动机的鲁棒性。
| 主题： | 人工智能（cs.AI）；形式语言与自动机理论（cs.FL）；机器学习（cs.LG） |
| 引用为： | arXiv:2511.19100 [cs.AI] |
| （或使用 arXiv:2511.19100v2 [cs.AI] 查看此版本） | |
| https://doi.org/10.48550/arXiv.2511.19100 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Hongjian Jiang [查看电子邮件]
[v1]
2025年11月24日星期一 13:36:45 UTC（185 KB）
[v2]
2026年10月21日星期三 13:42:27 UTC（138 KB）
来源：arXiv cs.AI · arxiv.org