Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

github.com

Post reply on HN
Print view View original

41–50 of 53 posts

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#41

Post by hooloovoo_zoo »

dwohnitmok wrote: post #13

Is everyone just glossing over the first place score of 118/120 on the Putnam?! I mean we'll see how it does on the upcoming 2025 test, but that's insane! We've seen absolutely ridiculous progress in model capability over the past year (which is also quite terrifying).

For one thing, it's not a real score; they judged the results themselves and Putnam judges are notoriously tough. There was not a single 8 on the problem they claim partial credit for (or any partial credit above a 2) amongst the top 500 humans. https://kskedlaya.org/putnam-archive/putnam2024stats.html.

For another thing, the 2024 Putnam problems are in their RL data.

Also, it's very unclear how these competitions consisting of problems designed to have clear-cut answers and be solved by (well-prepared) humans in an hour will translate to anything else.

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#42

Post by crvdgc »

awei wrote: post #4

Something weird here, why is it so hard to have a deterministic program capable of checking a proof or anything math related, aren't maths super deterministic when natural language is not. From first principles, it should be possible to do this without a llm verifier.

Checking the validity of a given proof is deterministic, but filling in the proof in the first place is hard.

It's like Chess, checking who wins for a given board state is easy, but coming up with the next move is hard.

Of course, one can try all possible moves and see what happens. Similar to Chess AI based on search methods (e.g. MinMax), there are proof search methods. See the related work section of the paper.

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#43

Post by gunalx »

viraptor wrote: post #20
gunalx wrote: post #14

If i read it right it used multiple samples of itself to verify the aqccuracy, but isnt this problematic?

In what way? Panel of experts approach has been a thing for a while now and it's documented to improve quality.

Well problematic because they are using their own verifier as apanem of experts, with their own model trained specifically to satisfy this verifier. On the benchmark runs, they dont mention using human experts to cross validate their scores.

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#44

Post by awei »

awei wrote: post #4

Something weird here, why is it so hard to have a deterministic program capable of checking a proof or anything math related, aren't maths super deterministic when natural language is not. From first principles, it should be possible to do this without a llm verifier.

Thanks to everyone who replied, I understand it better now!

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#45

Post by westurner »

hooloovoo_zoo wrote: post #41
dwohnitmok wrote: post #13

Is everyone just glossing over the first place score of 118/120 on the Putnam?! I mean we'll see how it does on the upcoming 2025 test, but that's insane! We've seen absolutely ridiculous progress in model capability over the past year (which is also quite terrifying).

For one thing, it's not a real score; they judged the results themselves and Putnam judges are notoriously tough. There was not a single 8 on the problem they claim partial credit for (or any partial credit above a 2) amongst the top 500 humans. https://kskedlaya.org/putnam-archive/putnam2024stats.html . For another thing, the 2024 Putnam problems are in their RL data. Also, it's very unclear how these competitions c…

What do other models trained on the same problems score? What about if they are RL'd to not reproduce things word for word?

Why do you think that the 2024 Putnam programs that they used to test were in the training data?

/? "Art of Problem Solving" Putnam https://www.google.com/search?q=%22Art+of+Problem+Solving%22...

From p.3 of the PDF:

> Curating Cold Start RL Data: We constructed our initial training data through the following process:

> 1. We crawled problems from Art of Problem Solving (AoPS) contests , prioritizing math olympiads, team selection tests, and post-2010 problems explicitly requiring proofs, total- ing 17,503 problems.

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#46

Post by ogogmad »

simulator5g wrote: post #38
ogogmad wrote: post #26

Earlier quoted context omitted.

It doesn't. However, having a free-of-charge maths genius available 24/7 has broad potential. It's hard to predict what it will be used for.

This already exists: https://www.wolframalpha.com/

Since you're bad at maths, you think being good at maths is being a calculator like WolframAlpha.

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#47

Post by isotypic »

westurner wrote: post #45
hooloovoo_zoo wrote: post #41

Earlier quoted context omitted.

For one thing, it's not a real score; they judged the results themselves and Putnam judges are notoriously tough. There was not a single 8 on the problem they claim partial credit for (or any partial credit above a 2) amongst the top 500 humans. https://kskedlaya.org/putnam-archive/putnam2024stats.html . For another thing, the 2024 Putnam problems are in their RL data. Also, it's very unclear how these competitions c…

What do other models trained on the same problems score? What about if they are RL'd to not reproduce things word for word? Why do you think that the 2024 Putnam programs that they used to test were in the training data? /? "Art of Problem Solving" Putnam https://www.google.com/search?q=%22Art+of+Problem+Solving%22... From p.3 of the PDF: > Curating Cold Start RL Data: We constructed our initial training data through…

> Why do you think that the 2024 Putnam programs that they used to test were in the training data?

Putnam solutions can be found multiple places online: https://kskedlaya.org/putnam-archive/, https://artofproblemsolving.com/community/c3249_putnam. These could have appeared in the training of the base LLM DeepSeek-V3.2-Exp or as problems in the training set - they do not give further detail on what problems they selected from AOPS and as the second link gives they are there.

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#48

Post by cubefox »

gunalx wrote: post #43
viraptor wrote: post #20

Earlier quoted context omitted.

In what way? Panel of experts approach has been a thing for a while now and it's documented to improve quality.

Well problematic because they are using their own verifier as apanem of experts, with their own model trained specifically to satisfy this verifier. On the benchmark runs, they dont mention using human experts to cross validate their scores.

I assume they use self-verification only during RL training to provide the reward signal, but not for benchmarks.

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#49

Post by blazespin »

zaxioms wrote: post #24
blazespin wrote: post #16

Earlier quoted context omitted.

More training data on advanced math. Lean is cool, but it's mostly about formalizing stuff we already know.

Ok I guess I could have told you that. What I really meant is that in the future where LLMs are doing new math (which I'm skeptical of, but I digress) I would not trust any of it unless it was formally verified.

if you read the paper that is the intention, to guide stuff like lean.

i don't think llm is a great pure rlvr

Re: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [pdf]

#50

Post by blazespin »

crvdgc wrote: post #42
awei wrote: post #4

Something weird here, why is it so hard to have a deterministic program capable of checking a proof or anything math related, aren't maths super deterministic when natural language is not. From first principles, it should be possible to do this without a llm verifier.

Checking the validity of a given proof is deterministic, but filling in the proof in the first place is hard. It's like Chess, checking who wins for a given board state is easy, but coming up with the next move is hard. Of course, one can try all possible moves and see what happens. Similar to Chess AI based on search methods (e.g. MinMax), there are proof search methods. See the related work section of the paper.

who likely wins, fify
Post reply on HN