Renaissance 资助新项目:让 AI 智能体顺畅驾驭计算机代数系统
ChrSzegedy · x · 2026-11-05
数学研究者 Bartosz Naskręcki 宣布启动「Agentic Approach to Computer Algebra Systems」项目,由 Renaissance Philanthropy 的 AI for Math Fund 2026 资助,由 Adam Mickiewicz 大学与华沙理工大学联合承担,为期两年。
- 要解决的问题:LLM 能流畅提出数学猜想但不保证正确,计算机代数系统(CAS)计算可靠却难以被端到端驱动,而 Lean 证明对模型来说很难直接使用。
- 方案:构建一个开源的 agentic CAS 中间层——LLM 驱动 CAS 在沙箱中执行与自修复,交叉核对结果,再把计算过程固定为机器校验的 Lean 证明,错误结论无法编译。证明捆绑可泛化到 Magma、SageMath、PARI/GP,成为「计算与形式化陈述一致」的可复现机器证明凭证。
- 目标:让数学家在保留纸笔探索灵活性的同时,顺畅地与 AI 智能体和形式化数学协作。
「漫话AGI」频道最新
- 评论：AI 公司的舆论反噬是图像视频语音模型自己招来的 — karmay007 · 2026-11-05
- Neel Nanda 与 tszzl 论模型隐性摆烂: 暗中消极比拒绝更难辩护 — tszzl · 2026-11-05
- 把算力建到太空逃避监管？业内：完全不正经的想法 — zacharynado · 2026-11-05
- Reddit 长文:AI 或永无意识,而这并非坏事 — Own-Cry-5520 · 2026-11-05
- 研究者认为内部护栏难防恶意 AI,主张外部防护机制 — IgorGabrielan · 2026-11-05
- 莱姆科幻被重估:早于 2000 年就写对了会犯错、写诗的成长式 AI — zetalyrae · 2026-11-05