Tokenization with Formal Guarantees: From Optimal Compression to Provable Bounds

Tokenization maps text into sequences of tokens from a fixed vocabulary and is a core component of modern NLP pipelines. Recent complexity-theoretic work formalizes tokenization as selecting tokens that optimize a compression objective over a corpus, and shows that computing an optimal solution is NP-complete. This shows that widely used tokenization methods such as Byte-Pair Encoding (BPE) are inherently heuristic and do not guarantee optimality. While this line of work has largely remained theoretical, Lim et al. recently took a practical step by introducing a mixed-integer programming (MIP) formulation and a greedy approximation algorithm for this objective. However, their MIP formulation suffers from a parameter explosion that makes it impractical for modern solvers such as Gurobi, while the greedy algorithm provides no optimality guarantee. In this work, we introduce a new *graph-flow MIP formulation* for tokenization that substantially reduces the number of decision variables and constraints, making optimal compression-based token selection tractable for state-of-the-art solvers. This enables, for the first time at this scale, the computation of *provably optimal* compression of token vocabularies for large corpora. To further improve scalability, we introduce a *Lagrangian relaxation* based on a shortest-path selection formulation. Our experiments show that our exact MIP algorithms achieve provably optimal compression and substantially outperform existing compression-based tokenization schemes, even on corpora with millions of candidate tokens. Moreover, our Lagrangian relaxation scales to significantly larger corpora, substantially improving over the state of the art in compression, and providing *provable upper and lower bounds* on the optimal value. Overall, this work takes a significant step toward turning optimal token selection from a theoretical objective into a practical algorithmic tool for building highly compressed vocabularies for real-world data.