fmap

6 ms·

1.
by fmap 2mo ago
Even if the test is run by an independent third party, they can always test open weight models against "finetuning attacks" or similar language which every model will fail for structural reasons. Their financial future is on the l
2.
by fmap 3mo ago
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 para
3.
by fmap 3mo ago
> 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 wi
4.
by fmap 6mo ago
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 &quot
5.
by fmap 1y ago
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: > I figured
6.
by fmap 1y ago
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 t
7.
by fmap 1y ago
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 read a few
8.
by fmap 1y ago
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.
9.
by fmap 1y ago
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 theorem proving c
10.
by fmap 1y ago
> 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 something more
11.
by fmap 1y ago
> 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 seriously. All
12.
by fmap 2y ago
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 only targeting large
13.
by fmap 2y ago
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 l
14.
by fmap 2y ago
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 contrast, this kind of open e
15.
by fmap 2y ago
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 model measure theory
16.
by fmap 2y ago
This is NYSE specific: https://www.nyse.com/article/parity-priority-explainer
17.
by fmap 2y ago
> 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
18.
by fmap 2y ago
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 the first place. The on
19.
by fmap 2y ago
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 since wrapped up, e.g.:
20.
by fmap 3y ago
I agree completely. I was just speculating on why there is so much discussion about marketing ploys in this comment section.
21.
by fmap 3y ago
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
22.
by fmap 3y ago
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 abstraction over somethi
23.
by fmap 4y ago
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 valued function as a
24.
by fmap 7y ago
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 capacity it makes a lot
25.
by fmap 7y ago
> 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 and abstract
26.
by fmap 7y ago
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. Templates are untyped, so t
27.
by fmap 7y ago
Lenses are more than reified record labels though. There is a hierarchy of concepts that can be freely composed based on which features your data structure actually supports. In particular, lenses can be composed with traversals ("lens
28.
by fmap 7y ago
The axiom of choice is part of ZFC. The existence of, e.g., a Mahlo cardinal is not.
29.
by fmap 7y ago
> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. Most mathematicians spend very little time thinking about the foundations of mathematics though, so I'd take that with a grain o
30.
by fmap 8y ago
Derivatives are simple to explain, but not entirely straightforward to implement efficiently. I personally prefer the Glushkov construction. The Glushkov construction (which Hyperscan uses among other things) is a similarly straightforward

More ›