srush 用 Lean 形式化验证 tokenizer,根治 RL 训练-推理不匹配 bug
srush_nlp · x · 2026-10-28
Princeton 研究者 Sasha Rush(srush)发布博客《Lean Verified Tokenizers》,提出用 Lean 形式化验证的 Rust tokenizer 流水线来消除 agent 训练中的一类顽固 bug。
问题背景
- Agent 通过结构化消息(system/user/assistant/tool)控制真实系统,而消息在 messages、bytes、tokens 三种表示间转换时,decode 再 re-encode 并不保证恢复原 token 序列。
- 预训练和 SFT 用固定 token 序列不受影响,但 RL 需要实时与工具交替运行推理,这种不匹配会直接毁掉 RL 训练——而目前大家还在用 Jinja 模板拼接消息。
方案
- 受 No Tokens Left Behind 与 GitHub BPE 博客启发,作者原型化了一条经 Lean 证明的 agent tokenizer 流水线(代码开源:srush/certified-tokenizer)。
文章还回顾了消息渲染器的演化,如早期每次添加用户消息都会改变所有历史 assistant 消息的渲染(如移除 thinking 块),渲染器甚至允许任意全局 Python 代码,进一步加剧不确定性。
所属事件:srush 用 Lean 形式化验证 tokenizer 与 LLM 代码(2 条相关)→
「编程与Agent」频道最新
- 开发者用 AI 审计自己 C 代码后：不再信任未经 AI 审查的代码 — burny_tech · 2026-10-28
- Snowflake 押注 Agentic RL：先过拟合再扩展，Qwen3.5-9B 提至 65.7 — StasBekman · 2026-10-28
- 微软 Anthropic OpenAI 齐转向 Hook 级 Agent 安全,实时拦截工具调用 — jacob_posel · 2026-10-28
- 开发者把 Claude SSE 流改造成 Agent 调试「法证时间线」 — Additional-Ladder-24 · 2026-10-28
- Supabase 推出 Compute 私测:Agent 与长任务可与 Postgres 数据同项目运行 — dshukertjr · 2026-10-28
- 营销从业者预判：2027 年 Agent 大众化，普通人无需自己搭建 — tjrobertson-seo · 2026-10-28