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

DeepSeek-Prover-V2

github.com

Post reply on HN
Print view View original

51–60 of 83 posts

Re: DeepSeek-Prover-V2

#51

Post by roywiggins »

thrance wrote: post #49
bearjaws wrote: post #42

Earlier quoted context omitted.

It's actually pretty hilarious how far into detail they can go. For example, I made a bot that you could give it a problem statement, and then it would return an array of steps to accomplish it. Then you could take the steps, and click on them to break them down and add them to the list. If you just kept clicking you would get to excruciating detail. For example taking out the trash can become over ~70 individual ste…

This feels like a manual for infiltrated aliens: "How to pass as humans, Vol. I"

or for goblins:

https://goblin.tools/

Re: DeepSeek-Prover-V2

#52

Post by devoutsalsa »

navanchauhan wrote: post #31
Implicated wrote: post #27

Earlier quoted context omitted.

Or, like with Claude, it being effectively lobotomized during north american 'business' hours. 3am PST? Cracked. 8am PST? ... mentally challenged.

This is pretty interesting. Do you have more information about this?

I’m pretty sure the parent comment is referring to capacity constraints. When the Americans come online in the morning, Claude frequently can’t keep up with demand and error messages saying the system is at capacity are common.

Re: DeepSeek-Prover-V2

#53

Post by mcshicks »

You can run the model for free on openrouter.ai. I have played around with lean, slowly working my way through mathmatics in lean. I was stuck on this problem in section 3.6

theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ} (sa : ConvergesTo s a) (sb : ConvergesTo s b) :

For fun I tried it on the free model on openrouter.ai. Got the answer the first time.

https://leanprover-community.github.io/mathematics_in_lean/m...

Here's the answer just to give you a feel.

  by_contra h
  have h₁ : a ≠ b := h
  have h₂ : |a - b| > 0 := by
    apply abs_pos.mpr
    exact sub_ne_zero.mpr h₁
  -- Use the definition of convergence to find N₁ and N₂
  have h₃ := sa (|a - b| / 2) (by linarith)
  have h₄ := sb (|a - b| / 2) (by linarith)
  cases' h₃ with N₁ h₃
  cases' h₄ with N₂ h₄
  -- Choose N to be the maximum of N₁ and N₂
  let N := max N₁ N₂
  have h₅ := h₃ N (by simp [N, le_max_left])
  have h₆ := h₄ N (by simp [N, le_max_right])
  -- Derive a contradiction using the triangle inequality
  have h₇ : |s N - a|

Re: DeepSeek-Prover-V2

#54

Post by pama »

whatshisface wrote: post #36

How much education would a human need to perform at this level on the benchmarks?

Learning to formalize math to then prove Putnam competition problems rigorously in Lean would require you to have mid-to-advanced college level math and CS background. (Learning to do a small fraction of the Putnam competition without using Lean probably only needs strong highschool math and early undergrad math, with training for competitions a strong bonus.)

Re: DeepSeek-Prover-V2

#55

Post by woah »

oofbaroomf wrote: post #12
samvaran wrote: post #9

Earlier quoted context omitted.

Is that not what MoE models already do?

No. Each expert is not separately trained, and while they may store different concepts, they are not meant to be different experts in specific domains. However, there are certain technologies to route requests to different domain expert LLMs or even fine-tuning adapters, such as RouteLLM.

Why do you think that a hand-configured selection between "different domains" is better than the training-based approach in MoE?

Re: DeepSeek-Prover-V2

#57

Post by neom »

AlexCoventry wrote: post #45
samvaran wrote: post #9

Earlier quoted context omitted.

Is that not what MoE models already do?

MoE models route each token , in every transformer layer, to a set of specialized feed-forward networks (fully-connected perceptrons, basically), based on a score derived from the token's current representation.

Good visual explainer in here: https://deepgram.com/learn/mixture-of-experts-ml-model-guide

Re: DeepSeek-Prover-V2

#59

Post by johnmcd3 »

ekez wrote: post #29

I wonder if the authors have tried incorporating error feedback from Lean into their models. Work from 2023 [1] showed general purpose models did better when they were able to incorporate error feedback, humans incorporate error feedback, but none of the SOTA models on minif2f seem to. [1]: https://arxiv.org/abs/2310.04353

In a way, DeepSeek Prover's subgoal decomposition is a partial-step towards error/proof-state feedback. (DS Prover breaks down a proof into subgoals and attacks each subgoal separately with batched sampling, then puts the pieces back together.)

This is distinct from the approach of the previous SOTA for an open-weights model (Kimina Prover) which generated at the full-proof level.

While it was very impressive to see Kimina's ability to generate medium-length proofs (think AIME-level problems) without sub-goals or feedback at intermediate steps, it's likely that at least subgoal decomposition will be required for longer proofs (think IMO-level problems.)

I certainly agree that where and how error/proof state feedback is best incorporated (training data synthesis / reward function / CoT during inference / etc.) is a fascinating area of research. (It's rumored that GDM's AlphaProof does use proof state / lean feedback already.)

Post reply on HN