Earlier quoted context omitted.
49/658 is 7%
Sorry, forgot multiply by 100
I bet DeepSeek-Prover-V2 wouldn't have made that mistake
DeepSeek-Prover-V2
21–30 of 83 posts
Re: DeepSeek-Prover-V2
#22related: 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.
> 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. In the future? I'm pretty sure people do that already.
No I disagree. I would want ChatGPT to abstract away expert models - biochemistry model, coding model, physics model and maybe O3 would use these models as tools to come up with an answer.
The point being that a separate expert model would be better at its own field than a single model that tries to be good at everything. Intuitively it makes sense, in practice I have seen anecdotes where finetuning a small model on domain data makes the model lose coherence on other topics.
Re: DeepSeek-Prover-V2
#23> 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…
Imo current models can already break things up into bite sized pieces. The limiter I've seen is twofold
1) Maintaining context of the overall project and goals while working in the weeds on a subtask of a task on an epic (so to speak) both in terms of what has been accomplished already and what still needs to be accomplished
and 2) Getting an agentic coding tool which can actually handle the scale of doing 50 small projects back to back. With these agentic tools I find they start projects off really strong but by task #5 they're just making a mess with every change.
I've played with keeping basically a dev-progress.md file and implementation-plan.md file that I keep in context for every request and end each task by updating files. But me manually keeping all this context isn't solving all my problems.
And all the while, tools like Cline are gobbling up 2M tokens to make small changes.
Re: DeepSeek-Prover-V2
#24related: 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.
For a concrete example today, see https://openrouter.ai/openrouter/auto
thats nice but imagine first having models that are expert in specific domains. routing seems to be the easy part (just feed the available models as tools to your wrapper LLM)
Re: DeepSeek-Prover-V2
#25The best part about these is that I know the weights are static so I know I won't have to deal with a sassy unusable update for a week suddenly.
Re: DeepSeek-Prover-V2
#26> 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…
Imo current models can already break things up into bite sized pieces. The limiter I've seen is twofold 1) Maintaining context of the overall project and goals while working in the weeds on a subtask of a task on an epic (so to speak) both in terms of what has been accomplished already and what still needs to be accomplished and 2) Getting an agentic coding tool which can actually handle the scale of doing 50 small p…
> Maintaining context of the overall project and goals while working in the weeds on a subtask of a task on an epic (so to speak) both in terms of what has been accomplished already and what still needs to be accomplished
This is a struggle for every human I’ve ever worked with
Re: DeepSeek-Prover-V2
#27The best part about these is that I know the weights are static so I know I won't have to deal with a sassy unusable update for a week suddenly.
Or, like with Claude, it being effectively lobotomized during north american 'business' hours. 3am PST? Cracked. 8am PST? ... mentally challenged.
Re: DeepSeek-Prover-V2
#28Earlier quoted context omitted.
Imo current models can already break things up into bite sized pieces. The limiter I've seen is twofold 1) Maintaining context of the overall project and goals while working in the weeds on a subtask of a task on an epic (so to speak) both in terms of what has been accomplished already and what still needs to be accomplished and 2) Getting an agentic coding tool which can actually handle the scale of doing 50 small p…
> Maintaining context of the overall project and goals while working in the weeds on a subtask of a task on an epic (so to speak) both in terms of what has been accomplished already and what still needs to be accomplished This is a struggle for every human I’ve ever worked with
Yes. I wonder if the path forward will be to create systems of agents that work as a team, with an "architect" or "technical lead" AI directing the work of more specialized execution AIs. This could alleviate the issue of context pollution as the technical lead doesn't have to hold all of the context when working on a small problem, and vice versa.
Shit. Do we need agile AI now?
Re: DeepSeek-Prover-V2
#29I 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.
Re: DeepSeek-Prover-V2
#30Earlier quoted context omitted.
> Maintaining context of the overall project and goals while working in the weeds on a subtask of a task on an epic (so to speak) both in terms of what has been accomplished already and what still needs to be accomplished This is a struggle for every human I’ve ever worked with
Yes. I wonder if the path forward will be to create systems of agents that work as a team, with an "architect" or "technical lead" AI directing the work of more specialized execution AIs. This could alleviate the issue of context pollution as the technical lead doesn't have to hold all of the context when working on a small problem, and vice versa. Shit. Do we need agile AI now?
This is kind of what the modes in roo code do now. I'm having great success with them and having them as a default just rolled out a couple days ago.
There are a default set of modes (orchestrator, code, architect, debug, and ask) and you can create your own custom ones (or have roo do it for you, which is kind of a fun meta play).
Orchestrator basically consults the others and uses them when appropriate, feeding in a sensible amount of task definition and context into the sub task. You can use different LLMs for different modes as well (I like Gemini 2.5 Pro for most of the thinking style ones and gpt o4-mini for the coding).
I've done some reasonably complicated things and haven't really had an orchestrator task creep past ~400k tokens before I was finished and able to start a new task.
There are some people out there who do really cool stuff with memory banks (basically logging and progress tracking), but I haven't played a ton with that yet.
Basic overview: https://docs.roocode.com/features/boomerang-tasks
Custom Modes: https://docs.roocode.com/features/custom-modes