Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Certigrad: bug-free machine learning on stochastic computation graphs

github.com

Post reply on HN
Print view View original

41–50 of 54 posts

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#41

Post by jojo3000 »

xgk wrote: post #28
wizeman wrote: post #26

Earlier quoted context omitted.

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 specif…

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 ne…

But your "intermediate specifications" are not part of your specification! The specification says that the result is a sorted version of the input. It does not care about the induction hypothesis in your program. It might be technically necessary depending on the verification condition generator you are using. When you verify a functional program using Isabelle, Lean, or Coq your statement is that the output is a sorted version of the input.

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#42

Post by wizeman »

xgk wrote: post #37
wizeman wrote: post #36

Earlier quoted context omitted.

You sound like you have more experience in this area than I do, so please correct me if I'm wrong. In the context of the original poster, the size of the specification that matters with respect to being a potential source of errors is the specification of the final (initial?) theorems that you want to prove, not the actual proof, nor the intermediate lemmas/theorems, induction hypothesis, etc. The latter ones can be…

The latter ones can be all incorrect for all you care Good point. Maybe we can call this the TSP (trusted specification base)? In my experience the TSP is subtle and contains most of the intermediate definitions too. A few years back I had a very large Isabelle/HOL proof invalidated because of some small mistake in an obscure part of the specification that I never though could be important. It required a redesign fro…

  I'm afraid that's not enough in practise: you will also have to specify (and verify) things like: the implementation does not touch memory except the array to be sorted (and some auxiliary variables). If you don't, it will typically be difficult to use the proof of the sorting function in the context of the verification of a larger program.
Depending on the programming language being proved, you don't need to specify that the algorithm doesn't touch other memory, nor which variables it uses as temporary variables, because it's implicit in the definition of the language or the types themselves (or the fact that you are not referencing global variables).

See [1] for an example of a formally proved implementation of an array search algorithm (implemented in the Dafny language, in this case. You can press the play button to see if the theorem prover approves of this implementation).

As you can see, in Dafny there's no need to prove that no other memory is touched, as it's implicit in the type of the method. However, even this example is not as good as it could be because:

- Ideally, you wouldn't need to specify that function arguments aren't null. This would have been implicit had the implementation language (Dafny) not had the concept of null (like Rust doesn't, for instance).

- Also ideally, you would refactor the pre- and post-conditions into a separate predicate, like it was done for sorted(), so that you could prove any array search function to be correct using the same short specification (and if a bug is found in the specification, the fix would be applied to all implementations of array search functions automatically).

Regarding having a large Isabelle/HOL proof invalidated, that sounds very interesting and would love to read more about it! I can definitely admit I have never done any large proofs yet, so I am interested in hearing about your experience.

Ideally there should be some way of isolating parts of a large specification such that a bug in one part could not affect the other parts (similar to how functional languages guarantee that a function can never read anything but its input, and can never write to anything but its output), but I have absolutely no idea if this is even logically possible, as I am still just a beginner in this area.

Thanks for the interesting discussion!

[1] http://rise4fun.com/Dafny/loJb

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#43

Post by xgk »

jojo3000 wrote: post #39
xgk wrote: post #34

Earlier quoted context omitted.

This is interesting. It will take me some time to digest this paper. As an aside: is there a terse description of Lean's type-theory? Also: Lean is Curry/Howard based, it's not an LCF-style architecture?

Lean is LCF style in the sense that there is a small kernel, and all proofs written by the user and generated by the automation are checked by this kernel. This kernel (i.e. type checker) is much smaller than that of Coq or Agda. It is _not_ LCF style in the sense that there is only a "theorem" datatype with proof operations. Lean proofs are type-checked expressions. It is hard to find a terse description of the Calc…

    there is only a "theorem" datatype
You mean that there is NOT only a "theorem" datatype? In contrast to Curry/Howard provers, the LCF approach forgets proofs, it guarantees soundness by giving you access to proof rules only through the "theorem" datatype (which is the key trusted computing base). To be sure the "theorem" datatype may internally maintain a proof object (e.g. for the purposes of program extraction), but that's not necessary.

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#44

Post by xgk »

jojo3000 wrote: post #41
xgk wrote: post #28

Earlier quoted context omitted.

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 ne…

But your "intermediate specifications" are not part of your specification! The specification says that the result is a sorted version of the input. It does not care about the induction hypothesis in your program. It might be technically necessary depending on the verification condition generator you are using. When you verify a functional program using Isabelle, Lean, or Coq your statement is that the output is a sor…

Yes. Mostly.

But in practise, you need to specify what sortedness means, and in a generic sorting algorithm that means axiomatising the comparison predicate, including its side-effects. Note for example the C standard library implementation of Quicksort does take an arbitrary predicate, which may not be transitive, may have arbitrary side effects etc. The behaviour of sorting becomes pretty complicated in this scenario.

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#45

Post by jroesch »

xgk wrote: post #37
wizeman wrote: post #36

Earlier quoted context omitted.

You sound like you have more experience in this area than I do, so please correct me if I'm wrong. In the context of the original poster, the size of the specification that matters with respect to being a potential source of errors is the specification of the final (initial?) theorems that you want to prove, not the actual proof, nor the intermediate lemmas/theorems, induction hypothesis, etc. The latter ones can be…

The latter ones can be all incorrect for all you care Good point. Maybe we can call this the TSP (trusted specification base)? In my experience the TSP is subtle and contains most of the intermediate definitions too. A few years back I had a very large Isabelle/HOL proof invalidated because of some small mistake in an obscure part of the specification that I never though could be important. It required a redesign fro…

In your second point you are referring to fact that is needed in a calling context when proving a large spec, that means it is a top level specification, and therefor trusted. You don't need to prove an implementation only touches the allocated array to verify it as a sorting algorithm, its because there is some other part of the top level specification that requires that.

For example I recently verified a JIT compiler, and the compiler spec was functional correctness but we really wanted to ensure it was correct AND only used the memory we allocated for it. In this case we had to grow the specification to be larger, its not longer just being correct, but isolated in some way. This of course has a trickle effect where we need intermediate facts, and proofs in order to be able to prove the top level theorem.

As some posters remarked above you should still be able to give a concise top level specification that is much smaller then the implementation. You really just want to say (where m is pre-sort, and m' is post-sort):

    (forall addr m m',
      addr  read addr m = read addr m')
We have a spec very similar to this in said JIT compiler, where we prove it doesn't write outside its input and output buffers. The top level spec is no more then a few definitions and a few lines of spec, compared to the JIT compiler which is 10,000s of lines of proof & implementation it is tiny and very easy to audit.

You can also make proofs obligations like this easier by using regions, a framing rule, or some programming model that gives some amount of memory isolation.

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#46

Post by jojo3000 »

xgk wrote: post #21
dselsam wrote: post #18

Earlier quoted context omitted.

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) s…

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?

The memory consumption will surely be better, as HOL or Isabelle will only store the fact that a theorem was proven, but not how. But then Lean can store the proofs and has two independent external type checkers. Isabelle has the infrastructure to do this, but it can not cope with it after a certain size (Isabelle's HOL-Proof does not even contain all of HOL/Complex_Main). In my experience Lean feels much faster than Isabelle, so I would guess the proof will take much longer than in Lean. But I don't have any concrete measures.

In Isabelle one might want to trust the code generator to evaluate certain computations in ML.

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#47

Post by xgk »

wizeman wrote: post #42
xgk wrote: post #37

Earlier quoted context omitted.

The latter ones can be all incorrect for all you care Good point. Maybe we can call this the TSP (trusted specification base)? In my experience the TSP is subtle and contains most of the intermediate definitions too. A few years back I had a very large Isabelle/HOL proof invalidated because of some small mistake in an obscure part of the specification that I never though could be important. It required a redesign fro…

I'm afraid that's not enough in practise: you will also have to specify (and verify) things like: the implementation does not touch memory except the array to be sorted (and some auxiliary variables). If you don't, it will typically be difficult to use the proof of the sorting function in the context of the verification of a larger program. Depending on the programming language being proved, you don't need to specify…

   Depending on the programming 
   language being proved
That's true, GCed languages are simpler in this regard. But for low-level languages you have to do this 'by hand', and it can be complicated.

   not had the concept of null
That doesn't make the problem go away, you just have another case in the destructors (e.g. pattern matching) that you need to account for logically. Just kicking the can down the road.

   would love to read more 
   about it
Nothing published. Long story. I'll tell you in person, should we meet some day.

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#48

Post by xgk »

jroesch wrote: post #40
xgk wrote: post #34

Earlier quoted context omitted.

This is interesting. It will take me some time to digest this paper. As an aside: is there a terse description of Lean's type-theory? Also: Lean is Curry/Howard based, it's not an LCF-style architecture?

There are older papers that describes Lean's meta theory, https://leanprover.github.io/publications/ , the first paper, and the one on elaboration. Unfortunately they both describe the version present in Lean 2, which still had the HoTT support we removed in Lean 3. The new tactic paper, set to appear at ICFP '17, also briefly describes Lean's meta-theory. https://leanprover.github.io/papers/tactic.pdf At a high leve…

Thanks for the link to the paper.

De Moura is giving a talk tomorrow in Cambridge at the workshop in computer aided proofs called "Metaprogramming with Dependent Type Theory". I wanted to go, but won't be able to attend. I guess that talk will mostly be about the content of the paper. Now I don't feel so bad for being unable to attend.

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#49

Post by jroesch »

taneq wrote: post #13
Eridrus wrote: post #9

Earlier quoted context omitted.

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.

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 w…

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.

Re: Certigrad: bug-free machine learning on stochastic computation graphs

#50

Post by jojo3000 »

xgk wrote: post #33
dselsam wrote: post #32

Earlier quoted context omitted.

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 c…

ITTs like Lean are more expressive as logics than HOL, but I doubt that Certigrad needs even a fraction of HOL's power. So anything you need that you express as types in Lean you should be able to express as theorem in HOL. Presumably that is inconvenient (= technical debt), but why?

Tensors are a good example: In a proof you might want to do induction over the dimensions of a tensor. This means your type of tensors needs to contain all tensors of all dimensions. But working on the type of all tensors is not so nice anymore: a lot of algebraic properties do not hold, they only hold for tensors of a specific dimension. An example is the Tensor library in the Deep_Learning AFP entry.

Now in Isabelle most strutures are encoded as type class, but when your type is not anymore in the type class suddenly you need to proof a lot of theorems yourself, and the automation does not work as nice as with type classes. Generally, in HOL provers you want at least that your type at least has nice algebraic properties on the entire type. If this is not the case proofs get much more convoluted. Isabelle's simplifier supports this case using conditional rewrite rules, but it still does not work as nice as using type inference to handle this cases.

In dependent type theorem provers it isn't a problem to proof everything on tensors with a fixed dimension. When a proof requires to do induction on the dimension itself these kind of shape can always constructed in the proof itsefl.

Post reply on HN