4 ms·
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 tri
by ijustlovemath 2y 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
- Vecr 2y agoThankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.
- magicalhippo 2y agoSo 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 2y agoIt'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.