数学小站

唠唠闲话

代码复现

根据 AIMO 的规则，参赛队伍必须公开其代码、方法、数据和模型参数。作为第一届获胜者，Numina 团队开源了完整的训练代码、数据集及微调后的模型参数，以及最终求解问题的代码，确保工作完全可复现。此外，Numina 还在 HuggingFace 平台上托管了一个可以在线运行的推理服务（不过该服务目前挂了）。

环境准备

GitHub 代码地址：project-numina/aimo-progress-prize。

项目的代码库组织如下：

1
2
3
4
5
6
7
8
9
10
11

aimo-progress-prize/
├── LICENSE
├── README.md               <- 开发者使用此项目的顶级说明文档
├── images
├── kaggle-solution.ipynb   <- 用于 Kaggle 提交的推理代码
├── requirements.txt        <- 项目依赖项
└── training
    ├── configs             <- 训练的超参数配置文件
    ├── numina              <- 项目源码
    ├── quantization.py     <- 使用 AutoGPTQ 量化模型的脚本
    └── sft.py              <- 微调模型的脚本

创建 Python 环境，并安装相关依赖：

1
2
3
4

conda create -n aimo python=3.10 && conda activate aimo
# cd <repo>
pip install -r requirements.txt
python -m pip install flash-attn --no-build-isolation

模型训练

Numina 的模型训练分为两个主要阶段，每个阶段都采用 DeepSpeed ZeRO-3 协议进行模型分片，并使用 8 个具有 80GB 显存的 GPU 进行全量微调。

1. 第一阶段：使用 NuminaMath-CoT 数据集对 DeepSeekMath-Base 7B 模型进行 SFT（监督微调），得到模型 NuminaMath-7B-CoT ：

   1	accelerate launch --config_file=training/configs/deepspeed_zero3.yaml training/sft.py training/configs/stage-1-cot.yaml

2. 第二阶段：在 NuminaMath-TIR 数据集上对第一阶段的 SFT 模型进行进一步微调，学习工具集成推理（Tool-Integrated Reasoning），最终得到一个能够结合语言推理和 Python 代码执行的 “推理代理” 模型 NuminaMath-7B-TIR ：

   1	accelerate launch --config_file=training/configs/deepspeed_zero3.yaml training/sft.py training/configs/stage-2-tir.yaml

3. 后处理量化：优化模型在 Kaggle 的 T4 GPU 上的运行效率，Numina 对模型进行了 8-bit 量化，使用 AutoGPTQ 降低计算资源需求。

   1	python training/quantization.py --model_id AI-MO/NuminaMath-7B-TIR --calibration_dataset data/NuminaMath-TIR

该模型不支持 Inference API 不能白嫖 HuggingFace 的 GPU 资源，可以在本地用 vLLM 运行，启动脚本：

1
2
3
4

python -m vllm.entrypoints.openai.api_server \
--model /sshfs/pretrains/AI-MO/NuminaMath-7B-TIR \
--trust-remote-code --tensor-parallel-size 1 --served-model-name tgi \
--max-model-len 4096

模型推理

使用 vLLM 推理。

解构代码，我们用 API 替代。

分两个部分，一个是 sample 的数目，一个是执行代码的轮次。

Gradio 演示

官方提供了演示 Demo：https://huggingface.co/spaces/AI-MO/math-olympiad-solver

该托管服务已经删除了。我们重写一个 Gradio 服务。

示例测试。

探讨了 Numina 在第二届 AIMO 竞赛中的技术方案，包括模型微调和推理算法。在数据集方面，Numina 开源了多个数据集用于模型的微调和验证，开放了微调各阶段的模型参数。Numina 取得最佳成绩的关键因素在于其**高质量的合成数据集**，其次是精心设计的微调技术和推理策略的选择。

SciBench，一个基准套件，用于评估 LLMs 解决大学水平科学问题的能力。

OpenAI o1-preview 展示了其在 IMO 问题上的解题能力。虽然得出了正确答案，但证明不完整。本文将对其解题过程进行简单的分析。

数学竞赛大致分为两类：一类面向高中生，例如国际数学奥林匹克竞赛（IMO）及相关选拔赛；另一类涵盖本科以上知识，如全国大学生数学竞赛和阿里巴巴数学竞赛等。IMO 作为高中生数学竞赛的巅峰赛事，由于背景知识需求相对较少，成为了测评 AI 能力的绝佳试金石。

由于 LLM 的幻觉问题，数学形式化——这一消除幻觉确保论证严谨性的手段——受到了很多关注。按照陶哲轩的说法，形式化是在前严谨阶段到严谨阶段的过渡，能避免常见错误和消除误区。然而，数学真正具有创造力和生命力的地方在于后严谨阶段。在这一阶段，研究者在已经掌握严谨理论基础的情况下，开始建立和形成数学直觉。如果 LLM 能够在后严谨阶段发挥其作用，那么它很有可能会真正引起数学学术界的广泛重视。

在数学研究领域，计算推导是不可或缺的一环。从上世纪 60 年代开始，数学家就开始使用计算机辅助发现模式和猜想。如今，专业的数学编程语言，如 Mathematica，Maple，SageMath，GAP4 等，应运而生，极大地拓展了人类的计算能力。这些语言使我们能够完成传统手算难以实现的任务。在 LLM 快速发展的时代，编程任务可以通过 AI 辅助更轻松地完成。我们将在无需自己编写代码的情况下，借助 LLMCoder 来辅助对问题的探索思考。

SageMath 简介，开发版的安装教程。

Lean 定理证明器的 Python 交互库，支持 Lean 3 和 Lean 4。

深入了解 Lean4Game 教程，学习如何开发游戏，构建丰富的互动学习体验。