I’m an AGI safety / AI alignment researcher in Boston with a particular focus on brain algorithms. Research Fellow at Astera. I’m also at: Substack, X/Twitter, Bluesky, RSS, email, and more at this link. See https://sjbyrnes.com/agi.html for a summary of my research and sorted list of writing. Physicist by training. Leave me anonymous feedback here.
Steven Byrnes
Karma: 32,164
My understanding (for various reasons including this tweet from an ex-OpenAI post-training engineer) is that OpenAI has been creating and checking proofs purely in natural language, and then Lean-formalizing them as an optional second step, only after they believe that they have a complete and correct natural-language proof.
I think it’s unlikely but not completely impossible that we could be in a situation where the Lean-formalization step always “works”, even for broken proofs, but where nobody at OpenAI has yet noticed that there’s something fishy going on with their Lean-formalization workflow.
Nice, yeah I’d also be curious about this.
Some of this will happen organically as experts digest the results. I’ve found a bit of relevant information already, but will refrain from commenting, everything will be clearer in a few weeks.
Many people expect the AI paradigm to approximately AGI complete, and expect it to smoothly scale to AI that can do innovative science. i.e. the kind of science you’d need to do to develop a plague from scratch that actually kills all humans, with very limited opportunity to experiment … A periodic thread of disagreement has been TsviBT, Steven Byrnes and some others arguing that, yes, the AIs are getting better at verifiable tasks, but they still seem to be missing some basic sauce that lets them actually form new concepts on the fly and apply them …
(For the record , I’ve long been a strong advocate of (something in the vicinity of) “LLMs can’t form and use novel concepts”, but am somewhat more agnostic on “…and therefore we needn’t worry about LLMs killing everyone / taking over”. I’m optimistic about the latter, but wouldn’t make a much stronger statement than that. Cf. recent discussion here.)
I think you can find lots of examples in the Sequences (and elsewhere) of Eliezer doing poor reasoning or believing things that are in fact false, but I claim that your OP example is not among them. I think my comment above responded to most of your specific complaints.
One additional complaint that I didn’t bother responding to above: if a probability teacher says “imagine flipping a coin a billion times”, would you raise your hand and say “Excuse me teacher, but nobody can actually picture a billion coinflips in their mind’s eye!” No, that would be silly. That’s being pedantic, or else being unable to grapple with of how imagination works. Or perhaps your own imagination doesn’t work that way, in which case fine, but that doesn’t apply to other people, and don’t begrudge them a helpful-to-them way to think.
Anyway, I can imagine some world where there’s a second edition of the Sequences, where we remove the citations to bad p-hacked psych studies, incorporate new-and-improved ideas and frameworks from the subsequent 18 years, and so on. That would be nice but alas I don’t see how that would ever happen: Eliezer has health problems and anyway he and everyone else who might get involved is too busy with AI x-risk. It’s too bad, really. I still recommend The Sequences on occasion as an important source of ideas, and am very happy to have read it myself. We can keep the good ideas, ignore the things that seem bad or unhelpful, and note which parts of it people are still relying on versus what’s irrelevant or obsolete. Just like any other source, I suppose.
Some takes on this post:
A writing style that some people find very appealing, other people will find insufferably annoying. Oh well.
Attempted-pedagogy that some people find helpful, other people find unhelpful and distracting. Oh well.
Eliezer has a bunch of unusual mental images and framings for things that I happen to find helpful, and often use. And of course, many others that bounced off of me.
If you just straightforwardly write something true, like “wishful thinking doesn’t work because I want $1000 to be in my wallet but it’s not there”, people will heartily agree, and then fail to apply it in a different context. Using lots of different mental images, and lots of different framings, and lots of different examples, can help a bit.
Unlike a classroom teacher, Eliezer did not have a captive audience, so he had to balance “clearly communicating his message” against “keeping people engaged, who might otherwise click away and never come back”. I think he struck a reasonable balance, but that’s just me, obviously opinions differ, especially the many people who find his writing insufferably annoying. Oh well.
People who read everything Eliezer has ever written sure don’t come out the other end perfectly rational, but nobody should have expected that.
It’s hard to make a simple and correct point without using examples that pedants can nitpick
E.g. it is in fact true and important that wishful thinking is irrational, but it’s also true that there are special circumstances where self-fulfilling prophecies are an important dynamic to keep in mind.
I call this a “nitpick” rather than an “error” because it is in fact true that the random chatroom participant’s beliefs about the likelihood of nuclear war have approximately (if not literally) zero causal impact on whether nuclear war will happen, so that person really should just be trying to figure out what’s true.
(I would say that they should just be trying to figure out what’s true even if self-fulfilling prophecies are a relevant dynamic, but that’s certainly a less obvious claim. Probably Eliezer talks about this at great length somewhere in the Sequences, but I don’t remember the details.)
(Even when wishful thinking is a relevant dynamic, visualizing a billion possible universes does not make it inherently harder to notice that fact, insofar as you find it helpful to visualize a billion universes in the first place. Like, if an optimistic attitude causes such-and-such consequence, then that would obviously create a correlation between the attitudes and the consequence across the billion universes.)
Eliezer has sometimes been wrong about things, although I would disagree that the excerpt in the OP should qualify as an example.
You might know more than me, but as of right now Wikipedia “Navier–Stokes priority controversy” does not make it sound so clear-cut that “it couldn’t have happened”:
…
13 September, [OpenAI spokesperson Laurance] Fauconnet: “After investigating, we can say with full confidence that no user inputs past July 3rd could have influenced this system in any way.”
No comment has since been made about the heavy use of Codex before July 3rd being potential training data for Astra.
(I can’t immediately find discussion of what progress Buckmaster & Alpöge had made before vs after July 3.)
(For the record, I’m currently at a (very lightly held) 70% that important information leaked from Buckmaster & Alpöge to OpenAI, mostly based on Buckmaster’s sentences from here: “They didn’t use 10,000 agents to get to the Euler problem; they used 100 agents. So they worked from absolutely nothing with only 100 agents. And that is key, the number of agents, because it means how wide you can search. They used 100 agents and then ended up with an identical architecture to what we had.”)
(I wouldn’t necessarily describe 100 agents with the word “only”, but it’s still relevant evidence. The “identical architecture” part is more important to me.)
(Unrelatedly, this might be dumb, but is it known for sure that no LLM agents were just, like, hacking into mathematicians’ computers? I dunno.)
Thanks!
If it’s true that “humans have an easier time because they bootstrap a world model and then learn language on top of it”, why would you contextualize that as, like, “…and so humans aren’t really data-efficient, that doesn’t count, it’s cheating”, rather than as “…and perhaps this is part of the explanation of how humans manage to be so data-efficient”?
suggesting model capabilities are limited using hominid metaphors has rarely done any good for anyone
I think it’s valid and useful for people to point out things that human brains can do that AI engineers can’t (yet) do, because human brains provide a convenient existence proof that the thing in possible at all. For example, (copying from a different comment) as of today, I strongly believe that there is no known learning algorithm that can start from random initialization, spend the equivalent of 2 waking years roaming around and doing stuff in various virtual environments like VR & Minecraft, occasionally happening upon people who are talking to each other about whatever, and/or watching YouTube videos, such that the model winds up at the end with the linguistic and other competences of a human 4yo. You sure can’t train an LLM that way. LLMs need (pre)training data, humans instead need a training environment. It’s very different.
But when (as above) someone points out a thing that human brains can do that AI engineers can’t (yet) do, I feel like you’re not treating that as an neutral observation about AI-algorithm-possibility-space, but rather as a front in the war over what we actually care about, which is whether we should be more impressed by human brains versus LLMs. And you’re fighting for the yay-LLMs side and they’re fighting for the yay-brains side. And indeed fighting this war is a popular activity on both sides. But that’s a waste of time, because this is a “meaningless argument” in the Scott Alexander sense. Really we should all be very impressed by both human brains and LLMs in their own ways, and then we should move on to arguing about more concrete and specific things.
I would say LLMs can actually learn language in a way that humans probably would not be able to do from scratch.
Yeah I probably agree.
It really doesn’t appear to me that there’s a straightforward comparison for language learning efficiency of LLMs versus humans, and probably both are better in certain senses.
I agree here too. Like I said, it’s hard to pin down an apples-to-apples comparison between human learning and LLM pretraining, because human learning is just a totally different thing from LLM pretraining. Best to ask more specific questions.
(But I stand by my belief that the gist of the OP is mostly wrong and misleading.)
I also think that the evidence you’re raising about people in other cultures giving children less attention is pretty weak. It seems to mean relative to western parenting, versus “not at all” or “sparsely” in some statistical sense. Also I don’t want to dig through that entire post, when it seems maybe one paragraph is relevant.
Yeah my claim was “western culture vastly overstates…” which I stand by. The relevant sections of Notes on “The Anthropology of Childhood” include “How do children learn?” and “How children are expected to speak”.
It seems like (in those cultures) 1yo toddlers might often be supervised by somewhat-older siblings, peers, etc., and I’m a bit unclear on what kinds of interactions they’d have. (I doubt it’s “deliberately teaching”, except for things like yelling at toddlers not to wander off in dangerous areas (cf. the “Chewong” excerpt). But maybe there’s other kinds of playful interactions between toddlers and older kids?)
Anyway, I put in that summary quote (“everyone waits until the child can talk sensibly before acknowledging its existence”) because it’s from the author and I figure he would know. His tone throughout the book is pretty careful as opposed to sensationalizing and exaggerating, IMO.
(I read the whole book, but that was a decade ago so my memory is a bit hazy. Julia’s excerpts are good.)
Do you think that a blind child who everyone ignored would learn to speak fluently? Intuitively I doubt it, though I’m not that confident.
It’s a bit pointless to argue since we don’t know the answer. Oh well: My guess is yes (assuming they survive), because I think little blind kids, just like little sighted kids, are generally capable of learning how the world works, and what’s what, and learning intuitive physics and intuitive biology and so on. It’s restricted to tactile and auditory for the blind kids, and for all I know it might take somewhat longer, but they still get there. And so they’re still in a position to connect overheard words to relevant objects and situations, just like the sighted kids are. (Again, maybe it would take somewhat longer, but I’d guess not overwhelmingly longer.)
If people kept ignoring the kid, they would sure have a lot of unanswered questions, e.g. about how to identify some plant by touch if everyone else is talking about its color. But that would be after the kid is fluently talking about more basic things like rain and beds and inside and mud and fighting etc., that blind kids can easily develop an intuitive understanding of by autonomous nonverbal exploration and sensing.
a lot of the brain’s data is kinesthetic/proprioception
Sure! A proper accounting of “how many sensory bits” should certainly include all the senses, including proprioception, tactile, interoception, and so on. (But those are OOMs fewer bits than vision, if I recall correctly.)
Do there exist blind + deaf + nonproprioceptive people who seem smart (or, survive at all?)
Lacking proprioception is super-rare. The most famous example is Ian Waterman, who lost all proprioception at age 19 (they think he got a random minor infection, and by terrible luck, the immune system response happened to also false-positive upon his own proprioceptive nerves, or something like that). There was a neat little BBC documentary about him.
On a quick search, it seems like a congenital absence of proprioception is something that’s happened in like two documented cases ever, and those two were not blind.
Putting proprioception aside: I think congenital deaf-blindness is a thing (I heard that congenital rubella syndrome can cause it) and such people can indeed acquire language in childhood.
I think that western culture vastly overstates the importance of deliberately teaching things to young children. There are cultures where “everyone waits until the child can talk sensibly before acknowledging its existence”, and the kids still learn to talk just fine. See Notes on “The Anthropology of Childhood”.
I don’t think your thought experiment is quite right: if I understand correctly, LLMs get pretraining data of different modalities coupled together; they don’t have to discover on their own a correspondence between a text corpus and a completely disconnected vision corpus.
Anyway, it’s definitely hard to pin down an apples-to-apples comparison between human learning and LLM pretraining, because human learning is just a totally different thing from LLM pretraining. See “LLM pretraining magically transmutes observations into behavior, in a way that is profoundly disanalogous to how brains work”. LLMs have pretraining data, humans are more like RL agents in that there’s a training environment. A fun example is Nicaraguan Sign Language, or pidgins turning into creoles, where a group of kids who have never seen a grammatical language in their life simply create one. What would be the “sample efficiency” of that? They’re learning grammatical language from exactly zero samples!
As of today, I strongly believe that there is no known learning algorithm that can start from random initialization, spend the equivalent of 2 waking years roaming around and doing stuff in various virtual environments like VR & Minecraft, occasionally happening upon people who are talking to each other about whatever, and/or watching YouTube videos, such that the model winds up at the end with the linguistic and other competences of a human 4yo. You sure can’t train an LLM that way. How would it ever take intelligent action?
Maybe you’ll say: Well, we raise humans in an appropriate environment built for humans, and we “raise” LLMs in an appropriate environment built for LLMs. Each would do badly if put in the shoes of the other. And my response would be: Yeah, sure, whatever, I think it’s obvious that LLMs can do things that humans can’t and vice-versa, and I’d like to avoid a getting into a vague and pointless argument about which of them is “more impressive”. Those arguments tend to be divorced from any concrete question and unhelpful for understanding.
I disagree, see some relevant discussion here (me) and here (Dwarkesh).
40 gigabytes of text is about how much a person would say if they spoke nonstop for 8 hours a day, 7 days a week, for 250 years.
Preschoolers learn language much faster than that.
You can argue that vision transfers to language, but blind preschoolers also learn language much faster than that.
You can argue that hearing-bird-songs-or-whatever transfers to language but (1) really? (2) that doesn’t add much.
You can argue that the full data-heavy audio waveform (as opposed to just the words per se) makes the language learning task dramatically easier, but (1) that seems like the exact opposite of what we should expect, i.e. I’d assume that one of the hardest computational parts of language acquisition is learning to ignore the countless aspects of the auditory waveform over which the linguistic content is invariant, (2) deaf-blind preschoolers also learn language much faster than that.
In model-size terms, how large is a preschooler?
I’m not sure why you’re bringing up parameter count in a post about data efficiency. You can argue that LLMs are more data-efficient than brains, or you can argue that brains are more data-efficient than LLMs because brains have a higher parameter count, but it’s weird how you seem to be arguing both at once.
(My own opinion, stated without justification, is that brains are more data-efficient than LLMs for reasons unrelated to “higher parameter count”.)
No, I definitely find AI x-risk takes I disagree with to be more emotionally taxing than ones I agree with, and thus (other things equal) am more likely to avoid them. That was my main point, and I was using the Ukraine war as an uncontroversial analogy to illustrate the idea that when things are emotionally taxing, it’s an actual cost and there’s nothing inherently wrong with taking that cost into account when you only have so much time in the day and only so much emotional energy and mental health.
I think there’s a strong temptation to judge people you disagree with on meta-level grounds: they broke the rules of thinking, they spent their time incorrectly, etc. But it’s very hard, if not impossible, to come up with meta-level rules of that type that would lead to results we like in every case. Like, “listen equally to both sides” sounds nice on paper, but I sure don’t want geologists to dedicate precisely equal amounts of their literature-search time reading mainstream geology papers versus young-earth creationism papers.
Sometimes you just have to drop down to the object level. Sometimes the problem is just that people have gotten the wrong object-level answer on an important matter. Everything else is commentary.
I’m comfortable ignoring Marc Andreesen’s AI takes because I’m really damn sure that his takes are nonsense, having spent enough time and effort to reach that conclusion to my own satisfaction. Meanwhile somewhere in the world, there’s probably some guy who thinks analogous thoughts about Steve Byrnes’s AI takes, and consequently decides to ignore those. If I saw the latter happening, I would be sorely tempted to say that this guy is bad because on general principle, people shouldn’t ignore other people. But I can’t say that! It would be hypocritical. Ignoring people per se is not where I think they went astray. The problem is that you really really have to get the right answer on the question of which people to ignore! Again, no escaping the object-level.
I think this OP clearly applies to some people and clearly doesn’t apply to other people. I’m reluctant to broadly disagree, because we’re probably just thinking of different prototypical cases.
But insofar as this post arguably applies to me, I will defend myself.
I try to avoid content that upsets me unless consuming it has a benefit that outweighs that cost. For example, I don’t routinely read general world news (outside my professional interests), with narrow and rare exceptions. And I stand by this as a great idea (see e.g. 1, 2), mainly because I find it upsetting and addictive and distracting, and the benefits of being up-to-date on the news are tiny and don’t outweigh those very real costs.
By the same token, if someone is posting bad takes on a topic I care about (say, AI x-risk), then I find it frustrating and addictive and distracting, and that’s a real cost, and we can ask whether the benefits outweigh the costs. In some cases, yes the benefits do outweigh the costs. Maybe the bad takes are bad in interesting-to-me ways that fit into some foreign-to-me world-model that I would like to understand better, or maybe it’s a corner of the discourse such that I may want to rebut it (e.g. I’m much more likely to reply to bad takes from neuroscientists [because I can engage with their expertise], or from x-risk-is-dumb-because-LLMs-won’t-scale-to-ASI people [because I can concede their whole argument but then explain why it’s not a crux for x-risk], or from leaders at my own organization), etc. But in many other cases the benefits are very low, and don’t outweigh the costs. Like, my strong belief is that the benefit of me reading a bunch of Marc Andreesen tweets about AI are just very small; I think there’s an extremely low chance that I would wind up with importantly different beliefs, or take importantly different actions. So I won’t follow those people on twitter, or read their stuff (unless it’s been specifically recommended to me), etc.
(I rarely block on twitter because I never look at the twitter algorithmic feed in the first place. I use twitter-lists, which are more like a white-list, which I guess you would say is even worse than blocking. And I’m currently not famous enough and don’t tweet enough to get many unwanted replies.)
When you say:
They’re protecting their egos from signal that would hurt their feelings, cocooning themselves away from information that might challenge what they would prefer to believe. Someone protecting their time might mute someone for being boring, but not for “being a dick.”
I think this is conflating a couple different things. Again, I find it very upsetting to read about the state of the Ukraine war, and there’s not much I would do with that knowledge regardless, so I only catch up on my Ukraine war news a couple times a year. Am I “protecting my ego from signal that would hurt my feelings”? Umm, kinda? But not in a bad way. Am I tuning out from it because it’s boring? No, my actions there are specifically because it’s upsetting, not boring. Am I protecting my time? Yes, but my time is not the main thing, it’s more about emotional energy and mental health. And also, the time I’ll spend literally reading the words of the article is probably much smaller than the time I’ll spend feeling distracted and upset afterwards.
Sure, there’s also the general rule-of-thumb that if people have true beliefs about how the world works, then they’re more likely to take good actions and make things better, and those might be actions that I never would have thought of myself.
E.g. almost nobody wants human extinction from future AI, so if human extinction from future AI happens, it would probably happen mainly as a result of people being mistaken or ignorant about important aspects of future AI.
Of course it’s possible for there to be “uncanny valley” U-shaped curves where a person makes OK decisions, and then gains a little knowledge and makes worse decisions, and then gains even more knowledge and swings back to good decisions. But I’m much more inclined to go with the rule-of-thumb above than trying to play 4-D chess about people’s beliefs.
In regards to brain-like AGI, I feel like “they might do the PNSE thing” is a relevant dynamic / possibility to keep in mind.
Would it be useful? I think I don’t have much opinion. My baseline assumption is that PNSE people are approximately just as kind / unkind as non-PNSE people (as discussed in that other comment thread, see also here), and I think I’m reluctant to update very hard on self-reports just because my experience researching this post was that the self-reports are evidence of something, but they’re generally hard to interpret and often shouldn’t be taken at face value. Is there any way to get stronger evidence? Like I dunno, probably PNSE people are disproportionately vegan but that’s hopelessly confounded with the influence of Buddhism. Do they give more to charity? Do third-parties report that they get angry less often? I recall people self-reporting that they’re behaving totally differently, but their friends and family don’t notice much difference if any.
It’s also possible that a superintelligence would almost inevitably eventually wind up in PNSE. I’m not sure. But if so, we’d presumably want that to happen early on, because maybe something weird would happen during the switch, and it would be good to observe that before the AI gets too powerful to control.
Looking forward to whatever you write :)
terrible for productivity and relevance
(Explaining my react.) I agree denotationally: the cost is real, and big, and people often under-weight it. I disagree with the connotation that it couldn’t possibly be the right decision despite that cost. It might or might not be, at least in principle. (This probably isn’t worth arguing about in the abstract; different situations are different.)
I think you’re missing my point. AFAIK there is no harm whatsoever in spreading the message of FDT or logical probability far and wide, and never has been. Yudkowsky could have taught these esoteric technical philosophy concepts to every last person on Earth, via extremely clear and viral explainer videos, and it wouldn’t have mattered at all to the ASI race. Then 8 billion people would know some random facts about technical philosophy, but none of them would have been spurred to found AI companies. The thing that (at least somewhat) mattered to the ASI race was spreading the message about how ASI could happen soon and what it big deal ASI would be. That’s a different message. The first is some technical content, the second is explaining why we should urgently care about that technical content. Right?
I agree that it’s common for researchers to not only communicate their findings but also to communicate why people should care about their findings. But it’s not necessary. A person can just publish papers like this one that they think are important for superintelligence safety without spelling out why superintelligence safety is an important cause area. Eliezer could have done that too.
(Obviously this is academic; at this point, the horse has long ago left the barn and there is no longer any reason whatsoever not to tell people that ASI risk is an important cause area. And also I still think Eliezer made a good decision on balance to spread the message back in the day that ASI risk is an important cause area, if you weigh the costs vs benefits of that outreach.)
Maybe it’s just that your post was confusing to me?
For example, one thing I would say is: “Sometimes you’re playing with early-stage ideas, and it’s unclear whether the ideas will ultimately be helpful for ASI safety or ASI capabilities or both or neither. If so, it’s often wise to keep those ideas secret until you have a better understanding of the lay of the land, and the answer is more clear. And THEN you can decide to publish those ideas, or alternatively decide to bury them.”
If that’s one of the things you were trying to say, then it didn’t come across to me in your text.
Like, your discussion of secrecy seems to imply that the idea is to keep all the work secret perpetually. It doesn’t mention selectively publishing things eventually, when it’s clear that those things are safety-promoting.
Likewise, your list of things to “make peace with” doesn’t include the possibility that your work is something that ASI capabilities researchers will have to figure out sooner or later on the way to ASI capabilities, regardless, so the right thing to do is bury it and find something else to do instead, because someone else will have to figure it out before ASI anyway. Instead you seem to imply that the only bad possibilities to worry about are that your research plan is technically unsound or proceeds too slowly.
See what I mean?
Example: MIRI and Recursive Self-Improvement
This section seems kinda weird to me. It seems plausible that Yudkowsky / MIRI got us to where we are today (e.g. GPT-6) sooner than otherwise, although the reverse also seems plausible for all I know. E.g. AlexNet had nothing to do with Yudkowsky, and I don’t think ULMFiT did either, and that led straight into LLMs, right? Maybe without Dario it would have taken another year or two? Whatever, I don’t really know either way, I’m not an expert on that.
But insofar as Yudkowsky / MIRI brought GPT-6 sooner, that seems almost entirely unrelated to the technical safety / alignment research that they did, but rather related to spreading the idea that ASI is a really really big deal, and dangerous, perhaps also the DeepMind Thiel intro. I really don’t think functional decision theory or probabilistic logic etc. had anything to do with today’s AI race.
(I acknowledge that there are also places, especially early on, where “spreading the idea that ASI is a really really big deal, and dangerous” overlapped with “technical ASI alignment / safety research”. E.g. things like IEM and Bostrom’s Superintelligence are a mix of both. But I still think they can be pulled apart pretty well. Like, if Eliezer had wanted to spread the idea of ASI less far, he easily could have written dry technical papers that would have been widely ignored except by other people in the still-infinitesimally-small field. He chose not to do that. I.e., he was making two separate decisions, one to do technical alignment research, and another to do field outreach. The latter was what led to unintended acceleration of capabilities, not the former, right? I don’t see any bad side effects of the former, and while it turned out that the research did not lead to a solution to the technical alignment problem, I still think it produced some good resources and “deconfusion”, e.g. I read and cite Yudkowsky’s Arbital articles regularly.)
I did mention that in footnote 3.
But I will defend my title.
First, I’m not sure what you’re thinking about, but for me the context of a post like this is “we want to refine our nuts-and-bolts understanding of LLM capabilities”. I.e., LLMs can often do all these very impressive things; we can ask: how and why? This is an obvious and centrally important question. It helps us understand the world, and helps us predict future progress, etc. In that context, you want to know what goes into LLM capabilities in terms of their immediate inputs: what role is training data quality playing, what role is neural architecture playing, etc. etc. If training data quality is the critical factor for such-and-such aspect of LLMs, then we can separately chat about what goes into training data quality, but that discussion topic is now a step removed from understanding LLM capabilities, which again is the conversation that this post is participating in.
Second, I think “verifiability” is more subtle than you’re suggesting. Imagine Lean or other formal verifiers didn’t exist today. Then human mathematicians would still be able to do math. After all, humans were doing math for thousands of years before the any formal verifier existed. In that hypothetical universe, what would it mean to say that natural-language proofs are “verifiable”? It really means that humans can reliably come to a consensus on proofs being right or wrong. But this is a joint property of a domain and a specific community of humans. I have on a few occasions argued for hours, days, even weeks, with morons / cranks about the validity of math proofs and derivations, and boy let me tell you, we did not reach any consensus. Mathematicians have developed social technologies to keep the cranks out, to double-check proofs, etc., and that’s an essential ingredient in math literature quality.
So (still in this imaginary universe where nobody has made a formal verifier), the claim “math is verifiable” is pretty dubious, at least in the context of natural-language proofs. If you assume everyone is perfectly rational and infinitely patient, then practically every domain is “verifiable” (including philosophy, futurism, etc.) by Aumann Agreement Theorem. Conversely, if you assume everyone is a random crank, then practically no domain is “verifiable”, not even natural-language math proofs. Again, pretraining data quality is a complex function of the domain and the human community of practice.
(And my claim in the OP is that people could get LLMs to be pretty damn good at natural-language math proofs even in a universe where formal verifiers didn’t exist. I have various reasons for thinking that, including a chicken-and-egg complaint about the story where autoformalization precedes LLM proof skills.)
One of the things is in §1 of my post “Sharp Left Turn” discourse: An opinionated review, or my linear algebra thought experiment. Like, if an LLM comes up with some new mathematical construction, then that construction exists only in its context window, not its weights, which is fine if it’s just one new construction but rapidly hits limits if you want to build giant new edifices of new concepts built on top of new concepts etc. The context window can’t handle all that, rather the “knowledge” has to somehow get into the weights.
So then people will say “Well humans can’t build giant new edifices of new concepts built on top of new concepts either”
and then I’ll say “Of course they can; the most magnificent example is that billions of humans over thousands of years built all knowledge from scratch”
and then they’ll say “Well the context window is just gonna keep growing”
and then I’ll say “It’s not about length, it’s about serial complexity, again see that linear algebra thought experiment thread”
and then they’ll say “OK fine, we’ll set up the LLM to produce math proofs and then automatically fine-tune on them”
and then I’ll say “I think that would go off the rails because it will make a few mistakes and then when we fine-tune on those mistakes it will get dumber and make more mistakes in a vicious cycle”
and then they’ll say “we’ll Lean-verify before we feed a proof back in”
and then I’ll say “sure that might work in principle, but isn’t it interesting that humans don’t need anything like that to do math? And also, that works in math but not in lots of other domains.”