Certigrad: bug-free machine learning on stochastic computation graphs

by kg9000 • 9 years ago

99 52 9 years ago

binarymax• 9 years 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...

taneq4• 9 years ago

PDF warning for those of us on mobile.

alimw• 9 years ago

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

taneq4• 9 years 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• 9 years 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• 9 years ago

How is that the case in this specific example? It looks a lot harder to check for correctness.

xgk14• 9 years 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).

Eridrus• 9 years 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.

taneq4• 9 years 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.)

dselsam7• 9 years 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".

taneq4• 9 years 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.

Scea91• 9 years ago

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.

nickpsecurity• 9 years 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• 9 years 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• 9 years 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-cr...

http://www.cleverhans.io/security/privacy/ml/2017/06/14/veri...

https://blog.foretellix.com/

and another preprint: https://arxiv.org/abs/1706.10268

pkay• 9 years 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?

dselsam7• 9 years 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.

xgk14• 9 years 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?

misterAxiom• 9 years 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.

Certigrad: bug-free machine learning on stochastic computation graphs

Related Stories