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

11–20 of 54 posts

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

#11

Post by dselsam »

taneq wrote: post #5

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

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

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

#12

Post by taneq »

dselsam wrote: post #11
taneq wrote: post #5

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

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

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.

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

#13

Post by taneq »

Eridrus wrote: post #9
taneq wrote: post #5

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

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 wrong thing.)

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

#14

Post by dselsam »

fchollet wrote: post #7
ogdan wrote: post #6

Earlier quoted context omitted.

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.

> 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/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/certigr...)

Here is the part of the specification that needs to be inspected carefully:

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.

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

#15

Post by dselsam »

taneq wrote: post #12
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".

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.

Yes, this is easy to express in a prover. A naive implementation can always serve as a specification for a sophisticated one.

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

#17

Post by nickpsecurity »

taneq wrote: post #5

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

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.

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

#18

Post by dselsam »

pkay wrote: post #16

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

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.

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

#19

Post by eriknstr »

dselsam wrote: post #15
taneq wrote: post #12

Earlier quoted context omitted.

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.

Yes, this is easy to express in a prover. A naive implementation can always serve as a specification for a sophisticated one.

This sounds very interesting indeed. Can this be done with Coq? Do you have any tutorials or such on doing this?

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

#20

Post by emmab »

taneq wrote: post #5

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

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

Post reply on HN