That's why I think getting formal verification "right" with LLMs will be huge.
Do we? When have LLMs come up with heuristics? I'm sure if you ask an LLM to tell you e.g. how to solve a maze it will print out the instructions for the follow-the-left-wall heuristic, but that's not "coming up" with a heuristic.
I fear though we are about to go into one of those unproductive conversations about the capabilities of LLMs to produce novel results which I think has now reached saturation point all over the internets.
And that's why my point was that we don't know how to come up with heuristics: because we currently don't.
Edit: if you mean that we can probabilistic-recall all those heuristics, that's not right. Because such heuristics are tacit knowledge that is very difficult, maybe even impossible, to articulate with enough accuracy to reproduce in a computer. We certainly can't get LLMs to learn them from the web because the web doesn't have text that explains e.g. how to control your muscles to climb a tree.
But this is a thread about a formal verification language, and in this area "just throwing non-deterministic proofs at it until something sticks" works kinda well.
And you just sort of said that something getting "figured out" by a random process with selection can't be a heuristic, as it has to be "novel" (whatever that means). Well, then unfortunately we have to exclude animals from that list as well, because if you read it again, that's pretty much how evolution works.