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

21–30 of 53 posts

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

#21

Post by N_Lens »

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).

Also the impressive IMO-ProofBench Basic benchmark, the model achieved nearly 99% accuracy, though it fell slightly behind Gemini Deep Think on the Advanced subset.

The approach shifts from "result-oriented" to "process-oriented" verification, particularly important for theorem proving where rigorous step-by-step derivation matters more than just numerical answers.

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

#24

Post by zaxioms »

blazespin wrote: post #16
zaxioms wrote: post #3

It's cool, but I genuinely cannot fathom why they are targeting natural language proofs instead of a proof assistant.

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.

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

#25

Post by drawnwren »

JacobiX wrote: post #10
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.

I think that mathematical proofs, as they are actually written, rely on natural language and on a large amount of implicit shared knowledge. They are not formalized in the Principia Mathematica sense, and they are even further from the syntax required by modern theorem provers. Even the most rigorous proofs such as those in Bourbaki are not directly translatable into a fully formal system.

If you don't mind stretching your brain a bit, Wittgenstein was obsessed with this notion. https://www.bu.edu/wcp/Papers/Educ/EducMaru.htm#:~:text=Witt...

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

#27

Post by indolering »

ogogmad wrote: post #26
mekpro wrote: post #23

How this improvement translate into real world agentic coding task ?

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.

It would be helpful in automating the busy work of many verification aware programming languages. At least the Dafny authors are excited about it.

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

#28

Post by Davidzheng »

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).

I think serious math research progress should come in 1-2 years. It basically only depends on how hard informal verification is, because training data should be not a problem and if informal verification is easy you can throw RL compute at it until it improves.

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

#29

Post by nextos »

indolering wrote: post #27
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.

It would be helpful in automating the busy work of many verification aware programming languages. At least the Dafny authors are excited about it.

IMHO, this remains a great space to explore. You type some formal specification in e.g. Hoare logic, and a mix of SAT/SMT and LLMs autocomplete it. Correct by definition.

It would also facilitate keeping engineers in the loop, who would decompose the problem into an appropriate set of formally specified functions.

They could also chip in when necessary to complete difficult proofs or redefine the functions.

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

#30

Post by Davidzheng »

zaxioms wrote: post #3

It's cool, but I genuinely cannot fathom why they are targeting natural language proofs instead of a proof assistant.

I think there's a lot of baggage doing it in lean. like what the libraries are at currently. how things are implemented. which things are not implemented, etc. but it still remains to be seen what wins (my money would be on informal)
Post reply on HN