AGI与强化学习 - 实现AGI需借助"经验"媒介，即强化学习过程中积累的高质量数据，突破人类数据集限制[3] - 强化学习是AGI关键解法，AlphaProof通过RL自行"做题"积累经验，在IMO获奖，展示RL在数学等人类知识接近极限领域的突破潜力[3] - 数学证明领域半年内密集突破：AlphaProof、OpenAI o1模型、DeepSeek-Prover三部曲均展现RL在数学推理上的惊人表现[3] 形式化数学与Agent - 形式化数学用符号化方法建模和验证数学推理，将数学正确性归结为代码编译正确性[20][23] - 当代数学面临"分布式挑战"，研究者间沟通成本高导致工程瓶颈，形式化数学可构建统一知识库实现中心化研究[26][30] - Lean因对前沿数学支持良好、社区活跃成为主流形式化语言，DeepSeek Prover采用后引领领域命名范式[30][34] - 形式化数学天然适配Multi-Agent，Proof Engineering Agent需具备自我规划、修复和知识积累能力，类似软件工程但更抽象[51][52] DeepSeek Prover技术演进 - Prover三部曲进展：V1验证合成数据Scaling效果，V1.5实现自然语言推理引导形式化代码，V2在671B规模实现高层次数学规划[35][37][38] - 数学RL动作空间开放无界，传统RL难以应对，LLM+RL可完成代码/数学等复杂任务[40] - 思维链扩展模型规模效应，Test Time Scaling成为可靠方向，如GPT-o系列投入更多推理预算提升结果[41] 评估与训练范式 - RL有效工作关键在Verification设定，需任务难度略高于模型当前能力，Evaluation比Training更重要[59][60] - APE-Bench基准设计聚焦Proof Engineering，要求模型处理大规模文本修改并与验证系统交互，推动从单任务向工程级能力跨越[62][63] - 合成数据在形式化数学中密集使用，AlphaProof通过问题变形/拆解从100万题扩展到1亿题，Test Time Training接近Online Learning[43][45] Certified AI与泛化 - Certified AI强调生成质量控制，通过形式化验证确保结果可靠性，数学需每一步正确，代码需通过安全性等检测[68][69] - 数学能力泛化依赖领域间共同推理模式，pre-training阶段数据配比和规则筛选是关键，如GPT-3.5因高比例代码数据提升推理[72] - 形式化方法可推广至化学、生物等依赖数理结构的领域，但需补充物理世界交互[73] 未来技术方向 - 下一个GPT-4级跨越将是具备自主规划、执行和反思能力的Agent，结合Online Learning可实现能力持续优化[80] - Reward Model演进为Reward Agent，动态收集信息判断生成正确性，解决复杂评估问题[76][77] - Pre-training仍为技术基础，虽Scaling单独难支撑跨越，但需持续融入Agent等新方法[83][84] 行业竞争格局 - AGI实现者大概率来自现有头部企业（Google/OpenAI/DeepSeek等），因需补足技术/Infra/人才积累，新入局者困难[81] - 技术发展进入积累期，o1模型与4o形成互补而非代际替代，pre-training瓶颈指单独Scaling不足，非整体重要性下降[82][83]