cs.FLOct 16, 2026

Finitely Verifiable Segmentation: Decidability for Every Tokenizer with a Finite-State Verifier

Authors: Nicklas Nidhögg

Organizations: Independent Researcher

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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

ResultStatementWhere
Four decisionsCertification, 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 maskTheorem 1
Cut and chunk independenceWhether 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 beTheorems 2 and 3
Where the class sitsA 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 sufficientSection 4 , Lemma 1 , Proposition 1
A normal formMarkings are length-preserving, so finite verifiability coincides with rationality of the marking relation; undecidability sits in presentations that do not convert effectively to a verifierProposition 2 , Section 4
ClosurePipelines over a labeled stage one, restrictions, splitter pre-tokenizers and byte-fallback unions of literal policies stay in the class and inherit all six decisionsTheorem 4
TransferCertificates 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 domainPropositions 4 to 6 , Theorem 5 , Corollary 1 , Proposition 7
Table 1: What the hypothesis of Definition 1 buys, and where each result is stated and proved. Each computation behind a row has an executable check, named in a source comment in its section or held by the claims gate; the outside lemma and the collapse proposition are proofs alone.
Figure 1: The landscape the hypothesis draws. Verification is strictly weaker than scanning, and the frontier between them is decidable. Every policy with a non-regular domain, the exhibited context-free segmentation among them, is provably outside. The theorems hold on the whole middle region, which is exactly the rational segmentation policies.
DictionarykkKeptRecoveredAnchors per KiBGap p99Longest stretch
  exacttest exacttest  
JSONbase1,174  482.4   
 11,1681,13236480.1476.417 / 1722 / 22
 21,1621,06894478.0462.817 / 1722 / 24
 41,152969183472.2428.217 / 1722 / 24
 81,136799337461.9365.920 / 2130 / 32
Table 2: Base certificates of a dictionary of 64 merges that survive its next kk merges, decided three ways, by the composite decision, the exact lift and the compatible-token test; the first two agree on every certificate and share the column exact, and test is the compatible-token test. Kept counts the surviving certificates of the frozen inventory and recovered those the lift keeps that the test discards; anchors per KiB, the 99th-percentile gap between consecutive anchors and the longest anchorless stretch, both in bytes, are measured on the held-out evaluation slice, exact against the test where a cell holds two figures, and the base row has no extension to compare. The JSON dictionary is trained on the corpus; the GPT-2 dictionary is the first merges of the GPT-2 table, whose space-led merges begin at k=8k=8 .
More in this topic

Tokenization

See all 47 papers

Explore similar work

CardsList
Sep 28, 2026

LatentSift: Policy-State Filtering for Token-Efficient Verification of Software Engineering Agents

Test-time scaling improves software engineering agents by generating multiple candidate trajectories and selecting the best one. Verifying and selecting among these long interactions can consume as many tokens as generation itself. Existing hybrid workflows first apply an LLM-based execution-free (EF) verifier to filter candidates before running tests, which adds another model pass over every trajectory. We introduce LatentSift, a token-free and execution-free filter that replaces this first stage with hidden states the policy already produces while generating the candidates. It represents each candidate through its reasoning, observation, and function-call states, compares them with positive and negative banks of such states collected from successful and unsuccessful trajectories during policy training, and fuses the resulting distance scores with a learned linear score to retain promising candidates for the execution-based stages. On SWE-bench Verified, across three agents and two policy sizes, LatentSift cuts EF-verifier tokens by 66.6--81.0% and total verification tokens, which include test generation, by 49.1--62.1% at K=16, while hybrid Best@16 matches or improves on each agent's reference workflow, rising from 59.26% to 60.06% on DeepSWE-Preview.

Yuning Han, Yangchenchen Jin, Tyler Jandreau +1

University of Florida · Aeronix

Software Engineering AgentsLLM Agent Verification
AskPDF
Sep 26, 2026

The Price of Token Boundaries: Compression Certificates and Prediction

Pre-tokenisation restricts which text fragments can become prediction units, but its compression cost is obscured when tokenisers are compared only under the same boundaries. We measure this cost by bounding the minimum token count from both sides, with and without a regular-expression boundary rule. Nonnegative prices on token occurrences yield a lower bound through shortest paths and vocabulary-budget selection; maximising over all prices recovers the linear programming relaxation, and an independent integer checker certifies the reported values. On English Wikipedia, boundaries increase the optimal token count by 28.3--36.8%. Byte pair encoding lies 2.1% above the constrained lower bound, but 10.9% above the unrestricted bound. Compression and prediction favour different dictionaries: at 85M non-embedding parameters and matched training-token budgets, unrestricted fitting yields higher mean held-out bits per byte under a common unrestricted decoder in all 12 languages in the paired study and 11 of 12 under independent tuning and evaluation. To study intermediate boundary policies, we introduce boundary licences, which limit the vocabulary entries permitted to cross cuts and admit the same form of certificate. On separate English and Chinese fitting corpora, licensing 10% of the vocabulary budget recovers 85.2% and 100.0% of the achieved token-count reduction from removing all cuts. These results quantify the compression cost of boundaries while separating it from the prediction quality of the resulting token units.

Yuhao Du, Shunian Chen

The Chinese University of Hong Kong, Shenzhen · Shenzhen Loop Area Institute

Token CompressionToken EfficiencySubword TokenizationNext-Token Prediction
AskPDF
Mar 25, 2026

Tokka-Bench: Evaluating Tokenizers Across 100 Natural and 20 Programming Languages

Large language models rely on subword tokenizers whose quality varies across languages, yet no standardized multi-metric framework exists for broad comparative evaluation. We introduce Tokka-Bench, an open-source framework that evaluates tokenizers on five complementary metrics -- bytes per token, unique token coverage, subword fertility, word-split rate, and vocabulary composition -- across 100 natural languages (30+ scripts) and 20 programming languages, using language-aware segmentation adapted to each writing system. Comparing seven BPE tokenizers (GPT-2, GPT-4, gpt-oss, Llama 3.1, Gemma 3, Qwen3, and Kimi K2) within individual languages, we find that vocabulary allocation strategy matters more than raw vocabulary size, and that programming-language efficiency has converged among recent tokenizers despite divergent natural-language profiles. The framework, data, and interactive dashboard are publicly available.

Ben Gubler

Tokenization in Language ModelsTokenizationSubword Tokenization
AskPDF