[HN Gopher] DeepSeekMath-V2: Towards Self-Verifiable Mathematica...
___________________________________________________________________
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
[pdf]
Author : fspeech
Score : 70 points
Date : 2025-11-27 20:03 UTC (2 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| photon_lines wrote:
| Exciting stuff from a fantastic team.
| zaxioms wrote:
| It's cool, but I genuinely cannot fathom why they are targeting
| natural language proofs instead of a proof assistant.
| mamami wrote:
| Natural language is a lot more, well, readable than say lean.
| You get a _lot_ less intuition and understanding of what the
| model is attempting to do in the first place.
| awei wrote:
| 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.
| riku_iki wrote:
| such high performance program indeed could potentially be
| superior, if it would exist (this area is very undeveloped,
| there is no existing distributed well established solution
| which could handle large domain) and math would be formalized
| in that program's dsl, which also didn't happen yet.
| jebarker wrote:
| I haven't read the paper yet, but I'd imagine the issue is
| converting the natural language generated by the reasoner into
| a form where a formal verifier can be applied.
| JacobiX wrote:
| 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.
| xemdetia wrote:
| Maths can be super deterministic but often difficult to compute
| because of concepts like inferring by induction. I had to
| personally unlearn and rebase my understanding of math based in
| computation to 'get' pure maths. Another example is set
| building. You often don't need to compute the existence of
| members of sets in pure math you just need to agree that there
| are some members of a set that meet the criteria. How many or
| how many things that aren't in the set aren't meaningful often
| times to accept something and move on with the proof. From the
| computing perspective this can be difficult to put together.
| agentultra wrote:
| So it's designed for informal proofs and it "verifies" based on a
| rubric fitting function and human interaction, is that right?
|
| What's the use case for a system like this?
| newyankee wrote:
| That is amazing if they can do all of this at < 10 % of the cost
| of frontier labs. Off course they work in the shadows of the
| great work done in the frontier labs and shared, but there is
| some exceptional high speed execution happening behind the scenes
| that shows this is clearly a race, but a race where China is
| happy to be #2 as long as the gap is not significant and the
| costs are reasonable
| dwohnitmok wrote:
| 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).
___________________________________________________________________
(page generated 2025-11-27 23:00 UTC)