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

41–50 of 83 posts

Re: DeepSeek-Prover-V2

#41

Post by nthingtohide »

revskill wrote: post #34

The way intelligence works to me, is more about: - Making correct and smart assumption. Currently all LLM bots are too stupid at making good assumptions. I don't want to explicitly repeat and repeat again my own assumptions while the context is clear enough. Hey bots, try harder. - LLM bot needs to bring their own secondary and contextual memory in reasoning, i don't want to do it for you, ok ? You're the bot. - Thin…

I propose human-AI interaction data must be made public. This is our collective wikipedia of AI era. Otherwise our progress will be blank line after 2022. Just as Egyptians didn't write down process to move giant rocks.

Re: DeepSeek-Prover-V2

#42

Post by bearjaws »

islewis wrote: post #14

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

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 steps if you really drill into the details.

Some of the steps:

Stand close to the trash can – Position yourself so you have stable footing and easy access.

Place one hand on the rim of the can – Use your non-dominant hand to press lightly on the edge of the trash can to hold it in place.

Grip the top edge of the bag with your other hand – Find the part of the bag that extends past the rim.

Gently lift the bag upward – While your one hand stabilizes the can, slowly pull the bag up with the other.

Tilt the can slightly if needed – If the bag sticks or creates suction, rock or tilt the can slightly while continuing to lift.

Avoid jerking motions – Move steadily to prevent tears or spills

Re: DeepSeek-Prover-V2

#43

Post by HappyPanacea »

EvgeniyZh wrote: post #35
HappyPanacea wrote: post #32

Earlier quoted context omitted.

How likely is it that Putnam answers were in DeepSeek's training data?

The solutions weren't published anywhere. There is also no good automatic way to generate solutions as far as I know, even expensive ones (previous sota was 10 solutions and one before was 8 using pass@3200 for 7b model). Potentially the developers could've paid some people who are good in putnam-level math problems and lean to write solutions for LLMs. It is hard to estimate likelihood of that but it sounds like was…

AoPS seems to have a forum dedicated to Putnam (including 2024): https://artofproblemsolving.com/community/c3249_putnam and here is a pdf with solutions to Putnam 2023: https://kskedlaya.org/putnam-archive/2023s.pdf

Re: DeepSeek-Prover-V2

#44

Post by EvgeniyZh »

HappyPanacea wrote: post #43
EvgeniyZh wrote: post #35

Earlier quoted context omitted.

The solutions weren't published anywhere. There is also no good automatic way to generate solutions as far as I know, even expensive ones (previous sota was 10 solutions and one before was 8 using pass@3200 for 7b model). Potentially the developers could've paid some people who are good in putnam-level math problems and lean to write solutions for LLMs. It is hard to estimate likelihood of that but it sounds like was…

AoPS seems to have a forum dedicated to Putnam (including 2024): https://artofproblemsolving.com/community/c3249_putnam and here is a pdf with solutions to Putnam 2023: https://kskedlaya.org/putnam-archive/2023s.pdf

These are still need to be formalized in Lean which can be harder than solving the problem sometimes

Re: DeepSeek-Prover-V2

#45

Post by AlexCoventry »

samvaran wrote: post #9
simianwords wrote: post #2

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?

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.

Re: DeepSeek-Prover-V2

#46

Post by eightysixfour »

bearjaws wrote: post #42
islewis wrote: post #14

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

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 used to be part of one of the intro to engineering courses at my school - write an XX page document describing how to make a peanut butter and jelly sandwich.

Re: DeepSeek-Prover-V2

#47

Post by lugu »

bearjaws wrote: post #42
islewis wrote: post #14

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

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 is how I imagine llms are used in robotics, with one or two more levels of description.

Re: DeepSeek-Prover-V2

#49

Post by thrance »

bearjaws wrote: post #42
islewis wrote: post #14

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

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"

Re: DeepSeek-Prover-V2

#50

Post by eightysixfour »

Fokamul wrote: post #48

>"an open-source large language model" Is it really opensource? Something changed?

Everyone calls "open weight" models "open source" at this point, it is wrong, but we'll have to find another way to fight this fight. Maybe "open data and pipeline" or something.
Post reply on HN