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

31–40 of 54 posts

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

#31

Post by dselsam »

xgk wrote: post #24
wizeman wrote: post #23

Earlier quoted context omitted.

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

I second this. Isabelle/HOL has much better proof automation than any prover based on Curry/Howard. That's primarily because HOL is a classical logic, while Curry/Howard is constructive (yes, I know we can do classical proofs inside constructive logic, e.g. with proof irrelevance). Almost all automated provers are also classical. Having comparably powerful proof automation to Curry/Howard based systems is an open res…

> Having comparably powerful proof automation to Curry/Howard based systems is an open research problem.

Isabelle/HOL is essentially isomorphic to a subset of Lean when we assume classical axioms, and any automation you can write for Isabelle, you can write for that subset of Lean. It is often easy to generalize automation techniques to support the rest of Lean (i.e. dependent types) as well, but sometimes doing so may introduce extra complexity or preclude the use of an indexing data structure. See https://arxiv.org/abs/1701.04391 for an example of generalizing a procedure (congruence closure) to support dependent types that introduces very little overhead.

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

#32

Post by dselsam »

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?

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.

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

#33

Post by xgk »

dselsam wrote: post #32
xgk wrote: post #21

Earlier quoted context omitted.

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?

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?

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

#34

Post by xgk »

dselsam wrote: post #31
xgk wrote: post #24

Earlier quoted context omitted.

I second this. Isabelle/HOL has much better proof automation than any prover based on Curry/Howard. That's primarily because HOL is a classical logic, while Curry/Howard is constructive (yes, I know we can do classical proofs inside constructive logic, e.g. with proof irrelevance). Almost all automated provers are also classical. Having comparably powerful proof automation to Curry/Howard based systems is an open res…

> Having comparably powerful proof automation to Curry/Howard based systems is an open research problem. Isabelle/HOL is essentially isomorphic to a subset of Lean when we assume classical axioms, and any automation you can write for Isabelle, you can write for that subset of Lean. It is often easy to generalize automation techniques to support the rest of Lean (i.e. dependent types) as well, but sometimes doing so m…

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?

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

#35

Post by misterAxiom »

> 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.

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

#36

Post by wizeman »

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…

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 all incorrect for all you care, but it doesn't matter because the theorem prover will always tell you that your implementation does not implement the specification unless the proof and the intermediate theorems are also correct.

In the sorting example, what matters is that you correctly specify what is a sorted array and that the result of the sort() function should be a sorted array with the same elements as the input. If you decide to prove that your implementation of Quicksort implements that specification, you can use whatever implementation code you want and whatever intermediate lemmas or proofs you want, but again, if you make any mistake in implementing the algorithm or specifying the intermediate lemmas and proofs or even the final proofs, the theorem prover will complain loudly.

If you simply mean that the total size of all the specification, including proofs and intermediate theorems and proofs can be as large or larger than the actual implementation, I agree with you, that can be the case and that is definitely a problem, because that is one of the reasons why most programmers and the industry in general won't find formal verification to be worth it.

That said, SMT solvers (if you are so inclined) and proof automation in general can really help to reduce the size of the complete specification, including intermediate results and proofs (this is the main reason why I prefer Isabelle/HOL to Coq).

(As an aside, I was pretty sure I knew of an example where a real-world system was verified with an SMT solver and where the complete specification and proofs ended up being around 10% of the code size of the implementation, but for the life of me I cannot find that example... perhaps I am misremembering).

If by full verification you mean verifying all the way down to the machine code, I would argue that this kind of verification probably belongs in the compiler (e.g. CompCert or CakeML) rather than being something that the typical programmer should do.

But perhaps, and most likely, I have not understood you completely :)

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

#37

Post by xgk »

wizeman wrote: post #36
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…

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 from scratch of almost all of the proof.

   only have to specify "after 
   running the function sort() 
   on an array,
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.

   all the way down 
   to the machine code
No, that's an orthogonal dimension.

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

#38

Post by jroesch »

Scea91 wrote: post #27
dselsam wrote: post #11

Earlier quoted context omitted.

> 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".

> your specification is simply "an optimized program always behaves the same as the original" I wouldn't say it is simple, since it is undecidable for general programs.

Daniel's point is that the specification itself is simple, he is saying nothing about the complexity of proving that your program matches the specification.

The decidability of the specification isn't important in this context. It is known there is no procedure to build a proof of this specification for any language or optimization, but as humans we can prove that it holds for a specific configuration of compilers, and optimizations, and have done so many times, for example CompCert, Alive, etc.

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

#39

Post by jojo3000 »

xgk wrote: post #34
dselsam wrote: post #31

Earlier quoted context omitted.

> Having comparably powerful proof automation to Curry/Howard based systems is an open research problem. Isabelle/HOL is essentially isomorphic to a subset of Lean when we assume classical axioms, and any automation you can write for Isabelle, you can write for that subset of Lean. It is often easy to generalize automation techniques to support the rest of Lean (i.e. dependent types) as well, but sometimes doing so m…

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 Calculus of Constructions or CIC. Lean's logic essentially consists of Martin-Löf type theory + (noncumulative) universes with Impredicative Prop + inductive type (where nested and mutual induction is compiled down to a simpler forms with only one eliminator) + quotient types + function and Prop extensionality. And optionally choice to gain a classical logic. Most other features, like a Agda like dependent pattern matching, or mutual and nested inductive types are compiled down to more basic features.

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

#40

Post by jroesch »

xgk wrote: post #34
dselsam wrote: post #31

Earlier quoted context omitted.

> Having comparably powerful proof automation to Curry/Howard based systems is an open research problem. Isabelle/HOL is essentially isomorphic to a subset of Lean when we assume classical axioms, and any automation you can write for Isabelle, you can write for that subset of Lean. It is often easy to generalize automation techniques to support the rest of Lean (i.e. dependent types) as well, but sometimes doing so m…

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 level our meta-theory is very similar to Coq's with a few important departures, a big difference the remove of pattern matching and fixpoints from the kernel, we instead have primitive recursors/elminators/recursion principles.

The lead author of Lean (Leo De Moura) has built some of the worlds most advanced automated reasoning tools, and his goal has always to unify type theory and automation. Our goal is to have the benefits of dependent type theory coupled with the high level of automation present in SMT and from tools like Isabelle.

Post reply on HN