计划231128

比赛

AI-MO Prize AIMO Prize是独立运行的，它并不正式属于国际数学奥林匹克竞赛（IMO）或国际数学奥林匹克竞赛大挑战（IMO Grand Challenge）。

规则:the AI receives a formal representation of the problem (in the Lean Theorem Prover), and is required to emit a formal (i.e. machine-checkable) proof.

• 关于格式。为了确保证明过程的严谨性和可验证性，问题和证明都需要通过形式化（formal，机器可验证）的方式来完成。LEAN语言
• 关于得分。AI的每个证明题都会在10分钟内被判断对错，因为这也是IMO裁判评分的时间。与人类不同，AI没有“部分得分”这一说法。
• 关于资源。和人类一样，AI每天需要用4.5小时解决3道题（共比赛两天），计算资源没有限制。
• 关于可复现性。AI必须开源，并在IMO第一天结束前公开模型、而且可复现。要求AI不能联网。

  接近的研究

• Exploring the MIT Mathematics and EECS Curriculum Using Large Language Models
  • 已被证实是数据集收到污染，最终只能达到65%的准确率。但是文章有很多调教大模型的小技巧。
  • 被撤稿，目前网上找不到

问题

• 时间计划（最近一次比赛是在2024.7，是否参加）
• 实现原理
• 编程语言和编译器：主python pycharm/VS code
• 训练时的服务器租赁

有用的

• 大模型版“5年高考3年模拟”来了！6141道数学题，还是多模态的那种｜微软&UCLA&UW联合出品
• Solving Challenging Math Word Problems Using GPT-4 Code Interpreter with Code-based Self-Verification 在MATH数据集上最高的准确率

工具

• github
• GPT
• VS code
  • 插件

数据集

• MATH

• MathPile

  规则更新12.19 2023

• 对于首次的进步奖，竞赛参赛作品只能使用在2024年1月1日之前开放源代码并可用的AI模型和工具。例如，编程语言如Python和Lean，以及具有公开可用权重的语言模型，如Llama。这将确保公平性，防止使用在私有数据集上训练并仅在竞赛期间发布的模型。

12月草稿

1月底回深圳的家-2.24 1.1前 ZB毕设 VAN 1.3-1.4 1.5 当天 每周找一天开

最终规则 24.3.14

• 提交答案时间3.16中午十二点到 3.17中午十二点
• prompt注意格式问题
  • 回答以latex格式
  • 提交以json格式
  • Answers should be expressed solely as numerical values or LaTeX. If the decimal can be calculated to be finite, please provide the exact answer. If the output answer is an infinite decimal, it should be rounded to four decimal places.
  • 最终答案相当简短

思路

底层基础大模型

• 借用API
• 自己部署模型
  • 模型种类：剩下的时间肯定可以布置7B的，
    • 8x7B的文件大小在180G，利用flash attention2 可以在24GB的GPU上加载 2h30min 可以下载完毕
    • 7B在30G，下载速度20M/s，25min下载完成

单用模型不够创新，再使用较为前沿的CoT技术

• CoT 提示学习（ZB）
• 分解法，将大问题拆解成小问题。涉及符号操作时分解法强于

以下方法来源 大语言模型的数学之路

• 自验证（self-verification）（VAN）
• Majority Voting（self-consistency） （HJS）
• OPRO （HJS）
• %% 让大模型学会调用python %% （实现起来难度较大）

api 部署模型 def abc （model，） output = model（input）

This line appears after every note.