11–20 of 83 posts
> The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench.
Which is 0.07% (edit: 7%) for PutnamBench
related: I imagine in the future we might several "expert" LLM's and a wrapper can delegate tasks as needed as if it were a "tool". That way we can have segregation of expertise - each individual model can excel at one single thing. A prover model might be used as a tool in the coming future.
Is that not what MoE models already do?
That Putnam bench graph (middle one) is showing 49/658 solve rate. > The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. Which is 0.07% (edit: 7%) for PutnamBench
It feels pretty intuitive to me that the ability for an LLM to break a complex problem down into smaller, more easily solvable pieces will unlock the next level of complexity.
This pattern feels like a technique often taught to junior engineers- how to break up a multi-week project into bitesized tasks. This model is obviously math focused, but I see no reason why this wouldn't be incredibly powerful for code based problem solving.
That Putnam bench graph (middle one) is showing 49/658 solve rate. > The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. Which is 0.07% (edit: 7%) for PutnamBench
49/658 is 7%
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.
related: I imagine in the future we might several "expert" LLM's and a wrapper can delegate tasks as needed as if it were a "tool". That way we can have segregation of expertise - each individual model can excel at one single thing. A prover model might be used as a tool in the coming future.
The No Free Lunch Theorem implies that something like this is inevitable https://en.wikipedia.org/wiki/No_free_lunch_in_search_and_op...
> The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals It feels pretty intuitive to me that the ability for an LLM to break a complex problem down into smaller, more easily solvable pieces will unlock the next level of complexity. This pattern feels like a technique often taught to junior engineers- how to break up a multi-week project into bitesize…
Super interesting that they chose 671B and 7B. no like 32B which feels like a "sweet spot"
--> "In an increasingly crowded field of LLMs, how will our (costly to produce) model stand out?"