尔以前道过道一下math V2的论文，来日诰日去借个愿 实在为何那论文出人重视呢？主要是二个启事： 1- 尽年夜大都人讨厌数教 2- 以前出过一个prover2，各人也没有明白搞啥的也战数教相关，而后又去一个 讨厌数教便没有道了（以至有人讨厌喷鼻菜），主要道第两个，prove2为何让人没有明白是搞啥的？ 它实际上是lean 天生器，您必然会问甚么是lean，现在皆是lean4 lean4 是 MS Research 开辟的接互式定理证实器，一种函数式编程语言 + 数教考证东西，实在理解没有了您便当他是python便完了，可是主要for 数教定理证实 好比： 保守数教：写证实如集文“明显由勾股定理所示，巴推巴推...”，人类读懂（小教便这样学的），但是电脑没法“考证”每一步可否松散（它没有理解）。 Lean 方法化：统统写成代码，电脑逐止编译/考证。证实 = 可施行法式，整歧义、机械查证 保守证实像“脚写做文”（主观，好比您下考问最初多少讲年夜题的时候），Lean 像“Python 代码 + 尝试用例”（运行即验）
Deepseek为何要玩 Lean呢？
数教野用它方法化数论/多少定理（已经方法化 10万+ 定理的 Mathlib 库），以是您有能够证实的dataset了么AI 数教增强：天生 Lean 代码， Lean 运行考证 ，证实胜利/失利因为有了binary的 feedback，能够完善 RL 嘉奖关环。Prover-V2 博为 Lean 劣化 tokenizer，撑持 theorem、by、sorry 等语法。现在能够天生也能瞅懂lean代码了
举个例子：好比咱们要算一个定理，前 n 个偶数的战即是 n^2：
那个对于应lean申明（formal state）即是import Mathlib.Data.Nat.Basicimport Mathlib.Algebra.BigOperators.Basic
open BigOperators
/--The sum of the first `n` odd numbers equals `n^2`:`∑_{k = 0}^{n-1} (2k+1) = n^2`.-/theorem odd_sum_square (n : ℕ) : ∑ k in Finset.range n, (2 * k + 1) = n ^ 2 := by -- proof to be filled admit
而后把那个工具改为prompts收给prover2里的V3（prover2是二个模子构成的一个V3，一个7B的子处置器）V3交到一个如许的prompts[System] You are a mathematical reasoning expert and Lean 4 proof designer.Given a math problem and its Lean formal statement, you should:
1. Explain the solution in natural language (chain-of-thought).2. Decompose the proof into clear subgoals.3. Produce a Lean 4 proof skeleton which follows your plan and contains `sorry` placeholders for subgoals.
[User]Problem (informal):Prove that the sum of the first n odd numbers equals n^2.
Formal statement (Lean 4):theorem odd_sum_square (n : ℕ) : ∑ k in Finset.range n, (2 * k + 1) = n ^ 2 := by ?_
处置完了，便成为了一个COT的解题的望角+lean的骨架了，牢牢好一点儿细节的subgoal出来证实[DeepSeek-V3]
(1) Natural-language chain-of-thought (high-level plan):
We prove by induction on n.
Base case: n = 0. The sum over an empty range is 0, and 0^2 = 0.
Inductive step: assume that for some n we have ∑_{k < n} (2k + 1) = n^2.Then ∑_{k < n+1} (2k + 1)= (∑_{k < n} (2k + 1)) + (2n + 1)= n^2 + (2n + 1)= (n + 1)^2.Thus, by induction, the equality holds for all n.
(2) Subgoal decomposition (informal):
Subgoal 1 (base case): Show: ∑_{k < 0} (2k+1) = 0^2.
Subgoal 2 (range decomposition): For all n, ∑_{k < n+1} (2k+1) = (∑_{k < n} (2k+1)) + (2n+1).
Subgoal 3 (inductive hypothesis usage): Assume IH: ∑_{k < n} (2k+1) = n^2. Show: ∑_{k < n+1} (2k+1) = (n+1)^2.
Subgoal 4 (algebraic identity): Show: n^2 + (2n+1) = (n+1)^2.
(3) Lean 4 proof skeleton with `sorry`:
import Mathlib.Data.Nat.Basicimport Mathlib.Algebra.BigOperators.Basic
open BigOperators
theorem odd_sum_square (n : ℕ) : ∑ k in Finset.range n, (2 * k + 1) = n ^ 2 := by -- induction on n induction' n with n ih · -- Subgoal 1: base case n = 0 -- ∑_{k < 0} (2k+1) = 0^2 -- (use simp to evaluate the empty sum) sorry · -- Subgoal 2 + 3 + 4: inductive step -- We rewrite the sum over `range n.succ`. have h_decompose : ∑ k in Finset.range n.succ, (2 * k + 1) = (∑ k in Finset.range n, (2 * k + 1)) + (2 * n + 1) := by -- Subgoal 2: range decomposition sorry
-- Use the induction hypothesis to replace the partial sum by n^2. have h_using_IH : (∑ k in Finset.range n, (2 * k + 1)) + (2 * n + 1) = n ^ 2 + (2 * n + 1) := by -- Subgoal 3: apply IH sorry
-- Now prove the algebraic identity n^2 + (2n+1) = (n+1)^2. have h_algebra : n ^ 2 + (2 * n + 1) = (Nat.succ n) ^ 2 := by -- Subgoal 4: algebraic manipulation sorry
-- Combine the equalities to close the goal. -- target: ∑_{k < n.succ} (2k+1) = (n.succ)^2 -- by transitivity using h_decompose, h_using_IH, h_algebra sorry
上面open Bigoperators的即是lean4的根本骨架了，而后每个-- 是一个subgoal，sorry留着当占位符，接给7b的小模子来证实了举一身材目标的例子：[System] You are a Lean 4 theorem prover. Your task is to fill in the proofof the given le妹妹a, without changing its statement.
[User]Context:
import Mathlib.Data.Nat.Basicimport Mathlib.Algebra.BigOperators.Basic
open BigOperators
-- `odd_sum_square` is being proved by induction on `n`.-- In the inductive step, we have the following subgoal:
theorem range_decompose_subgoal (n : ℕ) : ∑ k in Finset.range n.succ, (2 * k + 1) = (∑ k in Finset.range n, (2 * k + 1)) + (2 * n + 1) := by ?_
Please fill in the proof in Lean 4.
7B的便把那个给解了，解完以后的被戴进到本来的V3的成果了，sorry被交流成那个成果[Prover-7B]
theorem range_decompose_subgoal (n : ℕ) : ∑ k in Finset.range n.succ, (2 * k + 1) = (∑ k in Finset.range n, (2 * k + 1)) + (2 * n + 1) := by -- Use the standard le妹妹a `Finset.range_succ`. -- It tells us: -- range (n.succ) = range n ∪ {n}, -- and the sum over `range (n.succ)` splits accordingly. simpa [Finset.range_succ, Nat.succ_eq_add_one] using Finset.sum_range_succ (fun k => (2 * k + 1 : ℕ)) n
每一个subgoal皆被解完，那末天然便出了一个残破的lean证实，接给lean verify来考证就能够了以是prover-v2再解问数教题的时候是那个套路，各人瞅懂了吗？--------------出瞅懂不妨，归正您们也用没有到-------------上面道简单理解的math-v2mathV2 便出格的佳理解，可是很先天的设想好比尺度V3也能干数教题，可是干没有了证实题，因为年夜模子对于数教题的作法战人脑思考纷歧样，以是以前训了prove2，拿lean去干考证各人经常能瞅到一个数教题给LLM，它成果准确，可是中心的think步调皆正在治写为何如许？因为您grpo也佳，ppo也佳，您皆确认的是终极谜底的值有人道您的不合错误，因为R1论文里写的，grpo异常对于think的中心历程check，check是check，不过check您输出的范式是否是<think></think>
那末prm是否是个佳的思路，可是prm易训啊。Deepseek math V2的作法是甚么？实在能够归纳为抽象PRM差别于每步皆要考证准确取可的PRM，您针对于输出中心成果分歧确认个黑白，那个仍是能够完毕的吧！以是思路便去了起首，尔要有一个小镇干题野，一个给干题野批卷子的西席，可是那个西席可以自己便没有咋滴，以是尔借要找个学委果去监视西席的水平。
因而便有了上面那3个模子
1. 证实天生器 ，干题野(Proof Generator) (πθ)
那是担当理论天生数教证实的语言模子。
• 功用：依据 给定的成就 (X) 天生证实 (Y)。
• 锻炼目标： 使用锻炼佳的考证器动作嘉奖模子 (RY) 对于其截至加强进修锻炼，以最年夜化证实品质。
• 自尔考证： 为了增强拉理才气，天生器借被鼓励发生证实 Y 以后，松交着截至自尔阐发 (Z)，即自尔评介战纠错。这类自尔评介的精确性也受到嘉奖，简朴道即是您念下考得到下分，光干挑选题战挖空是不可的，您患上干年夜题证实题，并且您的证实步调患上写分明，那部门会有分外的分数。
2. 证实考证器 ，判卷西席(Proof Verifier) (πϕ)
那是担当评介证实品质的中心组件。
• 功用：依据 下层评介尺度 (Iv)，评介证实的残破性战松散性，并给出分数（1 分、0.5 分或者 0 分）。
• 感化： 它动作嘉奖模子，为证实天生器供给反应，辅导其劣化。
• 锻炼根底： 它最初是正在一个颠末监视微调的模子 (DeepSeek-V3.2-Exp-SFT) 的根底上，颠末加强进修截至锻炼的。
3. 元考证器 ，学委果监视职员(Meta-Verifier) (πη)
那是一个特地用于保证考证器自己的阐发成果忠厚可靠的帮助模子。
• 念头： 作家引进元考证是为了处置考证器可以正在评分准确的情况下，“假造没有存留的成就” 以得到谦嘉奖的漏洞。
• 功用： 元考证器被锻炼去评介考证器输出的阐发 (V) 的品质。它会查抄考证器指出的成就可否实在存留，和那些成就可否正在逻辑上撑持考证器给出的分数。即是您西席写的考语可否靠谱。
• 配合感化： 元考证器供给的品质分数 (Rmeta) 被调整到证实考证器的嘉奖函数中，进而进步了考证器正在识别成就圆里的忠厚性（faithfulness）
那里实在躲藏了一个逻辑，学委凭甚么能给西席的判卷考语挨分，他常识才气必然比西席强吗？也即是元考证器必然比考证器勇猛吗？
非也，因为他俩干的没有是一个任务，西席给师长教师挨分，长短常庞大的，它要确认它确实瞅懂了师长教师的对于取错，成就终归出正在哪？要写出很详确的证实。
可是，关于西席给题挨的分数对于应的考语，学委果逻辑是很简朴的，便像让您干题您干没有进去，可是让您给他人的论调里浮薄错，您又主动，又能找出成就地点，一朝元考证（学委果才气）发明西席那考语皆开端治写了，那末便到了升级西席的时候。
现在3个role皆到位了，开端干题干题野干了一讲题--->教员 不但瞅您干对于不，借要瞅您的中心历程，而后从谜底的准确性，战中心历程的准确性二个维度给您干题野挨分----> 谜底一般是有唯一的，可是中心历程一定是唯一的，如何能证实西席公允公平的给干题野挨分，学委（元考证器）便去查抄西席的考语去了。
那末要完毕如许一个干题到挨分过程，如何锻炼呢？
具体历程：
1. 证实考证器 (πϕ) 的锻炼战增强
动作西席（PRM，固然是all process的rm），证实考证器 (πϕ) 是全部体系的中心，因为它界说了嘉奖函数战证实品质尺度。
开端锻炼
1）. 根底模子： 考证器是鉴于 DeepSeek-V3.2-Exp-SFT 版原锻炼的，该版原颠末监视微调（SFT）处置，具有取数教战代码相干的拉理数据根底。
2）. 数据建立： 钻研职员起首从 AoPS 比赛中抓与了 17,503 个主要需要证实的数教奥赛成就 (Dp)。
3）. 天生战标注： 光有Dp那面工具不敷用啊，随即，使用DeepSeek-V3.2-Exp-Thinking （那个模子尔仿佛出睹过他们收啊）天生了候选证实，并提醒该模子截至多轮迭代劣化以进步全面性战松散性。而后便当上人推肩扛了，出法子热启用是如许的，找一堆数教大师按照预约义的初级评介尺度 (Iv) 对于那些证实截至评分（1 分、0.5 分、0 分），进而建立了初初的 RL 数据散 Dv。
4）. RL 目标： 考证器颠末加强进修截至锻炼，目标是天生证实阐发并给出分数。嘉奖函数包罗有格局嘉奖 (Rformat): 保证输出包罗识别出的成就归纳战分数，别的分数嘉奖 (Rscore): 鉴于猜测分数 (s′) 取大师标注分数 (s) 的交长途度 (1−∣s′−s∣) 去嘉奖模子。
弄定了西席目前，引进学委果监视元考证器 (πη)进步 忠厚性
元考证器 (πη)退场 ：开端锻炼存留一个枢纽漏洞：当西席证实存留缺点 (si<1) 时，考证器能够颠末猜测准确的高分数去得到谦嘉奖，但是共时假造出没有存留的成就（hallucinating non-existent issues），几有面嘉奖乌客（可以嚷嘉奖托钵人更适宜），进而损伤了它的可托度。为了处置一成就，引进了元考证器 (πη)。它是一个自力的、颠末 RL 锻炼的模子，用于评介考证器阐发自己的品质，而没有是评介本初证实的品质。
元考证锻炼： 大师按照元考证尺度 (Imv) 对于初初考证器发生的阐发 (Vi)中止 评分 (msi∈{0,0.5,1})，天生 Dmv 数据散。元考证器颠末 RL 锻炼，其目标是评介考证器指出的成就可否确实存留和那些成就可否逻辑上撑持考证器给出的分数。
增强考证器： 终极（正在某个锻炼的checkpoint里，论文出道那块），元考证器供给的品质分数 (Rmeta) 被调整到证实考证器的嘉奖函数中：RV=Rformat⋅Rscore⋅Rmeta。那提拔了考证器识别成就时的忠厚性。颠末增强，考证器正在考证散上的均匀阐发品质分数从 0.85进步 到 0.96。
以是也能够理解，元考证器正在锻炼初是存留的，正在锻炼中它的元考证才气便被考证器给吸纳了（西席战学委开体了）
2. 干题野证实天生器 (πθ) 的锻炼战自尔考证
开端锻炼
• 初初化： 正在每一个锻炼迭代中，证实天生器皆是从考证器的查抄面初初化的。比力挖苦的是，第一代师长教师干题野，实际上是个西席。。。
• RL 目标： 天生器使用锻炼佳的考证器 (πϕ) 动作嘉奖模子。天生器的 RL 目标是最年夜化考证器对于所天生证实 (Yi) 给出的分数 (RY)。
增强拉理才气的自尔考证
关于 IMO 战 CMO 等挑战性成就，单次测验考试很易天生完善的证实。为了让天生器具有迭代改良的才气，它被付与了自尔考证的才气。
1）. 自尔阐发请求： 锻炼时，天生器被请求正在天生证实 (Y) 以后，立即天生一个依照考证器差异格局战尺度 (Iv) 的自尔阐发 (Z)。
2）. 分离嘉奖构造： 嘉奖函数分离了对质明自己的评分 (RY) 战对于自尔阐发的元考证分数 (RZ)。
◦ RY=s（考证器给出的证实分数）
◦ RZ=Rscore(s′,s)⋅Rmeta(Z)（s′ 是天生器猜测的自尔分数，s 是考证器给的理论分数，Rmeta(Z) 是考证器对于自尔阐发忠厚度的评介）。
3）. 鼓励体制： 这类构造鼓励模子干到如下多少面：
◦ 忠厚天认可毛病，而没有是虚假天声称准确。
◦ 颠末天生准确的证实并精确天观点到其松散性去得到最下嘉奖。
◦ 天生器得到下嘉奖的有用战略是：正在终极肯定输出以前，识别并处置自己证实中尽可以多的成就。
3. 考证取天生之间的配合轮回
考证器战天生器（也戴着元考证才气的）颠末一个良性轮回连续相互提拔，那个轮回中的枢纽是主动化标签过程，它使患上体系能够正在不野生干预的情况下扩大数据。
1. 配合效力： 考证器进步了天生器的才气，而更强大的天生器则发生了新的、更具挑战性的证实，那些证实挑战了考证器目前的限度，即天生器取考证器之间的差异，道利剑了考证器整欠好便瞅没有太大白天生器再道啥了
。
2. 主动化标签过程： 可是也不克不及因为瞅陌生便再去一次人推肩扛吧？为了连续改良考证器以适应那些新的、易以考证的证实，deepseek开辟了一个主动化标签过程，该过程代替了野生标注。
◦ 步调 1： 对于每一个新的证实，天生 n 个自力的考证阐发，为啥要这样搞呢？
最年夜化毛病发明： 颠末屡次采样，即使证实的缺点十分细微或者荫蔽，此中最少一个阐发陈述识别出该缺点的可以性也会年夜年夜增加。
为元考证供给按照：只需 这些正在屡次阐发中陈述成就的证实，才会被收进下一步的元考证评介。那保证了只需最有可以包罗缺点的证实，才会截至更深入、更下品质的检查。
肯定最高分数： 终极的标签分派过程是查抄这些分派最高分数的阐发。假设多个自力的阐发皆陈述了差异或者类似的成就（即高分），那末那个凭证便更可靠，随即元考证会确认其有用
◦ 步调 2：关于 陈述成就的阐发（分数 0 或者 0.5），天生 m 个元考证评介去考证发明的成就可否有用。
◦ 步调 3： 取此共时，假设年夜大都元考证评介确认了成就，则该阐发被觉得是有用的。
◦ 步调 4： 那末，假设统统考证测验考试中皆不发明公道的成就，则证实被标识表记标帜为 1 分；不然，证实被标识表记标帜为有用阐发中给出的最高分数。
1分的（也可以晚期会把0.5分共同）那些证实因为元考证被标记为考证您的证实是可托的，因为考证您的证实是可托的，以是您的证实历程是可托的，那末，干题野也即是天生器的证实逻辑自己就能够成为一条dataset被参加到下一轮train的datasets里面，那个即是主动标签的逻辑。
这类齐主动化过程正在最初二次锻炼迭代中完整代替了野生标注，完毕了正在考证计较范围扩大下，连续为考证器创立新的锻炼数据，进而退一步改良考证器，因为天生器是考证器的女子，以是天生器也愈来愈勇猛，天生器天生的数据被主动标签流成给收到考证器来了，考证器又强了，强了目前又是下一个迭代的更勇猛的天生器了，周而复始。
那个比prover的作用年夜的启事，prover是一定范围机械对于机械的对于话（lean），素质上面太窄，可是鉴于天然语言考证的数教便纷歧样了，假设您能拿那个办法，干数教题能拿到IMO的金牌，这您玩代码一致能够用差异的办法拿到live bench的实践谦分，因为现在的vibe coding的一年夜成就是，思考范式比力好，只寻求最初的逻辑委曲被满意，而后瞎写很多多少治收集的次劣代码，部分品质比力好，假设您的中心步调皆能出格的简单被证实，被元证实，这实践上您就可以写出战初级法式员一致明了又繁复的代码（没有memory等需要处置的少尾效力的条件下）
|
提升卡
置顶卡
沉默卡
喧嚣卡
变色卡
千斤顶
照妖镜
广告
