9 ms·

Certigrad: bug-free machine learning on stochastic computation graphs

99 points by kg9000 9y ago

binarymax 9y ago
Meta to the Certigrad project, for those mystified by the 'lean' programming language, here is a good start: https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf https://leanprover.github.io/programming_in_lean/programming...
- taneq 9y ago
  PDF warning for those of us on mobile.
deleted 9y ago
[deleted]
alimw 9y ago
Previous discussion of the associated paper: https://news.ycombinator.com/item?id=14658832 https://news.ycombinator.com/item?id=14658832
taneq 9y ago
I find the appeal of formally proven languages somewhat confusing. All you're doing is moving the bugs from the source code to the specification. (Alternately, you can think of source code as a 'specification' for a compiled program. You still have to transfer the same amount of information to the computer.)
- ogdan 9y ago
  The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct.
  - fchollet 9y ago
    How is that the case in this specific example? It looks a lot harder to check for correctness.
    - dselsam 9y ago
      > The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct. >> How is that the case in this specific example? It looks a lot harder to check for correctness. Author here. Here is the specification for the stochastic backpropagation algorithm: https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#L13-L25 https://github.com/dselsam/certigrad/blob/master/src/certigr... The preconditions do not need to be inspected carefully because we prove that the models of interest satisfy them (example: https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/grads_correct.lean#L20-L27 https://github.com/dselsam/certigrad/blob/master/src/certigr...) Here is the part of the specification that needs to be inspected carefully: https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#L23-L25 https://github.com/dselsam/certigrad/blob/master/src/certigr... The syntax may seem strange to those unfamiliar with Lean, and a few of the functions involved may not be self-explanatory without reading their definitions, but the statement is conceptually simple: the stochastic backpropagation algorithm correctly computes unbiased estimates of the gradient of the expected loss. It is subjective, but I personally think that this specification is vastly easier to understand and to check for correctness than the actual implementation of the stochastic backpropagation algorithm.
  - xgk 9y ago
    specification is a lot smaller than the code I doubt that this is the case in general. How can the (full) specification of a program be smaller than the program? This would mean we can always compress a program into a smaller program (after all a specification can be seen as another program -- alternatively a program can be seen as its own specification).
    - wizeman 9y ago
      It's not true for all cases, but it's true for most real-world cases, especially for typical combinations of specification tools and traditional (imperative) programming languages. A real-world program is usually more complex and intricate than a specification, often a lot more complex. This is usually done in the interest of optimization / performance, so that you program runs at least somewhat efficiently. A specification is usually a lot simpler, because typically you only need to express the simplest possible way to do or to describe something. Even if the specification ends up looking like a very simple, naive and horribly inefficient program to a typical programmer, it doesn't matter: it's not going to be executed, it's only going to be used to prove that your program behaves in the same way, even though your program can be arbitrarily more complex. Also, in your specification, sometimes you don't even need to express how to do something - you only need to express what the result looks like. For example, let's say you want to prove that a sorting algorithm is implemented correctly. You literally only have to specify "after running the function sort() on an array, the resulting array is sorted. A sorted array means that for any X and Y elements of the array, if the index of X is less than the index of Y, then the value of X is less than or equal to the value of Y". It's easy to see how that specifies correct sorting behavior, even though it doesn't even say how the sorting is supposed to be done. In contrast, the actual implementation of the sorting algorithm can be way more complex or difficult to see that is correct than that, especially if your program is written in a programming language prone to errors, with pointer manipulation and potential undefined behavior (such as C, for instance).
      - xgk 9y ago
        A specification is usually a lot simpler, because ... I used to think that too, but after verifying some algorithms, I have become sceptical of that belief. Instead I conjecture that on average the full specification of an algorithm is at best proportional in length to the algorithm itself. There are two main issues: - Most verification does not tackle the full specification, but rather some aspect. - Verification needs many intermediate specifications (e.g. induction hypotheses in proofs), which need to be accounted for. I'm happy to be convinced otherwise. prove that a sorting algorithm is I produced the full verification of Quicksort (probably the first), and I needed to produce a large amount of intermediate specifications for auxiliary lemmas. The full specification was much longer than the algorithm.
- Eridrus 9y ago
  You have to make sure your spec is right, but you also have to make sure your tests are right, and people are pretty happy with the idea of testing.
  - taneq 9y ago
    Yeah, I'm not saying that automated testing (whether through unit tests or through theorem proving) is bad, just that the two approaches seem pretty much equivalent. All these strong claims about "proven correctness" get thrown about but I'm not sure it's very useful when all you're proving is that the computer did what you told it (which you know anyway - the problem is almost invariably that you told it to do the wrong thing.)
    - jroesch 9y ago
      They are fundamentally not equivalent, you can not guarantee that a system respects a safety property with testing. You can prove that certain concrete instances, i.e your test cases inputs are safe, but you don't know where there exists a path in your program where the safety property is violated. This is incredibly important in critical systems because it might not be possible to even detect a safety violation has occurred, for example file system corrupts data, distributed consensus algorithm commits to the wrong value, compiler slightly mis compiles your code. We want to be ensure there exists no path where something "bad" can occur, this is what verification gives us over testing. There is always the fundamental problem of needing to communicate what we want to the computer, but the goal is to do it minimal way, and then ensure the program we write exactly matches the minimal implementation.
- dselsam 9y ago
  > All you're doing is moving the bugs from the source code to the specification. The value of doing this can vary, but there are some cases in which the gain is immense and indisputable. Suppose you are writing a compiler optimization. Your source code could be arbitrarily complicated, but your specification is simply "an optimized program always behaves the same as the original".
  - taneq 9y ago
    Are things like "the output must be equal to the output of this other thing" easily expressed to a prover? If so this seems like it'd be awesome for optimisation as well.
    - dselsam 9y ago
      Yes, this is easy to express in a prover. A naive implementation can always serve as a specification for a sophisticated one.
      - eriknstr 9y ago
        This sounds very interesting indeed. Can this be done with Coq? Do you have any tutorials or such on doing this?
        wizeman 9y ago
        It can definitely be done with Coq. The typical recommendation is to read through and do the exercises in the freely-available Software Foundations book [1], which will teach you how to do that in Coq. That said, while it was educational and an extremely good introduction to interactive theorem proving, as I went through the book I became increasingly disappointed with how Coq-style proofs were so laborious and difficult to achieve, as often you had to prove even the simplest things step by step. You also had to go through many chapters before you finally arrived at proving correctness of optimization. I later found an alternative which I can't recommend highly enough. If you read through and do the exercises in the also freely-available Concrete Semantics book [2], you will also learn how to do exactly what you want, but you will learn it much sooner and in a much easier way. In the latter book, you will be using the Isabelle/HOL prover instead of the Coq prover, though. The language looks slightly more idiosyncratic (I'm referring to the weird extra quotes - you will know what I mean), but despite that, to me it was worth a hundred times over: Isabelle/HOL has the most amazing proof automation I've seen - it will not only find proofs all by itself quite often, automatically using hundreds of theorems it already knows or that you have already proved before, but sometimes it will even automatically spit out human-readable proofs, which will teach you how the proof can be done (which is useful when you are stumped and had no clue how to move forward). Isabelle/HOL can also be configured to automatically find errors in your specification and in your implementation - it has built-in automatic quickcheck / nitpick functionality, which can often tell you that you're trying to prove something that is not provable even before you attempt to prove it. IMHO, all of these things contribute to a significantly better user experience (as a newbie, at least). If you are interested, give it a try. I highly recommend it! [1] https://softwarefoundations.cis.upenn.edu/current/index.html https://softwarefoundations.cis.upenn.edu/current/index.html [2] http://concrete-semantics.org/ http://concrete-semantics.org/
- nickpsecurity 9y ago
  You used to have bugs in the ambiguous requirements in English, any formal specs which are precise, and the code. Formal specifications plus verification does indeed mostly move bugs to the formal specs or proofs. That mostly eliminates two classes of bugs. Then, it ensures that your extracted or verified code probably corresponds to your specs. It might even been proven free of (common errors here). With certifying compiler, the ML or C code might also be proven to compile to assembly without errors. Quite a bit of improvement there. Developer is not just moving things on a ledger. That developer is preventing entire classes of problems plus reducing problems in what remains.
- emmab 9y ago
  > You still have to transfer the same amount of information to the computer. Different target languages to transfer the information to may result in somewhat uncorrelated defects, allowing finding defects through mutual comparison. You can test a generator by writing a recognizer and vice versa. Errors in formal proof of correctness are somewhat uncorrelated with errors made in tests and errors made in implementation. By doing all 3 you can diversify to reduce risk.
gtani 9y ago
This seems to be a newly hot topic, whether to fight adversarial inputs or looking for efficiencies. I bookmarked a few relevant blogs (but really need to read more deeply) http://composition.al/blog/2017/05/31/proving-that-safety-critical-neural-networks-do-what-theyre-supposed-to-where-we-are-where-were-going-part-2-of-2/ http://composition.al/blog/2017/05/31/proving-that-safety-cr... http://www.cleverhans.io/security/privacy/ml/2017/06/14/verification.html http://www.cleverhans.io/security/privacy/ml/2017/06/14/veri... https://blog.foretellix.com/ https://blog.foretellix.com/ and another preprint: https://arxiv.org/abs/1706.10268 https://arxiv.org/abs/1706.10268
pkay 9y ago
> Note: building Certigrad currently takes ~15 minutes and consumes ~7 GB of memory. Why does it take so long and use so much memory?
- dselsam 9y ago
  Author here. Building Certigrad involves replaying all tactic scripts in the entire project to reconstruct all of the formal proofs, and then checking each of the formal proof objects in Lean's small trusted kernel. Proving (and checking) the main correctness theorem for stochastic backpropagation is very fast. The vast majority of the time and memory is spent verifying that a specific machine learning model (AEVB) satisfies all the preconditions for backprop. This involves proving several technical conditions, e.g. that various large terms are (uniformly) integrable. We have not experimented much with simplification strategies, and there is probably a lot of room for improvement in bringing these numbers down. It would also be good to provide an option to build the system without reconstructing the proofs; checking the proofs is analogous to running the entire test suite, and most users do not do this for every tool they build.
  - xgk 9y ago
    Could this problem have been (partly) avoided by going for an LCF-based prover such as HOL or Isabelle/HOL, rather than a system based on the Curry-Howard correspondence?
    - dselsam 9y ago
      I do not even know how I would have built Certigrad in Isabelle/HOL in the first place. In my first attempt to build Certigrad, I used a non-dependent type for Tensors (T : Type), and I accumulated so much technical debt that I eventually gave up and started again with a dependent type for tensors (T : Shape -> Type). This was my only major design error in the project, and development went smoothly once I made this change.
      - xgk 9y ago
misterAxiom 9y ago
> Machine learning systems are also difficult to engineer because it can require substantial expertise in mathematics (e.g. linear algebra, statistics, multivariate analysis, measure theory, differential geometry, topology) to even understand what a machine learning algorithm is supposed to do and why it is thought to do it correctly. It's like Teen Talk Barbie.

99 points by kg9000 9y ago

Meta to the Certigrad project, for those mystified by the 'lean' programming language, here is a good start: https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf https://leanprover.github.io/programming_in_lean/programming...

taneq 9y ago
PDF warning for those of us on mobile.

deleted 9y ago

[deleted]

alimw 9y ago

Previous discussion of the associated paper: https://news.ycombinator.com/item?id=14658832 https://news.ycombinator.com/item?id=14658832

taneq 9y ago

I find the appeal of formally proven languages somewhat confusing. All you're doing is moving the bugs from the source code to the specification. (Alternately, you can think of source code as a 'specification' for a compiled program. You still have to transfer the same amount of information to the computer.)

ogdan 9y ago
The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct.
- fchollet 9y ago
  How is that the case in this specific example? It looks a lot harder to check for correctness.
  - dselsam 9y ago
    > The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct. >> How is that the case in this specific example? It looks a lot harder to check for correctness. Author here. Here is the specification for the stochastic backpropagation algorithm: https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#L13-L25 https://github.com/dselsam/certigrad/blob/master/src/certigr... The preconditions do not need to be inspected carefully because we prove that the models of interest satisfy them (example: https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/grads_correct.lean#L20-L27 https://github.com/dselsam/certigrad/blob/master/src/certigr...) Here is the part of the specification that needs to be inspected carefully: https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#L23-L25 https://github.com/dselsam/certigrad/blob/master/src/certigr... The syntax may seem strange to those unfamiliar with Lean, and a few of the functions involved may not be self-explanatory without reading their definitions, but the statement is conceptually simple: the stochastic backpropagation algorithm correctly computes unbiased estimates of the gradient of the expected loss. It is subjective, but I personally think that this specification is vastly easier to understand and to check for correctness than the actual implementation of the stochastic backpropagation algorithm.
- xgk 9y ago
  specification is a lot smaller than the code I doubt that this is the case in general. How can the (full) specification of a program be smaller than the program? This would mean we can always compress a program into a smaller program (after all a specification can be seen as another program -- alternatively a program can be seen as its own specification).
  - wizeman 9y ago
    It's not true for all cases, but it's true for most real-world cases, especially for typical combinations of specification tools and traditional (imperative) programming languages. A real-world program is usually more complex and intricate than a specification, often a lot more complex. This is usually done in the interest of optimization / performance, so that you program runs at least somewhat efficiently. A specification is usually a lot simpler, because typically you only need to express the simplest possible way to do or to describe something. Even if the specification ends up looking like a very simple, naive and horribly inefficient program to a typical programmer, it doesn't matter: it's not going to be executed, it's only going to be used to prove that your program behaves in the same way, even though your program can be arbitrarily more complex. Also, in your specification, sometimes you don't even need to express how to do something - you only need to express what the result looks like. For example, let's say you want to prove that a sorting algorithm is implemented correctly. You literally only have to specify "after running the function sort() on an array, the resulting array is sorted. A sorted array means that for any X and Y elements of the array, if the index of X is less than the index of Y, then the value of X is less than or equal to the value of Y". It's easy to see how that specifies correct sorting behavior, even though it doesn't even say how the sorting is supposed to be done. In contrast, the actual implementation of the sorting algorithm can be way more complex or difficult to see that is correct than that, especially if your program is written in a programming language prone to errors, with pointer manipulation and potential undefined behavior (such as C, for instance).
    - xgk 9y ago
      A specification is usually a lot simpler, because ... I used to think that too, but after verifying some algorithms, I have become sceptical of that belief. Instead I conjecture that on average the full specification of an algorithm is at best proportional in length to the algorithm itself. There are two main issues: - Most verification does not tackle the full specification, but rather some aspect. - Verification needs many intermediate specifications (e.g. induction hypotheses in proofs), which need to be accounted for. I'm happy to be convinced otherwise. prove that a sorting algorithm is I produced the full verification of Quicksort (probably the first), and I needed to produce a large amount of intermediate specifications for auxiliary lemmas. The full specification was much longer than the algorithm.
Eridrus 9y ago
You have to make sure your spec is right, but you also have to make sure your tests are right, and people are pretty happy with the idea of testing.
- taneq 9y ago
  Yeah, I'm not saying that automated testing (whether through unit tests or through theorem proving) is bad, just that the two approaches seem pretty much equivalent. All these strong claims about "proven correctness" get thrown about but I'm not sure it's very useful when all you're proving is that the computer did what you told it (which you know anyway - the problem is almost invariably that you told it to do the wrong thing.)
  - jroesch 9y ago
    They are fundamentally not equivalent, you can not guarantee that a system respects a safety property with testing. You can prove that certain concrete instances, i.e your test cases inputs are safe, but you don't know where there exists a path in your program where the safety property is violated. This is incredibly important in critical systems because it might not be possible to even detect a safety violation has occurred, for example file system corrupts data, distributed consensus algorithm commits to the wrong value, compiler slightly mis compiles your code. We want to be ensure there exists no path where something "bad" can occur, this is what verification gives us over testing. There is always the fundamental problem of needing to communicate what we want to the computer, but the goal is to do it minimal way, and then ensure the program we write exactly matches the minimal implementation.
dselsam 9y ago
> All you're doing is moving the bugs from the source code to the specification. The value of doing this can vary, but there are some cases in which the gain is immense and indisputable. Suppose you are writing a compiler optimization. Your source code could be arbitrarily complicated, but your specification is simply "an optimized program always behaves the same as the original".
- taneq 9y ago
  Are things like "the output must be equal to the output of this other thing" easily expressed to a prover? If so this seems like it'd be awesome for optimisation as well.
  - dselsam 9y ago
    Yes, this is easy to express in a prover. A naive implementation can always serve as a specification for a sophisticated one.
    - eriknstr 9y ago
      This sounds very interesting indeed. Can this be done with Coq? Do you have any tutorials or such on doing this?
      - wizeman 9y ago
        It can definitely be done with Coq. The typical recommendation is to read through and do the exercises in the freely-available Software Foundations book [1], which will teach you how to do that in Coq. That said, while it was educational and an extremely good introduction to interactive theorem proving, as I went through the book I became increasingly disappointed with how Coq-style proofs were so laborious and difficult to achieve, as often you had to prove even the simplest things step by step. You also had to go through many chapters before you finally arrived at proving correctness of optimization. I later found an alternative which I can't recommend highly enough. If you read through and do the exercises in the also freely-available Concrete Semantics book [2], you will also learn how to do exactly what you want, but you will learn it much sooner and in a much easier way. In the latter book, you will be using the Isabelle/HOL prover instead of the Coq prover, though. The language looks slightly more idiosyncratic (I'm referring to the weird extra quotes - you will know what I mean), but despite that, to me it was worth a hundred times over: Isabelle/HOL has the most amazing proof automation I've seen - it will not only find proofs all by itself quite often, automatically using hundreds of theorems it already knows or that you have already proved before, but sometimes it will even automatically spit out human-readable proofs, which will teach you how the proof can be done (which is useful when you are stumped and had no clue how to move forward). Isabelle/HOL can also be configured to automatically find errors in your specification and in your implementation - it has built-in automatic quickcheck / nitpick functionality, which can often tell you that you're trying to prove something that is not provable even before you attempt to prove it. IMHO, all of these things contribute to a significantly better user experience (as a newbie, at least). If you are interested, give it a try. I highly recommend it! [1] https://softwarefoundations.cis.upenn.edu/current/index.html https://softwarefoundations.cis.upenn.edu/current/index.html [2] http://concrete-semantics.org/ http://concrete-semantics.org/
nickpsecurity 9y ago
You used to have bugs in the ambiguous requirements in English, any formal specs which are precise, and the code. Formal specifications plus verification does indeed mostly move bugs to the formal specs or proofs. That mostly eliminates two classes of bugs. Then, it ensures that your extracted or verified code probably corresponds to your specs. It might even been proven free of (common errors here). With certifying compiler, the ML or C code might also be proven to compile to assembly without errors. Quite a bit of improvement there. Developer is not just moving things on a ledger. That developer is preventing entire classes of problems plus reducing problems in what remains.
emmab 9y ago
> You still have to transfer the same amount of information to the computer. Different target languages to transfer the information to may result in somewhat uncorrelated defects, allowing finding defects through mutual comparison. You can test a generator by writing a recognizer and vice versa. Errors in formal proof of correctness are somewhat uncorrelated with errors made in tests and errors made in implementation. By doing all 3 you can diversify to reduce risk.

gtani 9y ago

This seems to be a newly hot topic, whether to fight adversarial inputs or looking for efficiencies. I bookmarked a few relevant blogs (but really need to read more deeply) http://composition.al/blog/2017/05/31/proving-that-safety-critical-neural-networks-do-what-theyre-supposed-to-where-we-are-where-were-going-part-2-of-2/ http://composition.al/blog/2017/05/31/proving-that-safety-cr... http://www.cleverhans.io/security/privacy/ml/2017/06/14/verification.html http://www.cleverhans.io/security/privacy/ml/2017/06/14/veri... https://blog.foretellix.com/ https://blog.foretellix.com/ and another preprint: https://arxiv.org/abs/1706.10268 https://arxiv.org/abs/1706.10268

pkay 9y ago

> Note: building Certigrad currently takes ~15 minutes and consumes ~7 GB of memory. Why does it take so long and use so much memory?

dselsam 9y ago
Author here. Building Certigrad involves replaying all tactic scripts in the entire project to reconstruct all of the formal proofs, and then checking each of the formal proof objects in Lean's small trusted kernel. Proving (and checking) the main correctness theorem for stochastic backpropagation is very fast. The vast majority of the time and memory is spent verifying that a specific machine learning model (AEVB) satisfies all the preconditions for backprop. This involves proving several technical conditions, e.g. that various large terms are (uniformly) integrable. We have not experimented much with simplification strategies, and there is probably a lot of room for improvement in bringing these numbers down. It would also be good to provide an option to build the system without reconstructing the proofs; checking the proofs is analogous to running the entire test suite, and most users do not do this for every tool they build.
- xgk 9y ago
  Could this problem have been (partly) avoided by going for an LCF-based prover such as HOL or Isabelle/HOL, rather than a system based on the Curry-Howard correspondence?
  - dselsam 9y ago
    I do not even know how I would have built Certigrad in Isabelle/HOL in the first place. In my first attempt to build Certigrad, I used a non-dependent type for Tensors (T : Type), and I accumulated so much technical debt that I eventually gave up and started again with a dependent type for tensors (T : Shape -> Type). This was my only major design error in the project, and development went smoothly once I made this change.
    - xgk 9y ago

misterAxiom 9y ago

> Machine learning systems are also difficult to engineer because it can require substantial expertise in mathematics (e.g. linear algebra, statistics, multivariate analysis, measure theory, differential geometry, topology) to even understand what a machine learning algorithm is supposed to do and why it is thought to do it correctly. It's like Teen Talk Barbie.