3 ms·

You can prove infinitely many cases by induction. It works like this: if you prove that a property about natural numbers holds for 0, and if you also prove tha

You can prove infinitely many cases by induction. It works like this: if you prove that a property about natural numbers holds for 0, and if you also prove that, assuming the property holds for N, it also holds for N+1; then, you can conclude the property holds for every N, up to infinity. This is a bit of a mouthful, but the logic holds. 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. And that's it actually. Of course, once you have an app with hundreds of actions, proving that no action leads to an invalid state requires a lot of these "induction arguments". But not infinitely many, because there is a finite amount of "infinite paths" that a real software can take. So, that's what the AI does. It proves, by induction, that none of these "infinite paths" that an app can take leads to an invalid state. And this convinces the compiler that invalid states are impossible. Theorem proving in Bend is a dance between the prover (the model) and the compiler (the checker); a machine trying to convince another machine about properties of infinite states. And that's is kinda poetic, don't you think?

YeGoblynQueenne 16d ago
>> 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 16d 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 15d 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 15d 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 15d 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 14d 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 13d ago

YeGoblynQueenne 16d ago

>> 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 16d 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 15d 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 15d 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 15d 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 14d 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 13d ago