3 ms·

I’m missing an actual explanation of how that works. I feel like we all had the idea, but how is all possible move sequences proven ? What if the possible sce

by jwpapi 17d ago

I’m missing an actual explanation of how that works. I feel like we all had the idea, but how is all possible move sequences proven ? What if the possible scenarios are too big to proof or test. Like on a 2 dimensional game it’s easy, but you could make it multidimensional and introduce an unlimited amount of special rules, (if on a prime number dimension on 3 but not more prime numbers you are allowed to jump to another prime numbers with 3 but not less coordinates) How is bend protecting it? I was checkin github and the paper, but I was not motivated enough. I feel like an actual explanation of how proofing works is missing. For Lean I understand how it works, here not.

developedby 17d ago
If your game is big, then your proof will need to be huge. It works basically the same as Lean.
LightMachine 17d ago
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 17d 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 17d 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 16d 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.

by jwpapi 17d ago

developedby 17d ago

If your game is big, then your proof will need to be huge. It works basically the same as Lean.

LightMachine 17d ago

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 17d 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 17d 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 16d 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.