What does “prove the behavior” mean? If you mean “prove that it will classify this next image correctly” then of course the answer is no, although that is because it’s not even necessarily true. If you mean “prove that the program’s behavior always falls within some well-defined regime”, then yes we can absolutely prove that sort of statement. Things that are at the boundary of what we can prove (i.e. I don’t know of any existing formal tools that do it, but I’m pretty sure we could make one) would be something like “the weights of the network don’t change too much if we change the input a small amount” or “the prediction error on the training set will decrease monotonically” or “the generalization error is bounded by assuming that the test data ends up being drawn from the same distribution as the training data”.
Presumably for friendliness you want something like “P and P’ satisfy some contract relative to each other” (such as sufficiently similar behavior) which is the sort of thing we are already relatively good at proving. Here I’m imagining that P is the “old” version of a program and P’ is a “modified” version of the program that we are considering using.
What does “prove the behavior” mean? If you mean “prove that it will classify this next image correctly” then of course the answer is no, although that is because it’s not even necessarily true. If you mean “prove that the program’s behavior always falls within some well-defined regime”, then yes we can absolutely prove that sort of statement. Things that are at the boundary of what we can prove (i.e. I don’t know of any existing formal tools that do it, but I’m pretty sure we could make one) would be something like “the weights of the network don’t change too much if we change the input a small amount” or “the prediction error on the training set will decrease monotonically” or “the generalization error is bounded by assuming that the test data ends up being drawn from the same distribution as the training data”.
Presumably for friendliness you want something like “P and P’ satisfy some contract relative to each other” (such as sufficiently similar behavior) which is the sort of thing we are already relatively good at proving. Here I’m imagining that P is the “old” version of a program and P’ is a “modified” version of the program that we are considering using.