用 LLM 辅助 Lean 形式化策略梯度证明，还真找出了漏洞
fpedregosa · x · 2026-10-08
Fabian Pedregosa 分享用 LLM 辅助写 Lean 4 形式化的体验：为自己策略梯度系列博客做形式化时，发现了几处证明中的细微问题。配套仓库 policy-gradient-lean 已开源。
- PolicyGradientVariance.lean：形式化 REINFORCE 得分函数梯度估计量的 O(T³) 方差上界（任意实 Hilbert 空间）
- 另含 REINFORCE 基线的配套形式化
对想用 LLM + Lean 做机器学习理论验证的人是有参考价值的实践案例。
「编程与Agent」频道最新
- Vibe coding 十大法律陷阱:上线上线前可能先吃官司 — alex_verem · 2026-10-08
- 微软扩展 GitHub Spec Kit：企业级规格驱动开发的分层方案 — WirelessLife · 2026-10-08
- AI Agent 越权泄漏薪酬数据，社区总结上线前五项权限自查法 — Wild-Lawyer8511 · 2026-10-08
- Codex 排障后续：真实复现故障并自行找到 MCP 日志位置 — dfinke · 2026-10-08
- Codex 自主配置 MCP：写 mcp.、起 server、跑基线全包 — dfinke · 2026-10-08
- Understand Anything 爆火:把代码库变成可问答知识图谱供编码 Agent 推理 — JeremyCMorgan · 2026-10-08