🏆 **竞赛背景与目标**：由中国计算机学会主办的ForMaLLM竞赛，旨在解决当前大语言模型在数学推理中存在的“幻觉”和逻辑不可靠问题。通过要求模型将自然语言数学问题转化为形式化语言证明代码，竞赛致力于提升AI的严谨性、可验证性和可审计性，推动AI向“可验证AI”迈进。

💡 **核心任务与技术要求**：竞赛的核心在于开发一个全自动解题系统，该系统接收自然语言数学问题后，需端到端地将其转化为使用Lean或Litex语言编写的、可被官方编译器独立编译和验证的证明脚本。此过程强制模型进行精确的逻辑表达和形式化建模，完全摒弃自然语言解释。

🚀 **重要意义与影响**：ForMaLLM竞赛不仅为评估大模型在形式化逻辑、数学结构建模和自动定理证明方面的能力设立了新的量化基准，还系统性地检验了模型处理归纳证明、存在量词等高阶数学推理任务的极限，为构建可信赖的AI推理系统提供了重要的技术路径。

💰 **激励机制与参与方式**：赛事设立总奖金10万元人民币，以丰厚激励吸引全球顶尖团队参与角逐。所有全球开发者和研究人员均可通过中国计算机学会（CCF）的比赛平台报名参赛，获取更多赛事信息。

52CV 2025-10-27 14:48 江苏

2025年10月20日，由中国计算机学会主办，蚂蚁数字科技和中国计算机学会大数据专家委员会联合组织，上海人工智能实验室、复旦大学、香港中文大学賽馬會「AI4SE」創科實驗室、新加坡科技局及Litex社区共同支持的“面向大模型的形式化数学竞赛”（Formal Mathematics Competition for Large Language Models, ForMaLLM）正式拉开帷幕。赛事设立总奖金10万元人民币，以丰厚激励推动跨学科创新与更高标准的形式化验证，吸引全球顶尖团队同台角逐。这一开创性赛事标志着人工智能在数学推理领域迈入一个追求严谨性、可验证性与无歧义性的新阶段，同时以实质性奖励加速大模型在严谨数学场景中的落地与突破。

随着大语言模型（LLMs）在自然语言处理和数学问答任务中取得显著进展，其在解决GSM8K、MATH等数据集上的表现令人瞩目。然而，这些系统的推理过程大多依赖于自然语言生成，存在“幻觉”、逻辑跳跃和推导不可靠等根本性问题，输出结果难以被机器自动验证。

ForMaLLM竞赛的设立，正是为了解决这一关键瓶颈。它要求参赛模型将自然语言描述的数学问题，端到端地转化为完全使用形式化定理证明器语言（Lean或Litex）编写的、可被计算机独立编译和验证的证明代码。这一过程摒弃了任何自然语言解释，强制模型进行精确的逻辑表达和形式化建模。

该赛事的意义重大：

ForMaLLM竞赛的核心任务是开发一个基于大模型的全自动解题系统，其工作流程如下：

全球开发者和研究人员均须通过中国计算机学会（CCF）的比赛平台（https://www.xir.cn/competitions/1143）报名参赛，获取更多信息。