Viewing profile — 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.

One of the founders of the IMO Grand Challenge here. FYI I presented the challenge along with a preliminary roadmap at AITP 2020 last week: https://youtu.be/GtAo8wqWHHg . No way to…

That repository has rotted. Preliminary roadmap described in recent invited talk at AITP-2020 http://grid01.ciirc.cvut.cz/~mptp/zoomaitp/aitp_sep_15_1930....

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

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

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

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

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

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

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

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

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

> Doesn't TensorFlow support random variables too? The paper doesn't explain this well, but although you can put random variables in TensorFlow programs, you cannot backpropagate t…

Author here. > Also as scribu states, this doesn't allow you to prove final goals of the system like "classify images with 95% accuracy", nor does it save you from insufficient or …

Author here. > They are wrapping unverified C++ code (Eigen) for the primitive kernels anyway, such as gemm, so AFAIK it could be extended to launch kernels on GPUs without any mod…