LessWrong 2.0 Reader

I don't believe this is true, actually! What do you mean by "resolve the conjecture"? If you mean write up with a proof of it, then of course you can write a turing machine that will write a proof of the conjecture, it's just infinite monkeys. ZFC is best thought of as the "minimal set of axioms to do most math". It's not anything particularly special. You can have various foundations such as ETCS, NF, Type theory, etc. If we have a model that can genuinely reason mathematically, then the set of axioms the model uses should be immaterial to its mathematical ability. In fact, it should certainly be able to handle more or less axioms, like replacing full choice with countable choice etc. Maybe I misunderstood your point here.

My point was to gesture at the fact that open conjectures can be so hard that neither humans nor AI can solve them in reasonable time, and that it's too hard to determine whether a conjecture is even provable by an AI or human in reasonable time, so the proving open conjectures benchmark is not a great benchmark, and I was using independence of ZFC as an example of such conjectures.

Also, a Turing Machine in that case (where a statement is independent but not recursively independent) will only prove independence from ZFC, not a proof or disproof of the conjecture.

More here:

https://x.com/ElliotGlazer/status/1871121633018331499

But my point was that there are things that should be extremely easy, like proving lemmas about elementary row transformations, that have not been done in Lean yet. That is not due to a lack of people formalizing, but due to fundamental limitations with the proof assistant. The point that I'm failing to make explicit is that this seems like a copout. The ultimate naturalistic benchmark for an LLM's math ability is being able to formalize the undergraduate math curriculum! But it starts with having a proof assistant that is amenable to the formalization project, which seems to be the bottleneck today.

I definitely would think that formalizing an entire undergraduate math curriculum would be a great benchmark, but it would have to be designed very carefully to ensure the LLM doesn't break the benchmark's usefulness.

Also, when you state that it's extremely easy to formalize certain lemmas/theorems, are you saying that it's easy to formalize them flat out, including all necessary details, or are you saying that it's easy to give a paper that would be accepted by mathematicians, and if necessary (though the journey may be painful) you could formalize the argument, including all necessary details?

Bonus question: What do you think are the current limitations of proof assistants such as Lean, more specifically?

Thanks for the links. Might go through when I find time.

Even if the papers prove that there's similiarities, I don't see how this proves anything about evolution versus within-lifetime learning.

But there's decent evidence that there's not much more initialization than that, and that that huge fraction of the brain has to slowly pick up knowledge within the human lifetime before it starts being useful, e.g. https://pmc.ncbi.nlm.nih.gov/articles/PMC9957955/

This seems like your strongest argument. I will have to study more to understand this.

our DNA has on the order of a megabyte to spend on the brain

That's it? Really? That is new information for me. 

Tbh your argument might end up being persuasive to me. So thank you for writing them.

The problem is that me building a background in neuroscience to the point I'm confident I'm not being fooled, will take time. And I'm interested in neuroscience but not that interested in studying it just for AI safety reasons. If you have like a post that covers this argument well (around initialisation not storing a lot of information) it'll be nice. (But not necessary ofcourse, that's upto you)

I totally agree. I think it's another framing for why open-ended RL is much more dangerous than pure LLMs. Models trained with open-ended RL are rewarded based on their final results, and will produce any series of tokens that help with that. They are incentivized to produce CoTs that do not logically represent their true thinking. 

Pure LLMs, on the other hand, have no desire other than making the next token as likely as possible, given whatever character they are currently simulating. Whether they are "good" or "bad", I can't see anything in their training that would incentivize them to develop an efficient secret language to communicate with their future selves in a way that produces misleading CoTs.

Before I attempt to respond to your objections, I want to first make sure that I understand your reasoning.

I think you're saying that in theory it would be better to have CoT systems based on pure LLMs, but you don't expect these to be powerful enough without open-ended RL, so this approach won't be incentivized and die out from competition against AI labs who do use open-ended RL. Is it a faithful summary of (part of) your view?

You are also saying that if done right, open-ended RL discourages models from learning to reason strongly in the forward pass. Can you explain what you mean exactly and why you think that?

I think you are also saying that models trained with open-ended RL are easier to align than pure LLMs. Is it because you expect them to be overall more capable (and therefore easier to do anything with, including alignment), or for another reason? 

In case it helps to clarify our crux, I'd like to add that I agree with you that AI systems without open-ended RL would likely be much weaker than those with it, so I'm definitely expecting incentives to push more and more AI labs to use this technique. I just wish we could somehow push against these incentives. Pure LLMs producing weaker AI systems is in my opinion a feature, not a bug. I think our society would benefit from slower progress in frontier AGI.

Would you personally answer Should we be concerned about eating too much soy? [LW(p) · GW(p)] with "Nope, definitely not", or do you just find it's a reasonable gamble to take?

Btw, thanks a lot for the post; MANY parallels with my past as more-serious-but-uncareful-vegan until body showed clear signs of issues that I realized only late as I'd have never believed anyone that healthy vegan diet is that tricky.

They've probably scaled up 2x-4x compared to the previous scale of about 8e25 FLOPs, it's not that far (from 30K H100 to 100K H100). One point as I mentioned in the post is inability to reduce minibatch size, which might make this scaling step even less impactful than it should be judging from compute alone, though that doesn't apply to Google.

In any case this doesn't matter yet, since the 1 GW training systems are already being built (in case of Nvidia GPUs with larger scale-up worlds of GB200 NVL72), the decision to proceed to the yet-unobserved next level of scaling doesn't depend on what's observed right now. The 1 GW training systems allow training up to about 5e27 FLOPs, about 60x^[1] the currently deployed models, a more significant change. We'll see its impact in late 2026.

I hope I will get around to rereading the post and edit this comment to write a proper review, but I'm pretty busy, so in case I don't I now leave this very shitty review here.

I think this is probably my favorite post from 2023. Read the post summary to see what it's about.

I don't remember a lot of the details from the post and so am not sure whether I agree with everything, but what I can say is:

1. When I read it several months ago, it seemed to me like an amazingly good explanation for why and how humans fall for motivated reasoning.
2. The concept of valence turned out very useful for explaining some of my thought processes, e.g. when I'm daydreaming something and asking myself why, then for the few cases where I checked it was always something that falls into "the thought has high valence" - like e.g. imagining some situation where I said something that makes me look smart.

Some survey articles:

https://arxiv.org/abs/2306.05126

https://arxiv.org/pdf/2001.07092

The difference is that the weights are not initialised with random values at birth (or at the embryo stage, to be more precise). 

The human cortex (the part we have way more of than chimps) is initialized to be made of a bunch of cortical column units, with slowly varying properties over the surface of the brain. But there's decent evidence that there's not much more initialization than that, and that that huge fraction of the brain has to slowly pick up knowledge within the human lifetime before it starts being useful, e.g. https://pmc.ncbi.nlm.nih.gov/articles/PMC9957955/

Or you could think about it like our DNA has on the order of a megabyte to spend on the brain, and the adult brain has on the order of a terabyte of information. So 99.99[..]% of the information in the adult brain comes from the learning algorithm, not the initialization.

How much predictive power does this analogy have as per you personally?

Yeah, it's way more informative than the evolution analogy to me, because I expect human researchers + computers spending resources designing AI to be pretty hard to analogize to evolution, but learning within AI to be within a few orders of magnitude on various resources to learning within a brain's lifetime.

"...you learn that there's three kinds of intellectuals. There's intellectuals that work in one frame. There's intellectuals that work in two frames. And there's intellectuals that change frames like you and I change clothes."

It's as efficient to work on many frames while easily switching between them. Some will be poorly developed, but won't require commitment and can anchor curiosity, progress on blind spots of other frames.