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

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

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

reply
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?

reply