The trouble is when you want to do that in the general case, i.e. when you don't know the problem you're solving. Unfortunately we don't know how to come up with heuristics automatically.
... well ish. We have relaxations in Planning again, but that really doesn't seem to have anything to do with what bend is doing.
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.
A bit of a contrived example, but let's say that the user starts at (0,0) and that all the four directions' movement will step 2. Then we can prove that all four directions will keep both the x and y coordinates' parity.
Now we apply the former theorem to our start position and can then conclude that after any number of steps the user will be on even x y coordinates. Now if the flag is on an odd coordinate we have proven that there is no way to get there, without searching the whole space.
For a less contrived example, it is also possible to work backwards from the goal, etc. The hard part of formal verification in general is that the proofs are closely coupled to the program code itself, so a different representation of state may make proving it more or less difficult to prove. And also code changes can easily break proofs, as the core of these languages is basically normalizing every expression to the max and comparing them (at that point basically programs) for equality.