4 ms·

I was hoping that this would have some technical insights on how automated proof repair could be improved. The ideas presented just seem a bit pie-in-the-sky.

I was hoping that this would have some technical insights on how automated proof repair could be improved. The ideas presented just seem a bit pie-in-the-sky. That said, I think the final point is the most important. Making proof repair more magical will just intensify the black-box nature of proofs to the programmer - and the more divorced specification and proof are from the people who actually write the code, the more likely that errors will slip in, not from bad code, but from bad specs instead. IMO, the most viable path forward for "proofs which repair themselves" is proofs that the average programmer can understand - at which point, their repair will be as easy as writing the code, and you wouldn't need to worry about complex self-repair techniques at all.

derefr 6y ago
> proofs that the average programmer can understand Do you believe that every computer-generated human-illegible proof has an analogous human-legible proof? It's my impression that much of the point of computational provers, is finding solutions to questions that humans would never otherwise answer in a million years, because the only proof of the conjecture (of a practical length/complexity†) is one structured in ways ill-suited to human mental processes. † There might be a human-legible proof, but at 100x or 1000x the length of the human-illegible proof. It might be beyond human capacity to ever deduce such a proof; and it would also be beyond the capacity of the algorithms used in current provers to generate it. It would be "out of reach."
- whatshisface 6y ago
  Do we have any examples of proofs that are "unsuited to human mental processes," except by being long and tedious?
  - gregorygoc 6y ago
    Long and tedious is the definition of an unsuitable human mental process.
  - jerf 6y ago
    I don't think we'd currently have any way of producing such a thing, because the two processes we have are 1. producing proofs suitable to human mental processess and 2. producing long and tedious proofs by a series of steps programmed by humans in the first place. Although it also depends to some extent on your definition of "suitable to human mental processes"... for instance, the famous proof that produced Graham's number is not "unsuitable to human mental processes" in the meta sense, but if you try to directly apprehend Graham's number with human mental processes, you fail. You can comprehend it and manipulate it mathematically, but you can not apprehend it.
  - mikedodds 6y ago
    I don't know if there are proofs unsuited to human minds, but for machine proofs, there's no essential difference between what a proof assistant like Coq can do, and what a human brain can do. Ultimately Coq boils down to a very simple core logic that could (in principle) be checked by a human. But the sheer scale of such proofs means they can't be meticulously checked. Proof tools are just the same as e.g. compilers - they can do things humans can't do because to do so would be so incredibly time consuming and tedious.
  - jacobr1 6y ago
    An analogy might be chess with derided "computer moves." The aren't necessarily more complex that existing human heuristics, especially at the grandmaster level, but they lack at least one of several traditional "aesthetic" attributes. I'm not all that familiar with generated proofs, but from those I've seen, they will point our pedantic linkages other proofs might avoid. I suspect that can easily be overcome though be building-in aesthetic conventions in the proof presentation layer, such as we do today with ASTs and compiler optimizations. Wild speculation: automated proofs use assembly constructs and goto's when they could be using higher order constructs - but this isn't always clear because there isn't a separation of abstraction layers (or a least a a clearly articulated one). I could imagine a project that regenerated many well known proofs (these exist in form in the solvers already, but these are intentionally redone) without some of the existing heuristics abridgments that exist in the solvers. Then pair them with the human curated proofs of oft-considered elegance and train a system to convert from one to the other.
    - Someone 6y ago
      “An analogy might be chess with derided "computer moves." The aren't necessarily more complex that existing human heuristics, especially at the grandmaster level, but they lack at least one of several traditional "aesthetic" attributes.” I think there’s a possibility that’s cultural. Generations of chess players grew up learning certain heuristics. Now, computers show those heuristics aren’t as good as we thought they were. It’s possible that new generations, trained more by computers than by older generations of chess players, will develop new heuristics. You see something similar in math. Sometimes, when a human discovers a new way to look at a problem, whole avenues of proofs open up, and what was incomprehensible becomes much easier not only for that human, but also for those learning about his work. On the other hand, I think computers sometimes make moves humans won’t make because they don’t have any notion of fear. When humans get into a minefield position where almost every move is clearly losing, but that do have one winning path through it, they may not choose that path even if they see it because they fear they’re overlooking something.
  - Penyngton 6y ago
    Here <https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext https://cacm.acm.org/magazines/2017/8/219606-the-science-of-...> is an article about a computer-generated proof of a combinatorial problem in number theory. Although you could characterise the proof as "just long", I think that the article may offer a different perspective on why proofs of this nature are interesting and useful.
- ivanbakel 6y ago
  It's my belief that the large part of computer-generated proving, and the overwhelming majority of formal verification of programs, revolves around proofs that humans would easily understand. While there are examples of mechanised proofs that reach the "limits" of human proof, they do so in domains where computers are good and humans are less good, like exhaustiveness checks for e.g. the four-colour theorem. It should be pointed out that automatic provers are surprisingly stupid. Exhaustive searches do not scale well for large and complicated proofs, and computers obviously lack the "intuition" that mathematicians lean on to prove. Lots of the work that goes into computer-assisted proofs is just bookwork for properties that humans would consider trivial. Even the OP's article is not concerned with computers generating proofs automatically (though lots of work has gone into that, especially w.r.t. code), but instead with computers repairing human-written proofs to persist them across small changes. The thing that most certainly argues that the proofs involved in the formal verification of software are within human reach is simply that humans make such ad-hoc proofs all the time - because they are very similar to the non-formal specifications that humans use to write code in the first place. Any programmer who can argue why their code runs correctly is most of the way towards a proof of its correctness - the real obstacle is not the complexity of the resulting proof, but the tediousness of its expression.
- lmm 6y ago
  Every design property of a human-created program likely has a human-legible proof. The program doesn't have that property by accident, a human wanted it to have that property and understood on some level how to make it have that property.
tlringer 6y ago
These problems are more closely related than you imagine. In particular, when you change a program, there is often necessarily more information you must give the computer in order to make the corresponding change in the proof. That additional burden is creativity, and is in many cases unavoidable. With good proof repair techniques you can fix the proof almost fully automatically in a way that mimics the change in the program, but then just ask the programmer a few questions to give the needed creativity to fix the proofs. As far as easy to understand goes, then, that "just" comes down to good UX for asking those questions. (Still not solved!) Here is the state of the art right now (my most recent paper): https://arxiv.org/abs/2010.00774 https://arxiv.org/abs/2010.00774 Lots left to do but the dream is quite realistic.
mikedodds 6y ago
Author here. This post is definitely more of a problem statement than a solution. I don't think this area gets enough attention and I'd like more people to think about it! However, I think there are some good reasons to think solving this is possible. E.g. Galois have had proofs in CI at AWS for several years that rerun on code changes - you can read about our approach here: https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26 https://link.springer.com/chapter/10.1007/978-3-319-96142-2_.... And elsewhere in the comments Talia Ringer posted about her research, which is very promising as well. I think there's a tight connection between 'proofs the programmer can understand' and self-repair / automation. The aim should really be to clear away a lot of the scaffolding that's currently needed and hand it off to solvers, and leave programmers to do what they are best at, i.e. understand the meaning of the code. Type checking is a great example of a lightweight formal method that disguises most of the sophisticated automation hiding behind the scenes.
- cocoafleck 6y ago
  I feel obligated to point out that there are tools that effectively repair broken proofs, but they just aren't labeled as such. For example, Frama-C is a program that takes in a simplified written proof (in a C comment language), and then validates it (as in the tedious middle steps) with z3, cvc4, etc. Unfortunately, Frama-C can't handle dynamic memory yet, and it doesn't handle array sizes correctly forcing for loops over memcpys in some cases if you want to prove anything. I wouldn't recommend it for actual usability, but it does seem to "repair" proofs (as in they were never non-broken/whole in the first place).

derefr 6y ago

> proofs that the average programmer can understand Do you believe that every computer-generated human-illegible proof has an analogous human-legible proof? It's my impression that much of the point of computational provers, is finding solutions to questions that humans would never otherwise answer in a million years, because the only proof of the conjecture (of a practical length/complexity†) is one structured in ways ill-suited to human mental processes. † There might be a human-legible proof, but at 100x or 1000x the length of the human-illegible proof. It might be beyond human capacity to ever deduce such a proof; and it would also be beyond the capacity of the algorithms used in current provers to generate it. It would be "out of reach."

whatshisface 6y ago
Do we have any examples of proofs that are "unsuited to human mental processes," except by being long and tedious?
- gregorygoc 6y ago
  Long and tedious is the definition of an unsuitable human mental process.
- jerf 6y ago
  I don't think we'd currently have any way of producing such a thing, because the two processes we have are 1. producing proofs suitable to human mental processess and 2. producing long and tedious proofs by a series of steps programmed by humans in the first place. Although it also depends to some extent on your definition of "suitable to human mental processes"... for instance, the famous proof that produced Graham's number is not "unsuitable to human mental processes" in the meta sense, but if you try to directly apprehend Graham's number with human mental processes, you fail. You can comprehend it and manipulate it mathematically, but you can not apprehend it.
- mikedodds 6y ago
  I don't know if there are proofs unsuited to human minds, but for machine proofs, there's no essential difference between what a proof assistant like Coq can do, and what a human brain can do. Ultimately Coq boils down to a very simple core logic that could (in principle) be checked by a human. But the sheer scale of such proofs means they can't be meticulously checked. Proof tools are just the same as e.g. compilers - they can do things humans can't do because to do so would be so incredibly time consuming and tedious.
- jacobr1 6y ago
  An analogy might be chess with derided "computer moves." The aren't necessarily more complex that existing human heuristics, especially at the grandmaster level, but they lack at least one of several traditional "aesthetic" attributes. I'm not all that familiar with generated proofs, but from those I've seen, they will point our pedantic linkages other proofs might avoid. I suspect that can easily be overcome though be building-in aesthetic conventions in the proof presentation layer, such as we do today with ASTs and compiler optimizations. Wild speculation: automated proofs use assembly constructs and goto's when they could be using higher order constructs - but this isn't always clear because there isn't a separation of abstraction layers (or a least a a clearly articulated one). I could imagine a project that regenerated many well known proofs (these exist in form in the solvers already, but these are intentionally redone) without some of the existing heuristics abridgments that exist in the solvers. Then pair them with the human curated proofs of oft-considered elegance and train a system to convert from one to the other.
  - Someone 6y ago
    “An analogy might be chess with derided "computer moves." The aren't necessarily more complex that existing human heuristics, especially at the grandmaster level, but they lack at least one of several traditional "aesthetic" attributes.” I think there’s a possibility that’s cultural. Generations of chess players grew up learning certain heuristics. Now, computers show those heuristics aren’t as good as we thought they were. It’s possible that new generations, trained more by computers than by older generations of chess players, will develop new heuristics. You see something similar in math. Sometimes, when a human discovers a new way to look at a problem, whole avenues of proofs open up, and what was incomprehensible becomes much easier not only for that human, but also for those learning about his work. On the other hand, I think computers sometimes make moves humans won’t make because they don’t have any notion of fear. When humans get into a minefield position where almost every move is clearly losing, but that do have one winning path through it, they may not choose that path even if they see it because they fear they’re overlooking something.
- Penyngton 6y ago
  Here <https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext https://cacm.acm.org/magazines/2017/8/219606-the-science-of-...> is an article about a computer-generated proof of a combinatorial problem in number theory. Although you could characterise the proof as "just long", I think that the article may offer a different perspective on why proofs of this nature are interesting and useful.
ivanbakel 6y ago
It's my belief that the large part of computer-generated proving, and the overwhelming majority of formal verification of programs, revolves around proofs that humans would easily understand. While there are examples of mechanised proofs that reach the "limits" of human proof, they do so in domains where computers are good and humans are less good, like exhaustiveness checks for e.g. the four-colour theorem. It should be pointed out that automatic provers are surprisingly stupid. Exhaustive searches do not scale well for large and complicated proofs, and computers obviously lack the "intuition" that mathematicians lean on to prove. Lots of the work that goes into computer-assisted proofs is just bookwork for properties that humans would consider trivial. Even the OP's article is not concerned with computers generating proofs automatically (though lots of work has gone into that, especially w.r.t. code), but instead with computers repairing human-written proofs to persist them across small changes. The thing that most certainly argues that the proofs involved in the formal verification of software are within human reach is simply that humans make such ad-hoc proofs all the time - because they are very similar to the non-formal specifications that humans use to write code in the first place. Any programmer who can argue why their code runs correctly is most of the way towards a proof of its correctness - the real obstacle is not the complexity of the resulting proof, but the tediousness of its expression.
lmm 6y ago
Every design property of a human-created program likely has a human-legible proof. The program doesn't have that property by accident, a human wanted it to have that property and understood on some level how to make it have that property.

tlringer 6y ago

These problems are more closely related than you imagine. In particular, when you change a program, there is often necessarily more information you must give the computer in order to make the corresponding change in the proof. That additional burden is creativity, and is in many cases unavoidable. With good proof repair techniques you can fix the proof almost fully automatically in a way that mimics the change in the program, but then just ask the programmer a few questions to give the needed creativity to fix the proofs. As far as easy to understand goes, then, that "just" comes down to good UX for asking those questions. (Still not solved!) Here is the state of the art right now (my most recent paper): https://arxiv.org/abs/2010.00774 https://arxiv.org/abs/2010.00774 Lots left to do but the dream is quite realistic.

mikedodds 6y ago

Author here. This post is definitely more of a problem statement than a solution. I don't think this area gets enough attention and I'd like more people to think about it! However, I think there are some good reasons to think solving this is possible. E.g. Galois have had proofs in CI at AWS for several years that rerun on code changes - you can read about our approach here: https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26 https://link.springer.com/chapter/10.1007/978-3-319-96142-2_.... And elsewhere in the comments Talia Ringer posted about her research, which is very promising as well. I think there's a tight connection between 'proofs the programmer can understand' and self-repair / automation. The aim should really be to clear away a lot of the scaffolding that's currently needed and hand it off to solvers, and leave programmers to do what they are best at, i.e. understand the meaning of the code. Type checking is a great example of a lightweight formal method that disguises most of the sophisticated automation hiding behind the scenes.

cocoafleck 6y ago
I feel obligated to point out that there are tools that effectively repair broken proofs, but they just aren't labeled as such. For example, Frama-C is a program that takes in a simplified written proof (in a C comment language), and then validates it (as in the tedious middle steps) with z3, cvc4, etc. Unfortunately, Frama-C can't handle dynamic memory yet, and it doesn't handle array sizes correctly forcing for loops over memcpys in some cases if you want to prove anything. I wouldn't recommend it for actual usability, but it does seem to "repair" proofs (as in they were never non-broken/whole in the first place).