arXiv:2610.30168 · v2
Finitely Verifiable Segmentation: Decidability for Every Tokenizer with a Finite-State Verifier
摘要
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. From a supplied verifier the paper gives constructive decisions for four questions, whether a window certifies a token boundary, whether the boundary gap is bounded, whether a mask can keep generation from dead-ending, and whether two policies are equivalent. The last three specialize limitedness, co-accessibility 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 online scannability is decidable in polynomial time through Choffrut's theorem. Markings are length-preserving, so the class is exactly the rational segmentation policies, a normal form rather than a restriction. The class is closed under four pipeline operations, composition over a labeled stage, restriction to a regular schema, splitting at character-class changes, 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.
作者备注：39 pages, 1 figure, 2 tables. v2: revises the introduction to credit existing exact procedures (Koo et al. for masks, Berglund et al. for BPE equivalence), proves gap boundedness undecidable from a program and the weighted theorem without unifilarity. Artifact: https://doi.org/10.5281/zenodo.23708161 . Companion to arXiv:2608.03473, arXiv:2608.09761, arXiv:2609.10600 and arXiv:2610.08854