61–70 of 83 posts
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
I'm surprised those even use actual lean code instead of like raw type theory.
> 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"
> 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…
```
# Copilot Instructions
## Prompts
### General Coding
- *Boyd’s Law of Iteration: speed of iteration beats quality of iteration*: First and foremost, break every problem into smaller atomic parts. Then make a plan to start with one small part, build it, give the user an opportunity to run the code to quickly check the part works, and then move on to the next part. After all the parts are completed independently, check that they all work together in harmony. Each part should be minimal.
```
With any big problem the LLM responds first with ..... Body's Law of Iteration ..... and proceeds to break the problem into smaller parts.
I've discovered keeping file size under 300 or 400 lines helps. The AI is great at refactoring.
Earlier quoted context omitted.
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?
But a simple way to see it is that when you pick between multiple large models that have different strengths, you have a larger amount of parameters just to work with (e.g. Deepseek R1 + V3 + Qwen + LLaMA ends up being 2 trillion total parameters to pick from), whereas "picking" the experts in an MoE like has a smaller amount of total different parameters you are working with (e.g. R1 is 671 billion, Qwen is 235).
Earlier quoted context omitted.
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.
That might already happen behind what they call test time compute
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?
> 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…
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 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.
The next day we had to follow our instructions exactly in class to make the sandwich which was hilarious. A formative experience for me!
Earlier quoted context omitted.
That might already happen behind what they call test time compute
Many models that use test time compute are MoEs, but test-time compute is generally meant to refer to reasoning about the prompt/problem the model is given, not about reasoning about which model to pick, and I don't think anyone has released an LLM router under that name.