4 ms·

>> Induction is the one trick that makes all of mathematics (as we know it) possible, and it also applies to software. So, for example, to prove that no move le

>> Induction is the one trick that makes all of mathematics (as we know it) possible, and it also applies to software. So, for example, to prove that no move leads to an invalid state, we prove that the initial state is valid, and then prove that, given a valid state, applying any event won't return an invalid state. That sounds like, for the grid navigation game in the example, in order to prove that no move leads from the initial state to an invalid state you'd have to search the set of all move sequences to find out if one of them leads to an invalid state. We know from Planning & Scheduling that this is a PSPACE-complete task. So that's ... not what you mean, right?

gf000 8d ago
Not the parent, but that's not the only way to prove stuff, depending on the exact configuration. 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.
- YeGoblynQueenne 8d ago
  Oh yes, if you know what problem you're trying to solve you can come up with clever ways to solve it cheaply: a heuristic. 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.
  - gf000 7d ago
    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.
    - YeGoblynQueenne 7d ago
      >> 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.
      - gf000 6d ago
        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".
        YeGoblynQueenne 5d ago
        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.

gf000 8d ago

Not the parent, but that's not the only way to prove stuff, depending on the exact configuration. 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.

YeGoblynQueenne 8d ago
Oh yes, if you know what problem you're trying to solve you can come up with clever ways to solve it cheaply: a heuristic. 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.
- gf000 7d ago
  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.
  - YeGoblynQueenne 7d ago
    >> 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.
    - gf000 6d ago
      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".
      - YeGoblynQueenne 5d ago
        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.