Agent Foundations 论文 Lean 形式化竟发现 Logical Induction 原文一处错误
jessi_cata · x · 2026-09-06
GitHub 上出现 Formalized-Agent-Foundation 项目:对 agent foundations 与理论对齐领域多篇重要论文进行系统化的 Lean 4 自动形式化,覆盖 Logical Induction、Cartesian Frames、Finite Factored Sets、Modal Agents、Condensation、Provability Logic、Shannon Information、PFR 等主题,已积累近千次提交,并配置了 CI 测试与 AxiomAudit 等审计文件。
- Logical Induction 论文共同作者本人转发并确认:形式化过程在「finite perturbations 下的闭包」一条上抓到了原论文的一个错误
- 不过作者表示,修改后的表述仍然成立
这是「用形式化验证反哺理论论文」的一个罕见案例:机器可检验的证明不仅复现了结果,还实际修正了被广泛引用的对齐理论文献,对 alignment 理论研究有参考价值。
「研究」频道最新
- 学者批驳「一年内形式化全部人类数学」计划 — lpachter · 2026-09-06
- DisCo 把 GitHub 仓库蒸馏成技能库,MLE-bench 成绩翻倍至 72.89% — rohanpaul_ai · 2026-09-06
- 南大等提出 Harness 持续学习：基座冻结，智能体靠脚手架进化 — jiqizhixin · 2026-09-06
- ICML 论文：对最后 5 层做 LoRA 超拟合可消除 AI 味 — grimjim · 2026-09-06
- 1000 美元训出 HRM-Text,Sapient 递归架构抢在 Astra 之前押注 — rohanpaul_ai · 2026-09-06
- 熵轨迹形状可预测 Qwen3-4B 出错，并能迁移到未见任务 — Happy_Brilliant7827 · 2026-09-06