3 ms·
Commands like /goal and similar are the more complex version of this; you write a prompt like it was a singular iteration, it runs one iteration, then runs an "
by Normal_gaussian 2mo ago
Commands like /goal and similar are the more complex version of this; you write a prompt like it was a singular iteration, it runs one iteration, then runs an "evaluator" to determine if the goal has been reached, then runs the prompt again with a little extra to make it go again - and so on. The evaluator is just an LLM with most of the result or context looking at the original goal and the state and answering the question "has the goal been met".
The interesting part of this: while some leading implementations use the same LLM and context for the evaluator, some call out to a different context, some to a tuned LLM and different context; so which is better? many blog-scale benchmarks are calling it a toss-up that is highly dependent on the primary model.
- eru 2mo agoFor mathematical research, you can just run until you have a computer checkable Lean proof.
- gf000 2mo agoGiven that it was formalized correctly, which is far from trivial in many cases (Of course LLMs can help there, get it right etc, just a caveat that people have to keep in mind)
- eru 2mo agoAgreed. But also formalising the statement of a theorem, or rather understanding the formalisation that the LLM suggested to you, is often a lot easier than understand the whole proof, especially if it's a formal proof.
- xyzsparetimexyz 2mo agoSounds overengineered to me
- Normal_gaussian 2mo agoI was surprised at how little improvement they could eek out of tuning it; but it is a non-trivial improvement which is much less likely to wastefully spin if your validation is more expensive than you realise. Makes sense that its in the major harnesses and not the self-built ones.