L3M：可验证自扩展Agent运行时

Carson Eisenach 等作者发布论文，提出 L3M——一个用 Lean 4 编写的智能体运行时。它把人类、智能体、模型与代码的状态全部存入 Git，使等待、通信、委派与撤销成为原语，并支持状态轨迹的恢复、回退、分叉、比较与合并。 作者称，在 Terminal-Bench 上，未经调优的 L3M 仅使用安全（无需人工审核）工具，即可达到其配备 shell 的不安全版本通过率的三分之二左右。

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。