How does the MCTS distinguish between 'generated a stupid lemma that is true' and 'generated a valid lemma'?
Is there any reason to expect that a 'good' partial subtree will result in a 'good' output?
Why do you think this approach will generate valid lemmas?
(Not structurally valid; valid as in, they assert a solution to the given problem).
It seeeems a lot like going like this:
"Generate me a function for X and a bunch of tests that verify X".
"If the tests pass, the function is good"
...but, there's no specific reason to expect that to be true?
How is what you're doing different?
Clearly (from the examples) in a trivial case, it is true, but generally speaking as the task complexity increases, this type of 'auto validation' seems to struggle...?
Using grammars to generate a structured output seems like a similar (and successful) approach, used by many people, but because it doesn't have the associated auto-validation, it's robust against LLM randomness.
I guess I'm struggling to see how this is superior / novel to existing approaches in that space.