婆罗米语脚本的类型驱动标记化

大型语言模型中使用的标准分词器在应用于婆罗米语脚本时会产生格式错误的文本。它们是附标书写系统的一个家族，其辅音带有可以修改从属标记的固有元音。它们包括梵文、泰卢固文、泰米尔文、卡纳达文等。根本问题是这些分词器违反了拼写限制，而这些限制在英语等字母文字中不会出现。我们观察到，英语正字法形成了 \emph{semigroup} （任何两个有效标记都可以自​​由连接），而婆罗米语正字法形成了 \emph{partial semigroup}：并非每个连接都会产生有效的字符串。我们在 Agda 中形式化了这种区别，将有效的婆罗米语标记建模为转换系统中的链，并导出一个可证明正确的 \texttt{fixToken} 函数，该函数扩展任何候选标记以尊重正交边界。然后，我们展示了这种形式推导如何转化为 SentencePiece 的实用补丁以及独立的基于 Rust 的预分词器库，从而消除了在印度语脚本中观察到的错误。