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

在CCF“面向大模型的形式化数学竞赛”中，“Lean说的都队”从33支队伍中脱颖而出，以总分57.21分夺冠。该北大华为联合团队依托华为openPangu-Ultra-MoE-718B大模型（7180亿参数），构建了融合自动形式化流水线与大模型直推的混合架构，并创新提出基于语义分解的多层级验证机制，显著提升形式化证明的准确性。系统在Lean语法通过率上媲美GPT-5等国际先进模型，且在命题可证明性方面表现更优。尽管当前在高等数学覆盖和求解效率上仍有局限，成果标志着国产大模型在AI数学推理领域的关键突破。
来源：https://mp.weixin.qq.com/s/L7nQikhOhz3mhPXInOSUAg