dselsam

5 ms·

1.
Terence Tao on O1(mathstodon.xyz)
664 points by dselsam 2y ago|482 comments
2.
by dselsam 4y ago
“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.
3.
by dselsam 6y ago
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 know if gold is five years out or five hund
4.
by dselsam 6y ago
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....
5.
NeuroCore: Guiding CDCL with Unsat-Core Predictions(arxiv.org)
5 points by dselsam 8y ago|0 comments
6.
by dselsam 8y ago
> 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
7.
Vaporithms(stanford.edu)
1 points by dselsam 8y ago|0 comments
8.
by dselsam 9y ago
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 Ne
9.
by dselsam 9y ago
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 eventua
10.
by dselsam 9y ago
> 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 classical axioms, and any automation you can wri
11.
by dselsam 9y ago
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 machi
12.
by dselsam 9y 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 checki
13.
by dselsam 9y ago
Yes, this is easy to express in a prover. A naive implementation can always serve as a specification for a sophisticated one.
14.
by dselsam 9y ago
> 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. Autho
15.
by dselsam 9y 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 optimizat
16.
by dselsam 9y ago
> 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 through them. With stochastic computation graph
17.
by dselsam 9y ago
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 inaccurate data. We focused on implementat
18.
by dselsam 9y ago
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 modification to the part in Lean that they proved correct. T