Certigrad: bug-free machine learning on stochastic computation graphs • Hacker News Board

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

#51

Post by xgk » Tue, Jul 11, 2017, 8:01 PM UTC

jroesch wrote: post #45

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…

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

   calling context

In compositional verification, you generally want to prove as much as possible about the piece of code at hand -- irrespective of calling context.

   spec very similar to this

Yes, I was using something similar. Note that this is right only in a purely sequential setting ...

   I recently verified a JIT compiler,

That sounds exciting. That must have been a major piece of work. Anything published yet?

With JIT compilers the issue of self-modification becomes pertinent. I know that Magnus Myreen has verified a small JIT compiler a few years back but I don't remember exactly what theorem he proves. IIRC he was using a tailor-made Hoare logic for x86 code that basically moved some of the complexity of the spec into the logic.

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

#52

Post by xgk » Tue, Jul 11, 2017, 8:20 PM UTC

jojo3000 wrote: post #46

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?

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…

One of my PhD students will soon have to learn an interactive prover. I was to recommend Isabelle/HOL because it's got the best automation, but maybe I should consider Lean (and learn it along with him).

I worry slightly about Lean being immature, and lacking a big library eco-system in 2017. OTOH, it's also good to be at the cutting edge.

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

#53

Post by jojo3000 » Wed, Jul 12, 2017, 8:45 AM UTC

xgk wrote: post #43

jojo3000 wrote: post #39

Earlier quoted context omitted.

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), bu…

Sorry, I was unclear. I meant that most LCF style theorem provers only have one theorem datatype to carry proof information.

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

#54

Post by cgmg » Wed, Jul 12, 2017, 9:12 PM UTC

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…

Verification ≠ specification.