FormalMATH团队 投稿 量子位 | 公众号 QbitAI 最强AI模型面对5560道数学难题，成功率仅16.46%？背后真相大揭秘。 香港中文大学、西湖大学、MAP、浙江大学、马克斯·普朗克智能系统研究所等机构联合推出 FormalMATH形式化数学推理基准测试 ，含 5560道经过严格验证的数学题，覆盖从奥数到大学水平的代数、微积分、数论等领域。 形式化数学推理是人工智能领域公认的核心难题之一。 尽管大语言模型（LLM）在自然语言处理和代码生成等领域取得显著进展，但面对需要严格逻辑推导的数学定理证明任务时，其能力仍面临严 峻挑战。 FormalMATH：「超大规模」的形式化数学推理基准 规模突破：22.8倍于现有基准 FormalMATH包含5560个经过Lean4编译器验证的数学命题，涵盖代数、数论、微积分、离散数学等12个子领域，问题难度从国际数学奥林 匹克（IMO）竞赛级延伸至本科课程，规模是经典基准MiniF2F的22.8倍。 构建创新：人类在循环中的自动化流程用于自动形式化和语义一致性检测 为解决传统形式化数据依赖专家手动标注的瓶颈，研究团队提出了一套 「三阶段过滤」 框架： 现有LLM证 ...

DeepSeek-Prover-V2-671B模型发布 - 公司发布专注于形式化数学推理的开源大型语言模型DeepSeek-Prover-V2-671B，参数量达6710亿 [1] - 该模型结合LLM泛化能力与形式化工具（如Lean），首次实现自然语言描述到机器可验证证明的大规模端到端转化 [2] - 形式化数学被视为AI"终极挑战"，突破可能将数学研究效率提升数倍，并打开金融建模、芯片验证、密码学等高价值商业场景 [2] 大模型开发者活动 - DeepSeek前成员辛华剑将参与"大模型开发者与AI基金合伙人跨洋对谈"，分享《大语言模型时代的形式化数学革命》 [2] - 辛华剑为DeepSeek-Prover系列模型开发主导者，现任爱丁堡大学AI博士生及字节跳动研究实习生，专注大模型在数学定理证明的创新应用 [2][4] - 锦秋基金合伙人臧天宇将同期分享2025年AI创投趋势 [3][4] 活动主办方背景 - 锦秋基金专注AI领域投资，在管基金为12年长期基金，59%项目为首次投资，采取多轮追加策略，已投资北美活跃AI基金 [6] - 剑桥中国人工智能协会(CCAIA)致力于链接中国AI产业与海外学界，采用轻量化社群模式促进中英资源流动 [7] - 清华大学学生通用人工智能研究会(THUAGI)以培养下一代通用AI人才为目标，依托清华AI研究院资源 [9] - 清华大学学生创业协会成立于1997年，为全国最早高校创业协会之一，28年来聚焦创业生态培育 [10] 活动流程 - 英国时间15:00/中国时间22:00开始辛华剑主题演讲，随后臧天宇分享AI创投趋势 [8] - 活动含圆桌对谈及观众提问环节，国内通过腾讯会议直播，需通过锦秋基金公众号报名 [5][6][8]