Finitely Verifiable Segmentation: Decidability for Every Tokenizer with a Finite-State Verifier
Organizations: Independent Researcher
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.
Figures & tables
| Result | Statement | Where |
|---|---|---|
| Four decisions | Certification, the boundary gap and realizability are decidable for every supplied verifier, and full equivalence for every pair of them; certification and equivalence return a witness string when negative, the boundary gap a pumpable lasso, realizability the mask | Theorem 1 |
| Cut and chunk independence | Whether a certified cut lets both its sides scan alone, and whether all of an inventory’s cuts do at once, are decidable, each with a shortest counterexample; the first for every pair implies the second, not conversely; every maximal-munch cut and inventory is independent, WordPiece and splice ones need not be | Theorems 2 and 3 |
| Where the class sits | A regular token set with unbounded commit delay has no finite-state scanner yet a finite verifier; non-regular domains are outside; a regular domain is not sufficient | Section 4 , Lemma 1 , Proposition 1 |
| A normal form | Markings are length-preserving, so finite verifiability coincides with rationality of the marking relation; undecidability sits in presentations that do not convert effectively to a verifier | Proposition 2 , Section 4 |
| Closure | Pipelines over a labeled stage one, restrictions, splitter pre-tokenizers and byte-fallback unions of literal policies stay in the class and inherit all six decisions | Theorem 4 |
| Transfer | Certificates are monotone under restriction, forced at splitter boundaries, subset-bounded through pipelines, and lifted through pipelines exactly when a product of two stage-local automata is empty, with a per-label side condition as the sufficient corollary; a tower’s certificate factors through its levels on the tower’s own domain | Propositions 4 to 6 , Theorem 5 , Corollary 1 , Proposition 7 |
| Dictionary | Kept | Recovered | Anchors per KiB | Gap p99 | Longest stretch | |||
|---|---|---|---|---|---|---|---|---|
| exact | test | exact | test | |||||
| JSON | base | 1,174 | 482.4 | |||||
| 1 | 1,168 | 1,132 | 36 | 480.1 | 476.4 | 17 / 17 | 22 / 22 | |
| 2 | 1,162 | 1,068 | 94 | 478.0 | 462.8 | 17 / 17 | 22 / 24 | |
| 4 | 1,152 | 969 | 183 | 472.2 | 428.2 | 17 / 17 | 22 / 24 | |
| 8 | 1,136 | 799 | 337 | 461.9 | 365.9 | 20 / 21 | 30 / 32 | |