arXiv cs.CL· Nicklas Nidh\"ogg·· 13 小时前AI 评分24
有限可验证分词：为每个 Tokenizer 提供有限状态验证器的可判定性
Finitely Verifiable Segmentation: Decidability for Every Tokenizer with a Finite-State Verifier
AI 导读
论文提出“有限可验证分词”概念：若一个作用于标记串（字节+边界位）的有限自动机能恰好接受某分词策略自身的所有分词结果，则该策略有限可验证。在此假设下，窗口能否认证 token 边界、边界间隙是否有界、掩码是否保持生成可完成、两个策略是否等价这四个问题均变为可判定。该策略类严格介于在线可扫描策略与正则域策略之间，且对流水线常用的组合、限制、拆分和字节回退并集封闭，munch 库实现了全部六项判定。
正文 · 原文
Abstract:A segmentation policy assigns to each byte string at most one segmentation into tokens. Call it finitely verifiable when a finite automaton over marked strings, bytes paired with boundary bits, accepts exactly the policy's own segmentations. The automaton judges a proposed segmentation and need not compute one. The paper shows what that hypothesis buys. Four questions that practice settles by folklore become decidable, whether a window certifies a token boundary, whether the boundary gap is bounded, whether a mask keeps generation completable, and whether two policies are equivalent. The last three specialize limitedness, coaccessibility and the equivalence of single-valued transducers. The first refines the synchronizing cut of code theory, and two more ask whether a certified cut, or the cuts of an inventory, let each piece scan alone. The class sits strictly between the online-scannable policies and those with regular domains, and its inner frontier is Choffrut's and decidable in polynomial time. Markings are length-preserving, so the class is exactly the rational segmentation policies, a normal form rather than a restriction, and what the decisions need is a supplied verifier. The class is closed under the operations pipelines use: composition over a labeled stage, restriction, splitting, and byte-fallback union of literal policies. Each composite inherits the six decisions, and certificates transfer between stages under four laws. Under rational, unifilar, almost surely stopping finite-state sources, each mass of the weighted section is an exact rational, and so is each rate where expected length is positive. Maximal-munch lexing, canonical byte-pair encoding and two-mode WordPiece instantiate the interface, and the munch library implements all six decisions. Every theorem carries an executable check, and every reported statistic is a program's own output.
| Comments: | 36 pages, 1 figure, 2 tables. Artifact: this https URL . The modules, the gate and the records of the library and tokenizer instances are in the artifact, with a verifier that runs every module and holds each reported count to the output line it rests on. Companion to arXiv:2608.03473, arXiv:2608.09761, arXiv:2609.10600 and arXiv:2610.08854 |
| Subjects: | Formal Languages and Automata Theory (cs.FL); Computation and Language (cs.CL); Programming Languages (cs.PL) |
| Cite as: | arXiv:2610.30168 [cs.FL] |
| (or arXiv:2610.30168v1 [cs.FL] for this version) | |
| https://doi.org/10.48550/arXiv.2610.30168 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Nicklas Nidhögg [view email]
[v1]
Fri, 16 Oct 2026 18:17:30 UTC (69 KB)
来源：arXiv cs.CL · arxiv.org