对谈 DeepSeek-Prover 核心作者辛华剑:Multi Agent 天然适合形式化数学 |Best Minds
海外独角兽·2025-06-12 21:27
嘉宾:辛华剑 访谈:penny Era of Experience 这篇文章中提到:如果要实现 AGI, 构建能完成复杂任务的通用 agent,必须借助"经验"这一媒介,这里的"经验"就是指强化学 习过程中模型和 agent 积累的、人类数据集中不存在的高质量数据。 强化学习是 AGI 的关键解法。从 OpenAI o1 到 DeepSeek R1,我们不断在看到强化学习的潜力:DeepMind AlphaProof 被认为是"经验时代"初露端 倪的一个例子,作为第一个在 IMO 获奖的 AI,AlphaProof 借助 RL 算法自行"做题",积累经验,AlphaProof 的案例表明,在像数学这样人类高水 平知识接近极限的领域,RL 通过互动试错可以突破瓶颈,取得超人类的成果。 以 AlphaProof 为开端,整个数学证明领域也在最近半年迎来了 AI 突破的密集期:除了 AlphaProof ,OpenAI 的 o1 模型在数学推理上展现出了惊 人表现,DeepSeek-Prover 三部曲也在形式化数学证明上不断创造新纪录。 为了理解数学和 AGI 的关系,海外独角兽访谈了 DeepSeek-Prov ...