Well, apparently we do have a non-deterministic black box that is pretty good at coming up with a bunch of heuristics ideas, and we also have a deterministic process to validate those ideas!
That's why I think getting formal verification "right" with LLMs will be huge.
>> Well, apparently we do have a non-deterministic black box that is pretty good at coming up with a bunch of heuristics ideas, and we also have a deterministic process to validate those ideas!
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.
Well, it doesn't have to be novel, does it? Most of the real life problems are probably related to an already solved issue, so intelligent (probabilistic) recall is fruitful, even if it's "unoriginal".
Yes, it does. There are tons of things that we don't know how to get e.g. robots to do in the physical world and it seems that animals have a library of heuristics that let them do them cheaply and accurately. We totally want to be able to learn those heuristics of search for them and find them somehow.
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.
I honesty don't quite know what you argue about. That LLMs are not AGI? Of course not!
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.
That's why I think getting formal verification "right" with LLMs will be huge.