analiza aiqbench
This paper gives formal-language guarantees for LLM tokenizers. Under a "finitely verifiable" condition, it shows that practical questions, such as whether a token boundary is certified, whether generation can always be completed under a mask, and whether two tokenizers are equivalent, become decidable. The results are theoretical and tied to specific implementations (maximal-munch lexing, BPE, WordPiece), so their practical value depends on whether those tokenizers actually meet the condition and on the cost of supplying a verifier.
Finitely Verifiable Segmentation: Decidability for Every Tokenizer with a Finite-State Verifier
arXiv:2610.30168v1 Announce Type: cross 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.
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.
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
Formal Languages and Automata Theory (cs.FL); Computation and Language (cs.CL); Programming Languages (cs.PL)
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)
Text integral sub licența deschisă a publicației · 360 cuvinte
Subiecte conexe
Trajectory-Triggered Sparse Collaborative Decoding
arXiv · 19 oct. 2026
Unlock Exascale Performance on NVIDIA GB200 NVL72 with Slurm Topology-Aware Job Scheduling
NVIDIA · 21 mai 2026
MentorCollab: Selective Large-to-Small Inference-Time Guidance for Efficient Reasoning
arXiv · 31 iul. 2026
Cracking the Data Science Case Study Interview
Analytics Vidhya · 26 iul. 2026