[Normal_gaussian]

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]

For mathematical research, you can just run until you have a computer checkable Lean proof.

[gf000]

Given 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]

Agreed. 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]

Sounds overengineered to me

[Normal_gaussian]

I 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.