Comment by vkazanov
2 hours ago
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?