dwohnitmok

44 ms·

91.
by dwohnitmok 10mo ago
This is mildly disingenuous no? I'm not talking about Rob Pike's reaction which as I call out, "makes sense to me." And you are not just talking about legal entities. After all the legal entity here is Sage. You're
92.
by dwohnitmok 10mo ago
You're misreading my comment. I understand Rob Pike's reaction (which is against the general state of affairs, not those three individuals). I explicitly said it makes sense to me. I'm reacting to @crawshaw specifically listi
93.
by dwohnitmok 10mo ago
Okay. So Adam Binksmith, Zak Miller, and Shoshannah Tekofsky sent a thoughtless, form-letter thank you email to Rob Pike. Let's take it even further. They sent thoughtless, form-letter thank you emails to 157 people. That makes me less
94.
by dwohnitmok 10mo ago
> Yet when you compare the same model in 2 different agents you can easily see capability differences. Yes definitely. But this is to be expected. Heck take the same person and put them in two different environments and they'll have
95.
by dwohnitmok 10mo ago
> even the APIs these days are wrapped in layers of tooling and abstracting raw model access more than ever. No, the APIs for these models haven't really changed all that much since 2023. The de facto standard for the field is still
96.
by dwohnitmok 10mo ago
> The improvements to programming (IME) haven’t come from improved models, they’ve come from agents, tooling, and environment integrations. I disagree. This almost entirely model capability increases. I've stated this elsewhere: ht
97.
by dwohnitmok 10mo ago
There's a fair amount of uncertainty on this point. In general it's unclear when/whether things will plateau out (although there are indications again that the trend is accelerating not decelerating). That being said, if by &
98.
by dwohnitmok 10mo ago
It's significantly accelerated to 4 months since the beginning of 2025, which puts 1 week within reach if things stay on trend. But yes 7 months is the more reliable long-term trend.
99.
by dwohnitmok 10mo ago
To be clear this doesn't mean that it takes the AI > 4 hours to do the task. METR is measuring the difficulty of tasks by how long it takes a human to do the same task. This benchmark is saying that Opus 4.5 can now do tasks (relate
100.
by dwohnitmok 10mo ago
No you can also model things that are client-only or server-only using such non-deterministic events. For example you could have the following client-only properties where you can treat "connection established" as an entirely non-
101.
by dwohnitmok 10mo ago
I can imagine a huge number of properties. 1. Eventual consistency: if no new edits are generated, then eventually all connected viewers see the same document. 2. Durability: if the system acknowledges an edit, then that edit is stored perm
102.
by dwohnitmok 10mo ago
This has definitely happened before with e.g. the o1 release. I will sometimes use the Wayback Machine to verify changes that have been made.
103.
Chess LLM Benchmark: Evaluating LLMs' ability to play chess(github.com)
2 points by dwohnitmok 10mo ago|0 comments
104.
by dwohnitmok 11mo ago
> How do AI did it? Using already existing math. If we need new math to prove Collatz, Goldbach or Riemman, LLMs are simply SOL. An unproved theorem now proved is by definition new math. Will LLMs get you to Collatz, Goldbach, or Riemann
105.
by dwohnitmok 11mo ago
> That's why you need to modify the type system, obviously. That is not a problem. What typing judgment rules would you have for RUNTIME? > On the other hand, if you can prove f x = g x for all x, then you should be able to prove
106.
by dwohnitmok 11mo ago
I don't see anywhere in HAKMEM where they advocate for the use of unbounded rational numbers. Do you have any examples of unbounded rational numbers used in a microcontroller program, in a production Forth program, or really in any pro
107.
by dwohnitmok 11mo ago
This approach seems entirely unworkable. You're saying that RUNTIME should be a built-in function, but then all the paragraphs succeeding that demonstrate that RUNTIME cannot be a function. All the typing judgments I can think of that
108.
by dwohnitmok 11mo ago
> What do you mean by "the current implementation"? Isabelle defines mathematical functions, not running code. This is the whole problem! The line gets blurry with `primrec`, `fun`, and `function` and indeed the book is treatin
109.
by dwohnitmok 11mo ago
This is potentially horrendous for performance, and even worse, unpredictably so. Instead of getting the incorrect answer (or NaN) with floating point if you have an unfortunate series of calculations, you get extreme memory blowup, where y
110.
by dwohnitmok 11mo ago
> First, you can see that time_f only gives you upper bounds for the runtime (they say this in the book explicitly, but in a different context), because who is to say that you cannot find even "faster" equations. I don't
111.
by dwohnitmok 11mo ago
Error in `f1_equal_to_f2`. Should be ` f1_equal_to_f2 : forall (x: Float), floatToR(f1(x)) = f2(floatToR(x))` with an implicit proof delivered to `f2` that `forall (x: R), IsFloat(floatToR(x))`. Also there's some subtleties in how to s
112.
by dwohnitmok 11mo ago
> You could do what you want by making that argument explicit formally and machine-checked, but then you have to do a lot more work, by translating all of the components of the informal proof into formal ones. I don't see how you ca
113.
by dwohnitmok 11mo ago
Is everyone just glossing over the first place score of 118/120 on the Putnam?! I mean we'll see how it does on the upcoming 2025 test, but that's insane! We've seen absolutely ridiculous progress in model capability ove
114.
by dwohnitmok 11mo ago
What I mean is that there is no relationship in Isabelle between their cost function and their actual algorithm. The process the book goes through for a function f is the following: 1. Define `f` 2. Create a correctness predicate (call it `
115.
by dwohnitmok 11mo ago
The link was to show Coq's floating point library. > As a concrete example, how would you prove an implementation of a Kalman filter is correct? This would be fun enough to implement if I had more time. But I need to spend time with
116.
by dwohnitmok 11mo ago
> If the abstraction maintains the properties you care about, PROVABLY, there is no problem. This approach doesn't do that. The translation from the actual executing code to the representation used for runtime analysis is done entir
117.
by dwohnitmok 11mo ago
> I'd say GPT-4 in 2023 vs GPT-3 as the last major "wow" release from a purely-model perspective. But they've also gotten a lot faster, which has its own value. And the tooling around them has gotten MASSIVELY better
118.
by dwohnitmok 11mo ago
IIRC this book unfortunately only proves correctness directly and not runtime. Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code. Does a
119.
by dwohnitmok 11mo ago
You use floating point numbers instead of real numbers in your theorems and function definitions. This sounds flippant, but I'm being entirely earnest. It's a significantly larger pain because floating point numbers have some mess
120.
by dwohnitmok 11mo ago
"Agentic" doesn't really mean much and I dislike it. There's no clean line between a "normal" LLM and an "agentic" LLM. Any LLM is perfectly capable of being an agent if you just pipe relevant LLM out

More ›