undefined | Better HN

0 pointssva_1y ago0 comments

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

0 comments

ijustlovemath1y ago

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.

magicalhippo1y ago

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.

ijustlovemath1y ago

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

Vecr1y ago

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

1 more reply

j / k navigate · click thread line to collapse

0 pointssva_1y ago0 comments

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

0 comments

ijustlovemath1y ago

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

magicalhippo1y ago

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.

ijustlovemath1y ago

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

Vecr1y ago

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

1 more reply

j / k navigate · click thread line to collapse