It's in Anthropic's best interest to focus the conversation on "distillation". Imo the more interesting thing to focus on is that there are now several more labs with the expertise and capabilities to train trillion…
> The actual opposing argument is that it's impossible to create a billion dollar enterprise without a group effort The other thing that we're often ignoring is that it's impossible to create a billion dollar enterprise…
I agree with most of what the author is saying, but the slogan that "a sufficiently detailed spec is code" can be misunderstood as "a sufficiently detailed spec is a program". The statement is only true if you read…
Apologies if this came across the wrong way. I really do want to know what the novel contributions of the post are, because the author implies that something about what they're doing is solving previously open problems:…
Isn't this an old idea? E.g., here's a textbook on optimization algorithms for matrix manifolds https://press.princeton.edu/absil and here's a library that implements this in python for the Stiefel manifold that's the…
The reason deep learning is alchemy is that none of these deep theories have predictive ability. Essentially all practical models are discovered by trial and error and then "explained" after the fact. In many papers you…
The usual way to check whether a definition is correct is to prove properties about it that you think should hold. TLA+ has good support for this, both with model checking as well as simple proofs.
I'm personally very excited about the progress in interactive theorem proving. Before the current crop of deep learning heuristics there was no generally useful higher-order automated theorem proving system. Automated…
> The idea is, if we don't think of anything more efficient, we'll at least be able to simulate a cat, and then an idiot, and then Einstein, and then something smarter. And since we almost certainly will think of…
> even if this doesn’t lead to AGI, at the very least it’s likely the final “warning shot” we’ll get before it’s suddenly and irreversibly here. I agree that it's good science fiction, but this is still taking it too…
Adding to this, inference is getting cheaper and more efficient all the time. The investment bubble is probably the biggest reason why inference hardware is so expensive at the moment and why startups in this sector are…
Theorem proving can be formulated as a game, see e.g., https://plato.stanford.edu/entries/logic-games/ and interactive theorem provers can verify that a proof is correct (and related sub problems, such as that a lemma…
Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them. By…
You don't get new theorems if you remove assumptions. Rather, you get the ability to add different assumptions. The Banach-Tarski paradox shows that classical set theory makes the wrong assumptions to intrinsically…
This is NYSE specific: https://www.nyse.com/article/parity-priority-explainer
> it doesn't distinguish between "isomorphism" and "canonical isomorphism" You can distinguish these concepts in (higher )category theory, where isomorphisms are morphisms in groupoids and canonical isomorphisms are…
For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in…
Others have already mentioned this, but Alan Kay spent his entire career experimenting with approaches to radically simplify computing. The progress reports from vpri give a good overview of a recent project that has…
I agree completely. I was just speculating on why there is so much discussion about marketing ploys in this comment section.
This particular statement really doesn't seem like a marketing ploy. It is difficult to disagree with the potential political and societal impacts of large language models as outlined here: https://www.safe.ai/ai-risk…
I don't think many people are arguing against having arbitrary byte arrays for storage and using application specific serialization formats. The real problem with file systems, imo, is that they present a leaky…
Open any book on differential geometry and compare the treatment of differentiation with the needlessly index heavy treatment in any undergraduate calculus textbook. The point is that we treat the differential of a real…
Wild speculation, but my guess is that both will continue to be developed. As far as I understand, the MLIR project predates its machine learning application and was originally intended as a new IR for clang. In that…
> Homotopy Type Theory doesn't really contribute much to logic Of all the things in this list, this is the one you think is odd? The idea behind homotopy type theory is a groundbreaking connection between type theory…
C++ has bad error messages because of language design. Contemporary C++ compilers are very good at reporting clear error messages about common mistakes, but template heavy code still yields arcane error messages.…
It's in Anthropic's best interest to focus the conversation on "distillation". Imo the more interesting thing to focus on is that there are now several more labs with the expertise and capabilities to train trillion…
> The actual opposing argument is that it's impossible to create a billion dollar enterprise without a group effort The other thing that we're often ignoring is that it's impossible to create a billion dollar enterprise…
I agree with most of what the author is saying, but the slogan that "a sufficiently detailed spec is code" can be misunderstood as "a sufficiently detailed spec is a program". The statement is only true if you read…
Apologies if this came across the wrong way. I really do want to know what the novel contributions of the post are, because the author implies that something about what they're doing is solving previously open problems:…
Isn't this an old idea? E.g., here's a textbook on optimization algorithms for matrix manifolds https://press.princeton.edu/absil and here's a library that implements this in python for the Stiefel manifold that's the…
The reason deep learning is alchemy is that none of these deep theories have predictive ability. Essentially all practical models are discovered by trial and error and then "explained" after the fact. In many papers you…
The usual way to check whether a definition is correct is to prove properties about it that you think should hold. TLA+ has good support for this, both with model checking as well as simple proofs.
I'm personally very excited about the progress in interactive theorem proving. Before the current crop of deep learning heuristics there was no generally useful higher-order automated theorem proving system. Automated…
> The idea is, if we don't think of anything more efficient, we'll at least be able to simulate a cat, and then an idiot, and then Einstein, and then something smarter. And since we almost certainly will think of…
> even if this doesn’t lead to AGI, at the very least it’s likely the final “warning shot” we’ll get before it’s suddenly and irreversibly here. I agree that it's good science fiction, but this is still taking it too…
Adding to this, inference is getting cheaper and more efficient all the time. The investment bubble is probably the biggest reason why inference hardware is so expensive at the moment and why startups in this sector are…
Theorem proving can be formulated as a game, see e.g., https://plato.stanford.edu/entries/logic-games/ and interactive theorem provers can verify that a proof is correct (and related sub problems, such as that a lemma…
Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them. By…
You don't get new theorems if you remove assumptions. Rather, you get the ability to add different assumptions. The Banach-Tarski paradox shows that classical set theory makes the wrong assumptions to intrinsically…
This is NYSE specific: https://www.nyse.com/article/parity-priority-explainer
> it doesn't distinguish between "isomorphism" and "canonical isomorphism" You can distinguish these concepts in (higher )category theory, where isomorphisms are morphisms in groupoids and canonical isomorphisms are…
For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in…
Others have already mentioned this, but Alan Kay spent his entire career experimenting with approaches to radically simplify computing. The progress reports from vpri give a good overview of a recent project that has…
I agree completely. I was just speculating on why there is so much discussion about marketing ploys in this comment section.
This particular statement really doesn't seem like a marketing ploy. It is difficult to disagree with the potential political and societal impacts of large language models as outlined here: https://www.safe.ai/ai-risk…
I don't think many people are arguing against having arbitrary byte arrays for storage and using application specific serialization formats. The real problem with file systems, imo, is that they present a leaky…
Open any book on differential geometry and compare the treatment of differentiation with the needlessly index heavy treatment in any undergraduate calculus textbook. The point is that we treat the differential of a real…
Wild speculation, but my guess is that both will continue to be developed. As far as I understand, the MLIR project predates its machine learning application and was originally intended as a new IR for clang. In that…
> Homotopy Type Theory doesn't really contribute much to logic Of all the things in this list, this is the one you think is odd? The idea behind homotopy type theory is a groundbreaking connection between type theory…
C++ has bad error messages because of language design. Contemporary C++ compilers are very good at reporting clear error messages about common mistakes, but template heavy code still yields arcane error messages.…