RL 训练暗藏 tokenizer 陷阱：srush 用 Lean 形式化验证修复 tito 问题
VoidAsuka · x · 2026-11-02
背景
reinforcement learning 中存在 tito(token-in, token-out)难题：消息、字节、token 三种表示之间的编解码不是双射——token 解码再编码可能回不到原序列，字节改动还会双向传播影响 tokenization。这在预训练和 SFT 中不成问题(用的是固定 tokenized 表示)，但在 RL 的 rollout 流程里会引发一类隐蔽的训练 bug。
各方进展
- @ChonghanLiu 承认最初以为该问题已被社区和内部团队解决，但细读 srush 的博客后意识到并没修干净：各家设计差异大，社区支持代码高度碎片化、没有标准。他因此向 verl 提交了相关 PR。
- srush 的博客《Lean Verified Tokenizers》 提出用 Lean 形式化验证构建 tokenizer 管线，以缓解 agent harness 中的此类 bug。博客受《No Tokens Left Behind》、Aeneas 文档和 GitHub 的 BPE 博客启发，正文人写、AI 辅助编辑，代码开源于 srush/certified-tokenizer。
核心问题：推理-训练不匹配
Agent 通过结构化消息(工具调用)通信，而消息渲染器允许任意全局 Python 代码(如加入用户消息时改写历史 assistant 消息、剥离 thinking),进一步加剧了不一致。
「编程与Agent」频道最新
- Karpathy 用 Claude 从 43M 条 HN 评论筛出 6454 个好视频做 HackerTube — _arohan_ · 2026-11-02
- 全程用 coding agent 挑战 codevember：附 Claude 生成的 30 个创作题目 — thespite · 2026-11-02
- Meta 与 NYU 论文：简单循环 h1 打平手工定理证明工作流 — rohanpaul_ai · 2026-11-02
- 网友建议 Karpathy 用 PID 控制器聚合 X、Threads、小红书信息流 — xiaosun86 · 2026-11-02
- rakyll 提议将 AX Studio 原型转正为 Google AX 官方桌面应用 — rakyll · 2026-11-02
- YC 新作 Click 发布：一个 API 调用托管任意模型的完整 Agent 栈 — ycombinator · 2026-11-02