北大华为联队夺冠：形式化数学竞赛33支队伍角逐，国产大模型啃下形式化证明硬骨头

Lean说的都队 投稿 量子位 | 公众号 QbitAI 当大语言模型在数学推理中频频出现"幻觉"，如何让AI的数学证明像人类数学家一样严谨可靠？ 这个困扰AI研究界多年的难题，在近日落幕的CCF"面向大模型的形式化数学竞赛"中找到了突破性答案。 一支名为"Lean说的都队"的联合队伍从33支参赛队伍中脱颖而出，以总分第一的成绩斩获冠军。这支北大华为的联合队伍，凭借华为 openPangu-Ultra-MoE-718B和创新的技术架构，在形式化数学推理这一"AI硬骨头"上实现了重要突破。 权威赛事：瞄准大模型的数学"硬伤" 这项由中国计算机学会主办、蚂蚁数字科技等多家知名机构支持的竞赛，旨在解决大模型在数学推理中的核心痛点——"幻觉"和不可靠问题。 作为CCF大数据与计算智能大赛 （CCF BDCI） 的重要组成部分，该赛事吸引了来自全球的33支顶尖团队参与。 与传统数学问答不同，竞赛要求参赛模型将自然语言描述的数学问题，直接转化为能被计算机验证的形式化证明代码 （Lean/Litex） ，整个 过程禁止使用任何自然语言解释。这相当于要求AI既要是数学家，又要是程序员，既要理解数学问题的本质，又要用严格的编程 ...