# 6.llm\_math

## LLM+math

### mathscale

[【LLM-数学】MathScale 用于数学推理的指令调优扩展方法](https://mp.weixin.qq.com/s/tQUIGdViMZTb_9NNh3b3RQ)

[MathScale: Scaling Instruction Tuning for Mathematical Reasoning](https://arxiv.org/pdf/2403.02884.pdf)

### AlphaGeometry

[奥数能力金牌级：DeepMind几何推理模型登上Nature，代码开源，菲尔兹奖得主点赞](https://mp.weixin.qq.com/s?__biz=MzA3MzI4MjgzMw==\&mid=2650904746\&idx=1\&sn=d39a3d92078cecbd29bd0fc82560d1da\&chksm=84e45cd4b393d5c24747f163fa0338761690447904a1a654aacf2344d7a16d36dfa2ac3ccdb0\&scene=21#wechat_redirect)提出了AlphaGeometry

### AlphaProof & AlphaGeometry 2

[谷歌AI拿下IMO奥数银牌，数学推理模型AlphaProof面世，强化学习 is so back](https://mp.weixin.qq.com/s/LNzbyf0w412BIz71sROyzw)提出AlphaProof和AlphaGeometry 2

### WE-Math基准

[真相了！大模型解数学题和人类真不一样：死记硬背、知识欠缺明显，GPT-4o表现最佳](https://mp.weixin.qq.com/s/uU1lZV0Ymj31cmZryhffyQ)

[WE-MATH: Does Your Large Multimodal Model Achieve Human-like Mathematical Reasoning?](https://arxiv.org/pdf/2407.01284)

<https://github.com/We-Math/We-Math>

<https://huggingface.co/datasets/We-Math/We-Math>

### case-based or rule-based

[ICML 2024｜Transformer究竟如何推理？基于样例还是基于规则](https://mp.weixin.qq.com/s/aVRiGW3xU_LpvxZzjDpwzQ)

[Case-Based or Rule-Based: How Do Transformers Do the Math?](https://arxiv.org/pdf/2402.17709)

<https://github.com/GraphPKU/Case_or_Rule>

## AlphaProof(nature)

[Olympiad-level formal mathematical reasoning with reinforcement learning](https://www.nature.com/articles/s41586-025-09833-y)

[代码](https://github.com/daiwk/collections/blob/master/assets/alphaproof_pseudocode.py)，从<https://www.nature.com/articles/s41586-025-09833-y>这里的Supplementary Data下载

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-eca2580e5245b84b5327040306d561a5acbe98f3%2Falphaproof1.png?alt=media)

* 状态：Lean prover的逻辑状态，即Lean tactic state，表示已经建立的假设，和剩下的目标
* 环境：给定一个状态，和agent采取的动作，输出下一个状态
* 动作：一个证明的中间步骤，是一段文本，例如“a=2,b=2a,==>b=4”
* episode结束条件：证明完成or预算花完（例如超时）
* reward：每个tactic的reward都是-1，因为要鼓励用更少的步骤完成证明，即到达终点的分支路径最短

prover agent是把dnn和alphazero的搜索算法相结合：

* proof network：是一个3B的encoder-decoder transformer，输入Lean tactic state，输出2个东西：
  * policy：下一步要尝试的N个动作
  * value：当前**状态**的价值，即从此刻到episode结束时的每步reward之和
* tree search：和alphazero类似，使用AND-OR tree structure将证明拆成多个独立的子目标(类似[Hypertree proof search for neural theorem proving](https://arxiv.org/pdf/2205.11491))，采样使用的progressive sampling

![](https://1725978874-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-MAwALUwRCP16VZ2I1KP%2Fuploads%2Fgit-blob-cadb95a82883b687c76c5f542abd0b84b01f85b1%2Falphaproof2.png?alt=media)

* 预训练：proof network在大概300 billion tokens的代码和数学语料通过next token prediction预训练
* SFT：在300k的人类用matlab标注的证明语料(state-tactic pairs)上sft，
* main RL：
  * 用gemini的LLM搞了一个自动形式化（formalization）的系统，将大概1M的非形式化的问题形式化成了80M的问题
  * proof network+tree search和Lean环境交互，生成形式化的证明和反证（disproof），然后用Alphazero的方式基于得到的经验去RL训练
* inference：
  * 首先参考Alphazero，增加tree search的预算，例如产生更多的搜索路径
  * 如果增加了搜索路径还不够，那就用Test-time RL（TTRL）：
    * 给定一个问题，variant generator生成其变种（例如简化或者泛化）
    * 基于这些变种去进行RL训练