主要来源Sasha Rush
查看原文事件专题 ·单一信源
Lean 形式化验证的分词器管线原型：消除训练与推理的消息不一致
Sasha Rush 提出 Lean Verified Tokenizers，针对 RL 训练中训练端与推理端消息构建不一致导致运行失败的问题。目前聊天模板通常用 Jinja 构建，缺少形式化保证。该项目用 Lean 对 Rust 实现的 agent 管线进行形式化验证，保证消息处理逻辑与训练时一致。目前为原型阶段，代码已开源。
当前结论
RL 跑崩很多时候是 Jinja 模板在训练和推理时不一致，Sasha Rush 用 Lean 验证 Rust 管线来根治这个问题，做 RL 的人可以看看。
2 个信源31° AI 热度最后更新 2026/10/27 21:42:13
证据链
2 个信源相关来源 1arXiv cs.AI
查看原文冲突核查
现有去重数据只说明这些来源讨论同一事件，不代表立场相同。当前没有结构化的支持或反驳证据，不自动推断冲突。