论文精选
Lean 形式化验证的分词器管线原型：消除训练与推理的消息不一致
精选理由
RL 跑崩很多时候是 Jinja 模板在训练和推理时不一致，Sasha Rush 用 Lean 验证 Rust 管线来根治这个问题，做 RL 的人可以看看。
Sasha Rush 提出 Lean Verified Tokenizers，针对 RL 训练中训练端与推理端消息构建不一致导致运行失败的问题。目前聊天模板通常用 Jinja 构建，缺少形式化保证。该项目用 Lean 对 Rust 实现的 agent 管线进行形式化验证，保证消息处理逻辑与训练时一致。目前为原型阶段，代码已开源。
原文 · Sasha Rush
Lean Verified Tokenizers (https://t.co/sX4zCF4C9y)
Training-inference mismatch kills RL runs, but yet we build messages in Jinja? Prototypes a Lean-verified Rust agent pipeline. https://t.co/VCoEU5Z18n
