Comment by tossandthrow
4 hours ago
Llm systems are not really build for adhering to a grammar (other than "a string og tokens").
It is also not clear whether the llm adhering to a grammar is necessary for intelligent agents.
Certainly,a harness can easily correct for it.
Someone build a chess harness already...
It seems absolutely crazy to me to expect an LLM to code a solution to a problem while also not expecting it to be able to adhere to a grammar.
How much support do we as humans need to get rules right?
I'm an expert in my field, read my comments, my gramma is shit.
Why?
You might never have tried to program before, so I don't blame it on you.
But most programmers, even experienced ones, see grammar and type errors regularly.
By the promise of it, llms should be able to both adhere to grammars, or go free form where necessary. I mean, doing math is supposed to be strict but in practice it's a somewhat educated random walk in the space of correct lean theorems.
Harnesses do correct things, sure.
You are right. I am imprecise.
Languages allow a certain flexibility in their grammars - you can read a sentence without that adhering it exactly to the grammar.
Games and programming languages (including lean) does not allow this flexibility.
A very intelligent person would likely also reason in terms of probably outcomes before correcting a statement to adhering entirely to the grammar.
Certainly it must be like that, otherwise reviews in math was rendered moot.
Do we blame research mathematicians for not adhering to the grammar?