Cohere Labs 开讲：用 Lean 形式化验证让 AI 数学推理可机器检验
Cohere_Labs · x · 2026-10-02
Cohere Labs 的 ML Math 开放科学社区将于 10 月 5 日（周一）举办线上讲座，由 Robert Joseph George 主讲「为数学与科学构建可信 AI」。
核心内容：
- 介绍 Lean 与形式化定理证明，如何用形式化方法让数学与计算推理变得机器可检验；
- 介绍 TorchLean 框架：在 Lean 中做经验证的机器学习，涵盖神经网络执行、自动微分、浮点语义与神经网络验证；
- FloatLib：经形式化验证的浮点算术工作；
- AI 与计算在数学难题上的进展，包括 Navier–Stokes 与 Euler 方程相关进展，以及作者在 3D Euler 方程奇点形成与稳定性上的工作。
主线是探讨 AI、数值计算与形式验证如何共同成为数学发现的工具，让 AI 输出可被独立核查而非仅被信任。
「研究」频道最新
- Gumbel Straight Flow：把自回归模型蒸馏成单步流映射并行采样 — sedielem · 2026-10-02
- 假说:人类学习也是爬山算法,难验证任务对 AI 并非相对更难 — Afinetheorem · 2026-10-02
- Google 新一代联邦学习:TEE 实现可验证差分隐私并提速训练 — gaganghotra_ · 2026-10-02
- 印度裔科学家 Anima Anandkumar 谈让 AI 理解物理 — nordicinst · 2026-10-02
- 量子优化 25 分钟解决药物发现难题,经典求解器 3 小时仍差 40% — MJBiercuk · 2026-10-02
- AI2 开源 AstaBrief 8B:研究问题一键生成带引用报告 — allen_ai · 2026-10-02