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

4 月 30 日，DeepSeek在 AI 开源社区 Hugging Face 上，发布名为 DeepSeek-Prover-V2-671B 的新模 型。 这是一款专注于形式化数学推理的开源大型语言模型。 数学推理长期以来被视为AI的"终极挑战"之一。形式化数学不仅是AI的"智力试金石"，更是打开高价值商业场 景的钥匙。DeepSeek-Prover系列模型通过结合LLM的泛化能力与形式化工具（如Lean），首次实现了从自 然语言描述到机器可验证证明的大规模端到端转化。这一突破不仅可能将数学研究效率提升数倍，更将为AI在 金融建模、芯片验证、密码学等依赖数学严谨性的领域打开新可能性。 5月9日，DeepSeek前成员辛华剑，也将参加剑桥大学中国人工智能协会、锦秋基金、清华大学学生通用人工 智能协会、清华大学学生创业协会合作的"大模型开发者与AI基金合伙人的跨洋对谈活动"。他将进行《大语言 模型时代的形式化数学革命》的主题分享。 辛华剑现在是爱丁堡大学人工智能博士生、字节跳动研究实习生，专注于大语言模型在数学定理证明中的创新 应用。他在DeepSeek实习期间主导开发了专注于数学证明DeepSeek-Prove ...