[sva_]

> if baked deep into an ML's kernel/structure/training process

Not sure of the feasibility of implementing lean as a GPU kernel, if you meant that. Also I'm not sure it makes sense to run Lean inside the (mostly matmul) training process. Now to use it to prepare some training data, it seems more realistic. But that seems to be what AlphaProof tries to do in the reinforcement step, if I'm not mistaken.

[ijustlovemath]

I think that in order for it to truly find deep insights, it would need to do more than just generate training data. I'm also a believer that the current AI approaches are approaching their limits as the human feed dries up and we start using old models to train new ones.

Of course, what that really means and how you'd go about adapting your CUDA code / hardware, would have to be researched.

[magicalhippo]

It could perhaps also be used to guide the sampling step at the end, or? Similar to those syntax-constrained samplers to ensure the LLM spits out eg valid JSON.

[ijustlovemath]

Syntax constraints are usually expressible as grammars, but the language of math is often very unique and domain specific, which makes this kind of approach tricky to get right

[Vecr]

Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.

[magicalhippo]

So yea that was my thought. Use it to spit out valid Lean syntax, and potentially also to backtrack if it outputs inconsistent or erroneous proofs.

[namibj]

It's fairly good at valid syntax already, and did the backtracking for a long time due to it doing tree search guided by it's predictions for how likely that tactic will end up finishing the tree leaf it's applied to.