数学小站

欢迎来到 lookeng.cn，博客定位是与数学关联的一切一切，这里是置顶博客，整理已写博文和计划展开的话题，欢迎交流~

我们从数学角度和形式化角度分析了 AlphaProof 的工作。模型技术角度也有许多值得深入研究的内容，如数据合成方式、策略空间的定义、以及采用的搜索算法等，这些我们在 IMO 后续系列中整理介绍。

数学形式化的目的是提供一个**完全客观和可验证的证明过程**，使得任何了解该形式体系的人都能够检查证明的正确性，而不需要对证明本身进行主观判断。由于数学形式化能用于消除模型幻觉，在当下格外受到关注。

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

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

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

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

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

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

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