dwohnitmok

Yeah. I don't think the cited RAND paper really backs up the author's conclusions.

Seeing lines like

> We were not able to determine whether this scenario [engineered pathogens] presents a likely extinction risk for humanity, but we cannot rule out the possibility.

and more generally

> Extinction threats are immensely challenging but cannot be ruled out.

in the RAND report is pretty terrifying!

And the person who is being cited as the expert on viral synthesis who claims to have trained frontier models seems to just be wrong about that? It doesn't seem at all like he's trained anything close to a frontier model unless there's something about his work history that I'm missing.

> You don't have to let the ATP do everything, you can speed it up immensely with well placed assertions where it struggles.

This is basically what you do with Dafny. I'm not very happy with this, not least of which is because it makes for an inferior developer experience in my opinion and because in general you are pretty limited in expressiveness of propositions.

Also it's kind of weird to be fixated on ATPs, as those are more or less a different level of abstraction from the language. You could develop an ATP for Bend.

More generally speaking, the largest, most well-known formal verification projects that verify actual code don't really rely on ATPs. SeL4 relies on explicit proof terms, CompCert relies on explicit proof terms, etc.

This significantly helps compile times, but will still end up with something far slower than Bend. What was I was talking about and presumably what LightMachine is talking about is how Bend is significantly more verbose than Rocq because even if you wrote out everything with terms, Rocq is still substantially slower than Bend, because Rocq relies a lot on implicit machinery (much more significant elaboration, implicit args, etc.) that slow down compilation.

I would encourage you to think more deeply about the assertions you're making here.

I've done a fair amount of work in this space as well, specifically my main toolbox of formal verification tools in the past have been Rocq, Idris, Dafny, and TLA+, and I can say that I've come away with roughly the same set of tradeoffs as what LightMachine describes in his comment.

Current formal verification tools are often very slow precisely because they try to reduce the number of lines of code that are required to write a proof. By making proofs more verbose and more explicit, proofchecking is sped up immensely (my own experiments check out with what LightMachine is saying here; indeed I've seen even greater speedups in the range of 100-1000x).

It makes far more sense to pay a series of one-time costs in LLM tokens that reduces your compilation time from 1 hour to 1 second than to pay the 1 hour compilation cost again and again (these are not exaggerated numbers for larger projects). This is especially true because with modern LLMs, it's usually just fire and forget and let it churn in the background than anything else.

Caching and incremental compilation has a lot of limitations, e.g. for CI. This is the promise that languages like GHC Haskell have promised for a while that always gets blown away by the other side like OCaml where global compilation is just so fast that you don't have to deal with those limitations.

Interesting. This was one of the two areas the AI as Normal Technology folks specifically called out as a bet that AI will not outperform humans at.

> Concretely, we propose two such areas: forecasting and persuasion. We predict that AI will not be able to meaningfully outperform trained humans (particularly teams of humans and especially if augmented with simple automated tools) at forecasting geopolitical events (say elections). We make the same prediction for the task of persuading people to act against their own self-interest.

Curious to hear what their take is now.

https://www.normaltech.ai/p/ai-as-normal-technology

Well it's because the article is AI-generated. Same with the Sacks tweet that was on the front page yesterday.

There's a deep irony that all of these "anti-doom" pieces are entirely AI generated.

What quote from 2024 are you thinking of here?

> The insiders that said every tech workers would be unemployed in 6 months and every white colar would be unemployed in 12 months like 2 years ago?

Eh. This entire tweet smacks of being AI generated. It has a huge amount of LLM-isms.

I wouldn't be surprised if Sacks just prompted an LLM to just come up with whatever rebuttal to whatever the regulation side comes up (given the big set of regulation tweets) with sounds most convincing, given his usual anti-regulation stance.

Anyone with a Pangram account who can check?

> Everyone should slow down AI development except for me

Who's said this? And then more broadly I guess who's implied this? Very curious if there are specific articles/posts prompting this.

The structure of Lean does impose that. The code isn't being run, it's being type checked. And that's it. The overwhelming majority of Lean code is never run. It exists only to be type checked (because type checking is equivalent to verifying the proof).

You could imagine the typechecker has bugs (and indeed another comment mentions examples of bugs!). Crucially though anytime the typechecker has a bug fixed you could rerun the typechecker on the code to see if it still type checks.

This is the whole promise of formal verification. It reduces the problem of verification purely to the typechecker. If the typechecker is correct, then the proof is verified, no matter how many lines of code the proof is. As a sibling comment puts it, the chance of bugs mainly scales with the number of lines of code in the typechecker, not in the amount of lines of Lean code.

Your question is akin to asking, "yes this spellchecker ran fine on your essay, but are you sure it runs fine on War and Peace? That's 1000x more words!" To which the answer is the number of words doesn't matter if the spell checker is correct (which it might not be! And longer passages might reveal more bugs! But you can always rerun it). The main source of bugs is more lines of code in the spell checker, not in number of words in the text.

Yes but that report wasn't written by OpenAI. It was written by three independent researchers. OpenAI seems to have tried to hide it.

Reuters reports that OpenAI tried to keep this one under wraps: https://www.reuters.com/world/europe/openai-agents-hijacked-...

> Astra’s progress helps clarify which AI capabilities are out of reach and which questions remain open.

Okay. But I don't think this entire article at all explained which AI capabilities remain out of reach. Did I miss something? Other than "oh I guess it could still get even more superhuman on ARC-AGI-3 than it is?"

> It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.

Generally you only need to look at 10-100 lines (unless you have a highly novel theorem that essentially invents a new field of math or builds on a field that has never been worked on in Lean before) of the 250k to verify what it claims. This is why there is excitement around formal verification. The rest of it is perhaps useful to read to figure out why the proof works, but is not necessary for checking.

That paper has had a pretty turbulent reception and looks pretty conclusively wrong at this point.

It used an incorrect theoretical framing that assumed that data was being replaced rather than accumulated as a result of more training (see https://arxiv.org/abs/2404.01413 which explores this). This is incorrect because this simply isn't how real-world datasets are created via synthetic data generation (which generally accumulate more data over time rather than replace their data). As a result most of the theoretical results were invalid.

Empirical evidence has also cast a considerable amount of doubt on the paper. For example, Microsoft Phi-4 was an empirical test in specifically what happens if the majority of your training data is synthetic rather than human and it turns out that Phi-4 did significantly better than previous models which relied primarily on human data.

There's some nuance to all of this in how exactly you do this, but the original claims of the paper are looking really shaky at this point.

Yes. Presumably you're referring to my use of the word "level". I mean here basically every "level" as denoted by the order of locations and places on the town map that you get (which is usually +- some other locations how game runners refer to different sections of the game).

> GPT-4(?) was capable of beating Pokemon 18 months ago but models only became capable of beating it without a harness in the last six months...?

GPT-4 was decidedly not capable of beating Pokemon 18 months ago. I doubt it would be able to complete a single level. I don't think people realize how large the advances in model capabilities have been. GPT-4 in a modern harness is absolutely horrendous compared to modern models.

> The responses to the pricing aspect of this announcement around the web disagree.

Which responses are you thinking of?

That's not the norm that's being broken here. Most DB technologies provide a "pay for updates, if you stop paying you keep the last version you paid for" model. This is how Oracle prices its DB tech, this is how jOOQ is priced (which is probably the closest thing to Acadia), this is how MS prices its DB tech etc.

No, not at least for Photoshop. If you have the subscription version and fail to pay it downgrades you to the free version which has more limited editing capacity but still has read capacities.

More broadly I think the only subscription products most software developers are used to where access to data is revoked is cloud infra. Most software stuff follows models like Jetbrains (where e.g. you pay for updates but keep the oldest version). E.g. this is how things like SQL Server or other paid DB technologies work, where you effectively are subscribing to yearly updates, but get to keep the current version if you stop paying the subscription fee.

Oh man. If this lobste.rs comment is correct about the subscription terms then this feels like a really hard pill to swallow: https://lobste.rs/s/ykq7ym/rethinking_database_programming#c...

Still might be viable, but would be tricky to sell.

> SUBSCRIPTION TERMS

> This license is subscription-based and will remain valid only for the duration of your active subscription. Upon expiration or termination of your subscription:

> a) Your rights to use the Software will cease; b) You must uninstall and stop using the Software; and c) You may lose access to any data or content created with or stored in the Software.

I'm wary of languages that seek to own the database. In particular, the claim "Coexist with SQL" seems a bit suspect given that e.g. sum types have a custom binary encoding, which likely makes them difficult to interop with from other languages. This makes the claimed interop with other languages really more of a temporary stopping point towards full Acadia adoption rather than a viable long-term equilibrium, unless you e.g. eschew using sum types. (I also suspect that trying to natively support sum types can lead to a kind of FP-equivalent of ORMs' impedance mismatch. The ways I model data with relational logic can be pretty different than the ways I model data with algebraic datatypes and I wonder if trying to force fit the latter into the former doesn't lead to the same problems as force fitting objects into relational logic).

This makes the database closer to something that Acadia compiles to, rather than something Acadia sits on top of. From my own developer experience this feels off, because I generally expect the data layer to be king and application code to revolve around that, rather than having data representation created in code and the database created off that (this is why I also dislike things like ORMs).

In general I view databases as usually having more longevity than application code, especially as you accumulate more data over time. For serious production applications, the database often outlives multiple rewrites of the production application.

I suspect though my concerns are overall rather minor. The ergonomics of the language itself seem enjoyable. Acadia seems like it would be great as an embedded DSL. It's a bit unfortunate that it currently seems coupled to creating an HTTP server. I think that Acadia has greater ambitions beyond just the database, as evidenced by creating a binary web connection with frontend Elm code to presumably obviate the need for encode-decode layers. It seems like Acadia is meant to be a stepping stone towards a closer frontend-backend fusion. But I agree with mjaniczek that something like Lamdera seems a better fit for that.

But given how early Acadia is, I'm still very excited for where it goes. What I've listed is surmountable and I also feel that often a closer frontend-backend fusion might be worthwhile.

To be clear the happy path for taxis for me was fine. When things worked things were quite smooth. But this thread is primarily about when things went off the happy path. If a taxi didn't show up, I'd usually have a disinterested dispatcher to talk with who might be able to send another in a half hour. If a taxi intentionally went the long way around to charge more, I'd have to have an argument with the cabbie about this and maybe things would go well maybe they wouldn't. While I didn't personally experience harassment from cabbies I definitely know people who have. So on and so forth. In all of these cases off the happy path the usual recourse back then was worse than the recourse today with e.g. Uber.

Again the overwhelming majority of my taxi rides were fine. The overwhelming majority of my Uber rides are also fine. But when things go wrong they definitely went wrong worse with taxis than Uber rides for me.

Infuriating as it is, this is still better than with the bad old days of taxis, which usually had even worse resolution and accountability. It sounds like people don't quite grasp just how bad the taxi experience was.

> For some programs, the shortest descriptions of what they do are the programs themselves.

There is almost no real-world program for which this is true. One corollary of this would be that it is impossible to refactor the program to be any cleaner, which is not true for basically any large real-world program.

Another corollary of this is that no observable aspect of a program could be changed without breaking user expectations, but this too is almost always wrong (e.g. almost always, but not 100% via e.g. the famous xkcd comic about spacebar heating, a global performance optimization would be viewed as good).

> I don't think I understand why they aren't leveraging the increased speed to do batching to serve more customers at a "normal" tok/s.

There's some technical hypotheses about it that other people are offering.

But also from a business perspective, it totally makes sense not to go any sort of batching play. It's really valuable and very clear to consumers to make your pitch entirely about lower latency rather than higher bandwidth.

There are so many scenarios that are latency-constrained that will be difficult or even impossible for someone even with fleets of high-bandwidth compute to compete with you on.

Very easy pitch to sell a customer who asks what differentiates you from other companies: you pay us a premium for lower latency than anyone else.

Sure. I'm mainly curious who beepbooptheory is thinking of.

> Everyday we see articles exactly like his by different people (or at least I do), but none attract the same kind of distinct attention.

Who else does a detailed financial breakdown like Zitron and thinks things are as corrupt/fishy as him (in particular make specific claims about certain unexplained sums of money)? All the articles I see ultimately just trace back to Zitron. Curious who else you've found.

> Nonsense. The "weights" in "models" refer to probabilities.

No they don't. They refer to the weights used for weighted sums. The weights don't have to even between 0 and 1.

> political commentary from someone

No it depends on what they choose to answer. canyon289's account self-describes as Bayesian, a hallmark of rationalists, one of whose taglines is "politics is the mind-killer". Nonetheless https://www.lesswrong.com/posts/iKm2FhpWkuuBojm82/why-i-left... is one of the most upvoted posts on LessWrong (the big rationalist site) of all time. Most of the comments don't touch on the politics of the situation at all.

> someone just going about their job

They're doing a little bit more than that by actively recruiting (even more so than the usual "if this interests you we're hiring" bit at the end of a post). So I'm doing a little bit more by asking them about a recent high profile departure. It's a little bit different from the usual way employees chime in on threads.