3 ms·

> Complexity is essential. It cannot be tamed, and there is no one big answer. The best we can do [...] is apply lots of ad hoc techniques I think this is righ

> Complexity is essential. It cannot be tamed, and there is no one big answer. The best we can do [...] is apply lots of ad hoc techniques I think this is right -- and yet wrong. In fact, I would say that it's only by accepting the correctness of this statement that we can begin to glimpse how it might be wrong. It is right that there is no one big answer that will work for any program. There is no algorithm, no language, no logic, no formalism, no decision procedure that will solve the problem, and there never will be. But I'll wager that we can get much much better at "apply[ing] lots of ad hoc techniques" -- to the point that in practice, for the programs we actually care about verifying, it will eventually be possible to automate most of the verification process even for our largest programs. If you look at what deep learning is -- to take one example of how this could happen -- it's essentially a method for generating ad hoc techniques by the zillions. When we train a network we generally neither know nor care what features it learns to detect at each layer. Each such feature detector is an ad hoc heuristic for something, but we don't even need to know what. My suspicion is that the current state of machine learning, as exciting as it is, is still in its infancy, and the techniques are going to get much more powerful yet. And the thing is, as humans, I believe we do often understand why our programs work. That means that a significant fraction of the time, we have in our heads informal correctness proofs that are actually right. I said "a significant fraction"! I am keenly aware how often we get them wrong, but I think that if we were practically never right about these things, our software wouldn't work even as well as it does. Sure, our short-term memory is minuscule, and our long-term memory unreliable. We make logic errors, we overlook corner cases by the thousands, and we simply forget required preconditions and postconditions. Anyone who writes software for a living knows how bad we are at it, and yet we can do it to a point. What we have that the machine doesn't have is an amazing pattern-matching ability. We're seeing that machines are getting a lot better at pattern matching. What the machine has that we don't is massive reliable memory and absolute indefatigability. Just to be clear, I'm not suggesting that pattern matching is all that stands between us and proving Goldbach's conjecture. (If that were true, we would have done it.) I'm saying that the proof tasks involved in verifying real-world programs are not difficult in that way. What makes them hard is not that they require great leaps of mathematical insight; a lot of them aren't even very long. (What makes them hard is, to return to the author's theme, complexity. To prove any particular fact about a large program requires figuring out what facts about the program are even relevant to one's task. Even just at the AST level, it would take many millions of facts (as relational tuples, say) to describe a large program. Naive brute-force search in a space like that would be beyond hopeless.)

pron 10y ago
> it's essentially a method for generating ad hoc techniques by the zillions But in the end, the network is just a single algorithm. Complexity theory doesn't care that from your point of view you consider it to be zillions of ad hoc techniques. Complexity theory tells us which problems are learnable and which aren't: https://en.wikipedia.org/wiki/Probably_approximately_correct_learning https://en.wikipedia.org/wiki/Probably_approximately_correct... > Anyone who writes software for a living knows how bad we are at it, and yet we can do it to a point. I agree, which is why I think that with enough empirical research there's hope (remember, the point of the talk is that math alone won't help, but empirical research might), but don't expect miracles. What we want is something that far exceeds what we think we know about our programs. That gap between what we think we know and what we actually know is where all bugs lie. > Naive brute-force search in a space like that would be beyond hopeless What complexity theory says is that knowledge comes at a price. If you want to know something you must pay that price. Your algorithm for knowing it is irrelevant. Knowing some things about programs can get really expensive, no matter the technique.
- ScottBurson 10y ago
  The PAC learning framework takes as one of its starting assumptions that the learner cannot be instructed as to the form of the answer. I think that's a stronger restriction than we need for this purpose. It's okay if we have to provide the learner with new concepts, as long as it can remember them and apply them appropriately after that. (I'm not actually sure that deep learning, at least as it exists today, is going to be particularly useful for this problem. I was just trying to come up with an example that people would be familiar with.)
  - pron 10y ago
    In the conclusion of the talk I say that the only way forward towards anything resembling a sufficiently general approach to verification. Any form of statistical analysis (which is what many current learning algorithms are) is simply an algorithmic view of that very statement. One of the attendees even asked if machine learning could assist in that empirical study, to which the answer is, of course! But it is important to understand that this is what the learning algorithms would do: empirically study human-written programs. I don't think there's currently a whole lot of research in that direction, though.

pron 10y ago

> it's essentially a method for generating ad hoc techniques by the zillions But in the end, the network is just a single algorithm. Complexity theory doesn't care that from your point of view you consider it to be zillions of ad hoc techniques. Complexity theory tells us which problems are learnable and which aren't: https://en.wikipedia.org/wiki/Probably_approximately_correct_learning https://en.wikipedia.org/wiki/Probably_approximately_correct... > Anyone who writes software for a living knows how bad we are at it, and yet we can do it to a point. I agree, which is why I think that with enough empirical research there's hope (remember, the point of the talk is that math alone won't help, but empirical research might), but don't expect miracles. What we want is something that far exceeds what we think we know about our programs. That gap between what we think we know and what we actually know is where all bugs lie. > Naive brute-force search in a space like that would be beyond hopeless What complexity theory says is that knowledge comes at a price. If you want to know something you must pay that price. Your algorithm for knowing it is irrelevant. Knowing some things about programs can get really expensive, no matter the technique.

ScottBurson 10y ago
The PAC learning framework takes as one of its starting assumptions that the learner cannot be instructed as to the form of the answer. I think that's a stronger restriction than we need for this purpose. It's okay if we have to provide the learner with new concepts, as long as it can remember them and apply them appropriately after that. (I'm not actually sure that deep learning, at least as it exists today, is going to be particularly useful for this problem. I was just trying to come up with an example that people would be familiar with.)
- pron 10y ago
  In the conclusion of the talk I say that the only way forward towards anything resembling a sufficiently general approach to verification. Any form of statistical analysis (which is what many current learning algorithms are) is simply an algorithmic view of that very statement. One of the attendees even asked if machine learning could assist in that empirical study, to which the answer is, of course! But it is important to understand that this is what the learning algorithms would do: empirically study human-written programs. I don't think there's currently a whole lot of research in that direction, though.