UCLA 博士用 LLM agent 63 天产出 12.6 万行 Lean 4 机检证明
siyan_zhao · x · 2026-10-06
UCLA 末期 CS 博士生 Zhu Yanqiao 公开求职（2026 年下半年入职），并展示其 LLM agent 研究成果：
- RetroAgent（COLM 2026）：让 LLM 在结构化记忆上搜索，规划多步逆合成路线，用可验证奖励的 RL 训练。
- FormalFlow：多 agent 通过共享仓库、CI 和代码评审协作做自动形式化，63 天内生成了 MIP = RE 核心定理的完整 Lean 4 机检证明，约 12.6 万行，还修复了原发表表述中的两处错误。
- ARLArena（ICML 2026）：agentic RL 训练平台。
作者将于 10 月 5-9 日在旧金山 COLM 2026 现场。
「编程与Agent」频道最新
- Google 发布两级 agent 记忆架构,token 开销可省 70% — rseroter · 2026-10-06
- Compound 用 AI 重写 Rust 版 Office:称渲染性能超 Google Workspace — peterjliu · 2026-10-06
- Thinking Machines 开源 Prompt Distillation 配方:把长提示词炼进模型参数 — TheZachMueller · 2026-10-06
- Claude 可直接加入 Slack 群聊,像同事一样在串里跟进对话 — maxleiter · 2026-10-06
- 自研插件把 opencode 上下文从 10.3k 压到 1.3k tokens — laerciosantana · 2026-10-06
- 一条命令开启远程调试：像 Debug 网页一样调试 Codex Mac 客户端 — dotey · 2026-10-06