dwohnitmok

> I don't think OpenAI ever actually disclosed what they were doing when the hijiacking happened.

They did as part of their big October dump. There was also of plenty third-party evidence (you could see prompt leakage in a lot of the hacks).

Many of these did not have an exploit prompt at all.

> I want people to stop pretending they are surprised when the computer does exactly what it's instructed to do.

This is very wrong though. We now have many examples of cases where the computer very much does not do what it is instructed.

OpenAI's hack of DseWiki is an example where the instruction given to the AI agents was to collate data to generate economic reports and it hacked into DseWiki as part of that. It was not given instructions to do any sort of cybersecurity stuff.

The hospital bed stat research project was a similar thing, where OAI's AI agent found the hospital bed statistics through a simple web search and then hacked into the website anyways to download even more data.

More prosaically, models make up reasons for doing crazy things all the time!

Models may or may not be "malicious" (if that's even coherent), but at this point we have lots of evidence they definitely go off the rails in systematic, sustained ways that cause real world disruption that are not at all what they were instructed to do.

Yes but that is significantly less surface area (indeed asymptotically less in the general case if you believe P != NP).

As I mention elsewhere (https://bugs.php.net/bug.php?id=78876) I'm very confused. Looking at the PHP bug tracker the specific bugs were fixed. So my best guess is that the LLM was able to find alternative variants that still worked? But then the report makes less sense.

I'm very confused about what's going on. In fact as far as I can tell those specific bugs were fixed.

https://bugs.php.net/bug.php?id=78876 marks the OOM bug as closed and fixed in 2020.

It seems the AI exploration was able to find variants of those bugs that were not fixed rather than exactly those bugs themselves?

> since Google showed you don't need to retrain an autoregressive model to rework it for diffusion inference

IIRC you do need to retrain the model, just closer to the level of finetuning rather than e.g. pretraining from scratch. Which also means that the model will perform differently with a different capability profile.

> Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?

Absolutely none of them. I have some experience formalizing math by hand in the pre-LLM era. I never started with making the formal proof. It is way too difficult. I don't think I've ever heard of any mathematician starting with a formal proof vs writing a natural language proof. Starting with a formal proof vs a natural language proof is putting the cart before the horse.

Without a natural language proof, or at least an idea of how to write the natural language proof, it is very difficult to write a formal proof. It's flying blind. I can blindly apply tactics, but without some larger plan to guide my formal proof, it's near impossible to make progress on all but the most trivial proofs. I don't think it has ever happened that a major proof was formalized before its natural language proof was written.

I don't think people appreciate just how labor-intensive it previously was to write a formal proof. It takes easily 10-1000x as much time for a human to write a formal proof vs a natural language proof. Even just formalizing a single undergraduate math textbook for certain subjects by hand was considered a multi-year project for a professional mathematician to undertake.

Formalizing a new paper, even if it was building on previously already formalized theorems, could be months of work just by itself, even with the natural language proof in hand.

It is no surprise that OpenAI releases natural language proofs before they release formal proofs. Presumably the same difficulty difference applies to LLMs as well.

> accept two trivial extensions to the standard that are widely used and don’t affect the resulting data in any way

That's always how it starts. If they're truly trivial the reasoning also cuts the other way. Remove them upstream.

I pretty strongly disagree. The body of the text was what I expected based off the title.

> Theorems by definition must be formalizable. A theorem is not simply a true proposition, it's a provable proposition and a proof is necessarily a formal/syntactic property of a proposition.

Yes that's fair. To be accurate the formal definition of a theorem entails that provability. I was being too loose in essentially using "theorem" to refer to any proposition.

This is irrelevant. The theorems Avigard, Buzzard, et al. are talking about all have natural language proofs already that in theory should be formalizable.

They are not claiming all possible theorems are formalizable. They are claiming to try to formalize all already proven theorems in the mathematics canon.

To the extent the theorems in question are impossible to formalize this means the original proof must be in error.

There's maybe an even simpler way of illustrating this.

Fermat's Last Theorem is very easy to state. There are no positive integers a, b, and c such that a^n + b^n = c^n. This likewise easy to write in Lean. The statement of the theorem is exactly one line of code.

    theorem fermat_last_theorem (n : ℕ) (n_ge_3 : 3 ≤ n) (a b c : ℕ) (a_is_positive : 0 < a) (b_is_positive : 0 < b) (c_is_positive : 0 < c) : a ^ n + b ^ n ≠ c ^ n

Kevin Buzzard's team of human mathematicians attempted to prove this in Lean. They got to about 60000 lines of Lean code and were not anywhere close to finishing the job.

Anthropic came around with a Claude model that proved it in 13 million lines of code. (Buzzard's team might have ultimately used within the same order of magnitude if they finished. It's very unclear. They were at minimum years away.)

Whether 60000 or 13 million, only one line of code was necessary to manually verify whether they had successfully proved Fermat's Last Theorem, just the statement of `fermat_last_theorem`. None of the rest of the code built up the theory at all.

Indeed if those lines of code built up the theory, that would suggest that the statement of Fermat's Last Theorem is incomprehensible, if professional mathematicians cannot define Fermat's Last Theorem in even 60000 lines of code! But that's pretty absurd. You can explain the statement of Fermat's Last Theorem, completely rigorously, to a middle schooler.

> First, one question arises: what are the 12 million lines doing if they're not needed? Secondly, don't those 12 million lines build up the theory that is eventually proved? Mistakes could be there that makes the outer statement seem like something it isn't, could there not be?

This seems to reflect an incorrect understanding of formal mathematics.

Formal mathematics can be thought of as a game with rules where a statement to be proved is some game end state. If you play 12 million valid moves and arrive at the desired end state then you have proved that the statement is valid. If your logical system is sound (e.g. first order logic), then you have proved your statement is true.

The entire point of the formalization of logic and mathematics through the 19th and 20th centuries was to unlock this capability. Such that, if you only care about whether your statement is true or not and not why it's true, the intermediate steps are entirely unnecessary.

To answer each of your questions:

> First, one question arises: what are the 12 million lines doing if they're not needed?

They are the intermediate computations necessary to show that the final statement is valid. This is much like intermediate arithmetic operations in a large complicated arithmetic expression. As long as you believe that the computer can calculate each individual arithmetic expression correctly, you don't need to manually review the billions of intermediate calculations that result in the final number.

> Secondly, don't those 12 million lines build up the theory that is eventually proved?

No. Not in the way you're thinking of. It seems you are using "theory" to mean the concepts necessary to express the statement itself. This is a very different set of lines than the proof itself (and generally much much more compact). Very difficult to prove statements can be stated in very simple language. Often the theory is <0.01% of the total lines of code.

> Mistakes could be there that makes the outer statement seem like something it isn't, could there not be?

No. Only the language used in the final statement can cause this issue, i.e. the theory. The intermediate 12 million lines cannot affect this, assuming your computer can carry out arithmetic correctly.

Another way of thinking about it is that the big breakthrough of 19th and 20th century mathematical logic is to conclusively show that formal mathematics is fundamentally just a set of arithmetic operations.

Hence in a very real sense, proving a mathematical statement is exactly identical to finding x in an arithmetic expression f with some constant k such that f(x) = k, where k is determined by the statement you wish to prove (not the 12 million lines).

Showing that x causes f(x) to equal k is exactly equivalent to proving the mathematical statement associated with k.

The 12 million lines are an alternative notation, no different in spirit to decimal notation or binary notation, of writing down x. It is some gigantic natural number.

You must understand k. If you use the wrong k, then you have proved another statement than what you intended. This is usually about a dozen lines of code.

You must be confident in the correctness of f. This corresponds to the believing that your type checker (since Lean uses dependent typing as its method of proof checking) has no fundamental soundness bugs. This can be controversial and indeed Lean's type checker has had soundness bugs in the past! But crucially f does not depend on k or x. Every time you fix a bug in f you can rerun it for any k or x you care about.

But you don't have to actually read all the digits of x, in whatever notation you care about. You can copy paste it in from some gigantic file handed to you by a stranger. As long as f(x) = k, you know that you have proved the mathematical statement associated with k.

Overall, this is roughly like asking why you trust a computer to solve a long division problem that has 12 million intermediate steps if you don't actually read all 12 million intermediate steps yourself. Well I trust the computer to do one step of division correctly and to be able to repeat that faithfully 12 million times. Hence I trust the computer can solve a long division problem involving millions of digits, even if I don't actually look at all 12 million intermediate computations myself.

> and that training data will not be a "new thing", because AI can't invent new things. Just recycling of what it already "knows".

Regardless of the truth of the underlying assertion, this is about as textbook an example of circular logic as it gets. (at least combined with the implicit beginning assertion that "AI can't invent new things.")

>"I didn't introduce the vulnerability, he did! Look I can even prove it with my signed commit!"

I misspoke. It's worse. "I didn't introduce the vulnerability, he did! Look I can even prove it with his signed commit!"

> The signing process doesn't recursively traverse the bytes of the commit to pull them into GPG, like you would expect.

No I wouldn't expect this. If by recursive you mean traversing the entirety of git history, that would be prohibitively expensive performance-wise (imagine rehashing the entire multi-gigabyte history of the Linux kernel every time to sign and verify a commit) and destroy git functionality such as shallow clones and blob-less clones.

If you by recursive you are only referring to the current working directory, as I lay out here https://news.ycombinator.com/item?id=49930048 it doesn't work. Indeed, without attestation of parent commits, a malicious attacker can actively frame any pre-existing vulnerability as someone else's handiwork by simply inserting a new commit that purports to be the parent of another commit that does not contain the vulnerability, which then makes the original commit look like the source of the vulnerability.

"I didn't introduce the vulnerability, he did! Look I can even prove it with my signed commit!"

> We can round up the bits that make up a commit in a SHA-1-based repo, and sign those bits securely; this is a thing that is possible.

Yes but as my other comment explains, this is not particularly useful in and of itself.

> it would be good enough that the meaning of a commit signature is that the content of the commit is attested, not the parents.

This is a significant degradation of the implicit guarantees given by a cryptographic signature, to the point that basically all personal use cases I have for signed commits would be invalidated.

Keep in mind that git does not have diffs as first-class objects. Every commit is just a snapshot of some state of the working directory. That means that without attesting to the integrity of the parents of a commit, the only thing a commit X signed by a person A says is "at some point on A's computer, the state of the repo looked like X".

Almost all the relevant questions I would want to ask are not answered by this. E.g. there is a malicious function F that is present in X. Did A write it? Don't know. Did someone else write it? Can't know for certain. Who introduced a certain feature? Don't know. Did A sign off on a new bugfix? Don't know.

All you know is that at some point the codebase looked like X on A's computer. A might not have made any relevant changes at all!

You can only back out a diff and therefore actually attribute a change to someone (either explicitly through `git blame` or informally by looking at git logs) if you have attestation of the parents.

The Merkle tree structure of git repos is interwoven through basically ever useful thing git does. Without cryptographic signatures implicitly carrying a promise of validity for that structure, this would make commit signing useless (depending on just how broken SHA-1 is) for the needs of any org I've ever worked at.

> it is not a logically deductive necessity that we just scan the topmost object and trust the hashes it contains.

It kind of is. Otherwise the whole idea of signing a commit with a backing git history (rather than just a snapshot of a working directory) collapses. The only guarantee you have that the git history is what is claimed by the cryptographic signature is some sort of Merkle tree structure. Either the original one, or you have to construct a whole new parallel one with a better hash, in which case, as I bring up in a cousin comment, why not just use a better hash in your original one?

> If that's how it works, that is massively stupid and can be fixed without forcing SHA-256 as a git hash.

I don't think it's massively stupid. Unless you want to re-hash the entire Merkle tree structure to sign your commit, you basically have to trust the hashes in the Merkle tree (or have a separate parallel Merkle tree) at some point in what you sign, which means you do have to trust the SHA-1 hashes. Otherwise even with a cryptographic signature you can always spoof at least the git repo history (e.g. even if you try to directly hash the entire contents of the current commit).

Re-hashing the entire Merkle tree structure seems prohibitively expensive to generate (even with a lot of caching) and pretty complicated for e.g. verifying a signature. Or you can do that incrementally, but then you're just generating a whole new parallel Merkle tree structure.

Regardless, at the end of the day, you need to trust the integrity of the Merkle tree structure. And you can either do that by trusting the hashes of the current Merkle tree, or you have to completely recreate a new one with more trustworthy hashes, in which case why not just use better hashes in your original tree?

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.