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

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.

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

#5

Post by [deleted] » Thu, Nov 27, 2025, 8:50 PM UTC

[deleted]

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

#6

Post by agentultra » Thu, Nov 27, 2025, 8:55 PM UTC

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?

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

#7

Post by mamami » Thu, Nov 27, 2025, 9:00 PM UTC

zaxioms wrote: post #3

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

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.

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

#8

Post by riku_iki » Thu, Nov 27, 2025, 9:06 PM UTC

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.

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.

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

#9

Post by jebarker » Thu, Nov 27, 2025, 9:09 PM UTC

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

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

#10

Post by JacobiX » Thu, Nov 27, 2025, 9:12 PM UTC

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.