dselsam

“Here is a Homer poem about the Singularity:”

It is not possible to say

Whether the gods set the Singularity

Upon us, or the Singularity

Caused the gods to be.

> Its always funny to realize how "easy" beating human-intelligence is (Chess AI, Go AI, even Mathematical Proofs), but how hard beating human-simple behaviors are.

This is the baseless myth that won't die. We are nowhere near rivaling humans in mathematical proving. Even after a human has proved a theorem, it can be an astronomic amount of work to even explain the proof to a machine after the fact (i.e. to construct a machine-checkable version of the proof), even when using suites of sophisticated software tools developed solely to facilitate this process. Progress has been glacially slow since the field began in the 1950s. Deep learning has had zero impact.

We will have robots that can grasp competently way before we have machines that can rival humans in mathematical proving.

Author here. We weren't shooting for low-hanging fruit, and we realize that we are still very far from contributing to the state-of-the-art. We tried to approach this project as scientists instead of as engineers. I personally found NeuroSAT's success to be extremely surprising, and I think it underscores how little we understand about the capabilities and limitations of neural networks. Our approach might prove to be a dead-end but I think there is some chance we have stumbled on something powerful.

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.

The specification is simple in the sense that it is easy to understand what it states and to confirm that it has the intended meaning. This does not mean that all proofs of the specification will be simple, but once you do construct a machine-checkable proof of the specification, your level of confidence that the system is correct will be extremely high (commensurate to the simplicity of the specification) and will not depend on the complexity of the proof.

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.

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

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