赛事与成果概述 - 中国计算机学会主办的“面向大模型的形式化数学竞赛”旨在解决大模型在数学推理中的“幻觉”和不可靠问题[2] - 赛事吸引了来自全球的33支顶尖团队参与，参赛人数超过600人[2][6] - 一支名为“Lean说的都队”的北大华为联合队伍以总分57.21分获得冠军，从33支队伍中脱颖而出[1][6] 竞赛任务与意义 - 竞赛要求模型将自然语言描述的数学问题直接转化为能被计算机验证的形式化证明代码，禁止使用自然语言解释[4] - 赛题是对大模型形式化推理能力的系统性检验，为未来构建可信赖的大模型提供技术路径和评估基准[6] 冠军团队成绩 - 初赛阶段：正确解答181道题目（共220道），初赛分数82.27分[6] - 决赛阶段：正确解答5道高难度题目（共50道），决赛分数10分[6] - 方案评审：技术方案获得87分的高分[6] - 最终总分：57.21分，位列榜首[6] 核心技术：openPangu大模型 - 团队采用华为openPangu-Ultra-MoE-718B作为核心模型之一，总参数量达7180亿，激活参数量390亿[9] - 该模型在形式化数学推理任务中展现出强大的语义理解能力和形式化表达能力，尤其在数论和代数问题上性能强劲[9] - 实测表明，该模型在Lean语法检查通过率方面与国际前沿的Gemini 2.5 Pro和GPT-5模型表现相当，在形式化命题的可证明命题比例方面更具优势[10] 创新的混合式系统架构 - 系统采用协同式求解系统，结合大模型的形式推理能力与专用证明器的高效性[7] - 核心特点包括动态切换策略：先尝试流水线方法，失败则回退到单体模型方法[13] - 建立了多层质量检查体系，包括语法验证和严格的语义对齐检查[14] - 采用多模型协同，根据模型的知识边界和成本效率进行智能调度[14] 关键技术创新：语义分解验证 - 团队创新性地引入了基于语义分解的多层级验证机制，将自然语言问题解构为数据类型、前提条件和证明目标三个正交维度[16] - 该方法解决了传统LLM-as-a-Judge方法“判定过松”的问题，实现了从整体模糊匹配到结构化精确对齐的范式转变[16][17] - 相比传统方法，这一改进显著降低了误判率，为形式化结果的可靠性提供了保障[19] 技术应用与实战案例 - 案例一（抽象代数）：成功处理环的整扩张与幂零根相关的命题，生成了严谨的Lean代码[20] - 案例二（复数计算）：成功处理求满足复数方程实数个数的问题，展示了拆解子问题与生成完整证明的能力[22] 当前局限与未来展望 - 现有证明器主要在高中竞赛题目上训练，对微积分、代数几何等高度专业化数学分支的掌握仍显不足[23] - 单题平均约1小时的求解时间限制了在时间敏感场景下的应用[23] - 未来建议通过主动学习构建专门化证明器，探索动态采样策略，并关注人机协作的交互式证明模式[23] 行业影响与意义 - 此次突破为中国在AI形式化推理领域赢得了荣誉，为攻克严谨数学证明这一“最后堡垒”提供了可行的技术路线[31] - 随着openPangu等国产大模型的持续进化，AI有望在数学研究、科学发现、教育辅助和软件验证等领域扮演更重要角色[31]