The Thermodynamic AI Computing Chip - Thomas Ahle

Thomas Ahle wants Normal Computing to be the Lovable for chip design: type your intent, and a swarm of agents carries it from design through optimisation, formalisation and verification to tape-out. To get there, his team at wrote their own open-source Verilog simulator, 580,000 lines in 43 days, because commercial EDA verifiers run about $10,000 per core and there are no decent open-source compilers to build on. That sets up the question Tim keeps pressing: if an agent can produce a chip design, a proof, or a working program, how do you actually know it is correct? Passing 70% of tests is not the same as being right, and a single fabricated bug can cost a company a fortune. They dig into ProgramBench (rebuild a program from its tests, roughly 0% success), the difference between structure and competence, and the "understanding debt" you take on when nobody reads the code. From there: auto-formalisation in Lean and the AlphaProof trick of training on prove-or-disprove; why there is no single true representation of a spec (Petri nets, TLA+, Erik Curiel's "math does not represent"); and thermodynamic computing, where Normal Computing's CN101 chip is built so that its physical noise *is* the computation, settling a stochastic differential equation in hardware to invert a matrix. Plus Bayesian uncertainty, specialisation, the Chomsky hierarchy, AI slop, and whether performance is all that matters. Recorded in Zurich. Disclosure: Normal Computing paid our production and travel costs for this show. We retained full editorial control. They did not see the video before publication, and we did not show it to them or discuss it with them beforehand. --- TIMESTAMPS: 00:00:00 Meet Thomas Ahle: the Lovable for chip design 00:03:41 Why hardware needs formal verification 00:06:36 Ten thousand dollars per core and a six-month agent run 00:07:40 Rebuilding programs from tests: ProgramBench and zero percent 00:12:15 Structure vs competence: can you learn a program from behavior? 00:15:27 Continual learning, abstraction, and Claude as an ecosystem 00:23:17 Autoformalization and the AlphaProof trick 00:29:31 No single true representation: specs, Petri nets and TLA+ 00:34:43 Thermodynamic computing: when noise is the computation 00:37:32 Bayesian uncertainty in the age of token streams 00:41:12 Hybrid compute: vibe-coding loops, binaries and Stockfish 00:44:44 Co-design, central-AI apps and API pricing 00:49:45 Chain of thoughtlessness and the Chomsky hierarchy 00:53:40 AI psychosis, slop and the broken social contract 00:57:34 Typing it yourself, teamwork and performance vs competence --- REFERENCES: person: [00:00:10] Thomas Ahle https://thomasahle.com organization: [00:00:27] Normal Computing https://normalcomputing.com/ paper: [00:11:21] ProgramBench: Can Language Models Rebuild Programs From Scratch? https://arxiv.org/abs/2605.03546 [00:31:55] Autoformalizing Memory Device Specifications with Agents https://arxiv.org/abs/2605.00058 [00:35:20] Thermo AI and the Fluctuation Frontier https://arxiv.org/abs/2302.06584 [00:36:40] Thermo Comp System for AI Applications https://arxiv.org/abs/2312.04836 [00:37:05] Thermodynamic Linear Algebra https://arxiv.org/abs/2308.05660 [00:44:50] An efficient probabilistic hardware architecture for diffusion-like models https://arxiv.org/abs/2510.23972 tool: other: [00:01:00] Building an Open-Source Verilog Simulator with AI: 580K Lines in 43 Days https://normalcomputing.com/blog/building-an-open-source-verilog-simulator-with-ai-580k-lines-in-43-days [00:02:55] Normal Computing Announces Tape-Out of the World's First Thermodynamic Computing Chip (CN101) https://www.normalcomputing.com/blog/normal-computing-announces-tape-out-of-worlds-first-thermodynamic-computing-chip [00:32:02] DRAMBench: Autoformalizing DRAM Specifications with Timed Petri Nets https://www.iese.fraunhofer.de/blog/drambench-autoformalizing-dram-specifications/ --- ReScript: https://app.rescript.info/share/ff9684a112ab37744096adaeb097a263

Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.

• 0:00Speaker 00

  Yeah, so why not try and build a chip that's just inherently random?

• 0:03Tim Scarfe?

  Meet Thomas Arli. I caught up with him in Zurich. And he's one of these rare galaxy brain people who's comfortable in probabilistic machine learning, formal verification, and chip design. However, there's a small problem. When the token god hands you something that looks like it works, how do you know it's actually right?

• 0:27Speaker 00

  So my background is in theoretical computer science. I used to do algorithms for high-dimensional data, locality-sensitive hashing. Then I moved to normal computing to develop thermocomputing, also to speed up Bayesian intelligence. Sometimes I think about it as the lovable for chip design. So we take it all the way from your intent through the design, through optimizing your design, to formalizing and verifying your design, all the way to tape out.

• 0:52Tim Scarfe?

  Now, I didn't fully appreciate this before. These days, a chip doesn't necessarily start in a factory. It can start as code. So engineers design the whole circuit in a language called Verilog, almost written like software. And only much later does any of it become physical silicon. But first, that code has to be simulated and formally verified. It has to be proven correct. Because once a chip is fabricated, if there are any bugs, you're in big trouble. So a few months ago, Thomas blogged about building a Verilog simulator using a swarm of AI agents collaborating with each other. And it generated over half a million lines of code in forty-three days.

• 1:38Tim Scarfe?

  Now, the reason he needed to do this is that commercial software costs a ridiculous amount of money and isn't very friendly to using agents. Ten thousand dollars per seat or something?

• 1:48Speaker 00

  Yeah, per for one CPU kernel.

• 1:50Tim Scarfe?

  If an AI can generate a chip design, or a proof, or a working program, how do you know it's actually correct?

• 1:58Speaker 00

  The percentage of tests that it got right, or like, even like the fable, it was like, oh, it got like seventy, eighty percent tests correct. And it's like, yeah, but I talked with the people who made the benchmark and like, yeah, but it didn't get any of them actually right, you know?

• 2:11Tim Scarfe?

  Now, in chip design, noise is the enemy. Manufacturers spend a fortune getting rid of it. But in thermodynamic computing, The opposite is kind of true. The noise is the computation. It comes straight out of probabilistic machine learning, which already runs on randomness and uncertainty. And thermodynamic computing tries to make the chip itself a stochastic differential equation. Let the chip's own noise settle into place, and then it can land on answers that would normally cost a fortune to compute.

• 2:47Speaker 00

  And then you infuse all of this noise, and it'll start to behave according to to these stochastic differential equations. It actually behaves sort of according to the inverse of that matrix.

• 3:01Tim Scarfe?

  They've already released their first version of this technology. It's a chip called CN101, all the way to silicon. It's still early days, and it's aimed at a fairly narrow band of probabilistic workloads. But the real test is what can the benchmarks say once they scale this up? And something of huge interest to us at MLST is, if we're going to let AI build everything, what kind of understanding do we actually keep in the overall process?

• 3:28Speaker 00

  It's not just that it's getting smarter, it's also that humans are getting dumber.

• 3:33Tim Scarfe?

  Now, I should disclose that Normal Computing very kindly offered to cover our production and travel costs for this show, but we kept full editorial control.

• 3:41Speaker 00

  These are tools for device manufacturing. So it's things like, I mean, it's compilers for RTO. It's like, where RTO is like the programming languages you use. So if you're building a new chip, you typically don't draw all the different gates and so on. You write it in programming language like Verilog, which has sort of constructs that are quite, it's like a super parallel programming language, which had a lot of constructs that map well to hardware. But then there are actually no good open source compilers for this system.

• 4:19Speaker 00

  So the whole hardware industry, it doesn't have the same open source feeling as like software where all the good stuff is free and there's like this big vibrant market of tools here. It's much more locked down to like big providers. But people then, yeah, they compile this to and they get like a netlist, they can start building their schematics, they can also look at it. You get like these giant things that you can eventually send to the fab. But yeah, so they also need to do simulations, for example, for testing, you can do like formal verification.

• 4:57Tim Scarfe?

  Let me just play that back so I understand it. So Verilog, it's a bit like a programming language for describing a circuit. And what we might probably before we go and get that fabricated is we want to do simulations because it's very expensive to get it fabricated. So yeah, we can design the circuit and do simulations.

• 5:17Speaker 00

  Yeah, exactly. It's super expensive too. It could cost you what they said, like there was this famous Intel division bug in the 90s that probably cost them between 500 million and $2 billion. And I mean, that's a lot of money in the 90s. There's, I think there are other examples later on that nearly bankrupted some of these companies, like TinyBox that managed to make it through to the fab. And it's, yeah, it's a really different world again from software where we just, you know, people fix stuff in prod, you just move fast and break things. It's definitely like, yeah, people are much more paranoid in the hardware industry, which

• 5:59Speaker 00

  is also why it's a cool place for formal verification, formal methods to thrive.

• 6:06Tim Scarfe?

  Okay, so you're saying at the moment there are these commercial, you know, verifiers and simulators and they cost a ridiculous amount of money. So is it something like $10,000 per seat or something?

• 6:16Speaker 00

  Yeah, for one CPU kernel. Right, yeah, like say you want to scale this up in a data center with a million agents running like you're gonna like, I mean, a computer is already expensive, but not that expensive. What, yeah, what is that, $10 billion or something, right? Just for those licenses. And I think actually that's one of the reasons also why. AI still is not as popular in the in the hardware space because they haven't been able to train like the the models are not as trained to this kind of workloads because they just it's not feasible like you don't have all of the open source code out there to start the training but you also don't have the tools that they need to learn to use you

• 6:59Speaker 00

  don't have the yeah all of the like the task like you can't just all of the reinforcement learning on top of it I mean I mean they clearly are doing some of that like we can also see from model generation to model generation that they are getting better but it's just it's kind of day and night between like Python or JavaScript we've been sort of developing these EDA tools in-house using using AI having you know I I think I probably have the world records of the longest running agents having like some twenty GPT agents running for around six months now are still making making a progress

• 7:38Tim Scarfe?

  So as I understand correctly so similarly to you know anthropic Carlini had this blog post out and you know they had a functional specification of a C compiler and they had about forty thousand agents and they reproduced the C compiler you did a similar thing for an EDA

• 7:52Speaker 00

  It didn't work by the way, right?

• 7:53Tim Scarfe?

  Well, I mean that's an interesting thing as well you know because this is what I want to get to right that it's tantalizing that there are there are some domains that are so well evolved that we have you know they might be very complex but but we have a functional specification and it's reasonably coherent so the idea is we get a shitload of agents and we reproduce the function of this software based on these tests and we do it recursively agentially and so on now my contention with this is I think that it's not about where you end up it's not about the functions and the tests passing it's about how you got there and how structured it is so there is this tendency with agentic coding to build

• 8:34Tim Scarfe?

  a spaghetti monster which seems to work but because if you think about it in this project you're talking about I think you said there's like five hundred or more five hundred thousand lines of code and in five years' time there's all of this code that probably you know you folks haven't read most of it You know, that that that sounds like a problem.

• 8:53Speaker 00

  Yeah, I think for a lot of this stuff, we're relying on the hope of some kind of escape velocity from code complexity, that the models are going to keep improving faster than our code gets messed up. I had those three days of, you know, Fable, Fable access, and it was really good. Like, it definitely cleaned up a few things that GPT-5.5 had had messed up.

• 9:16Tim Scarfe?

  But but but did it, though? Do you think it could be deceptive? Because you know, when Fable comes out, all of a sudden, 4.8 looks terrible. And when 4.8 came out, it looked amazing compared to, you know, 4.6. So there's something deceptive about it, but you know, it's like a parlor trick?

• 9:34Speaker 00

  Yeah, no, it's true. Like, in principle, you could all be be smoke and mirrors. I mean, but I think that's why it's good to have also the the hard tests, right? So I could also see that it was actually suddenly I was making more progress on the more objective tests than I hadn't seen for a while with the other models. So I guess that gives me some trust. But it is, yeah, it is weird to sort of not have the same in-depth level of understanding everything in your code and, you know, definitely miss it.

• 10:02Tim Scarfe?

  And I'm interested in what the consequences of that are, because you said you put this blog post out earlier in the year. And then when we had a chat on the phone, you you said that you you noticed there were some things that that were that were wrong. And it isn't there's this tendency, though, to accumulate understanding debt. And when that happens, you I think from an evolutionary point of view, you're stuck. Because I think deep grounded understanding of how things are are the basis for the next design decisions, the next evolution. So do you get into this kind of fishbowl thing where like now you're in no man's land and you don't really know what to do?

• 10:38Speaker 00

  Yeah, I do think it's important to understand as much as you can and have time for. I mean, I think for compilers, there is some very important architectural design decisions. And then there's a lot of sort of just implement like these like 100 different functions, like they all just.

• 11:01Speaker 00

  Especially like modern compilers, it's like layer by layer by layer. You have to lower these things from like the front end level to the middle interpretation to the backend layer. And and a lot of that, I definitely don't want to have to write like it's it's it also paralyzes as well. I think I mean, I'm sure it could be one of the reasons why Anthropic also picked it. We talked about this program bench thing. I think Facebook released where it's a benchmark where the task that I think they took hundred and fifty, hundred and seventy programs. Some of them are really complicated, like FFmpeg is one of them. The AI just has to re-implement them without internet access. Yeah, basically when it came out, they had like all of the L L M's got zero percent because none of

• 11:45Speaker 00

  them like were able to pass all of the tests. But I've seen like people like I very rarely see that when people post benchmarks for this thing. They always post this like, oh, the percentage of tests that it got right or like even like the fable was like, oh, yeah, it got like seventy, eighty percent tests correct. And it's like, yeah, but I talked with the people who made the benchmark and like, yeah, but it didn't get any of them actually right, you know, because it's if if the program only passes seventy percent of the tests, it's probably not right.

• 12:14Tim Scarfe?

  And in a way, this is the thread that we were talking about before. You know, like for the last sixty years, going back to behaviorism, there's been this kind of thread between a structure and competence and prediction, right? So essentially, this this program bench is making the argument that you can learn the physiognomy of a program from its external behavior. So you can learn the deep structure, the constraints and so on. And I suspect that that is not possible. Unless, of course, the L L M already knows about the source code because it's in its training data or whatever. But what do you think about that?

• 12:49Speaker 00

  Yeah, I think I think humans do it all the time. Actually, I think.

• 12:54Speaker 00

  There's the whole field of kind of reverse engineering where people,

• 13:01Speaker 00

  yeah, actually, I listened to something with the FFMPAC people where they were talking about all these codexes that they put in there and they, like a lot of time, they have no idea what they do. Like it's just like this obscure blob of code, like they probably don't even have access to the code. They just have a couple of like example, video examples that were encoded with this. And maybe some people had shared some screenshots like with clips from the movie. And then they had to go and try and read this like encoded blob and being like, what is it doing? Like, how could we like write a program that decodes this thing? And somehow people are able to do it, you know, we must have some sort of prior, right? Like what, what are the typical things people put in a video codex?

• 13:45Speaker 00

  Like, oh, there's probably some, you know, you know, Fourier transforms of some stuff where they're probably like, you chunk things up or, I don't know, I haven't done that much video encoding. But yeah, just like completely black box, just try and keep improving your program and visualize the output until the end, the movie comes out and you have an idea of, oh, this probably looks how the movie is supposed to look.

• 14:13Tim Scarfe?

  Yeah, well, that's an interesting thing as well. So we can hill climb in a partial knowledge regime, right? So we might have a verifier. And as you say, like a lot of science is a form of intelligence where you're using MATLAB and you do like a, you know, like a Laplacian or you do, you do an image plot, you take a distribution and it like, it takes shape one step at a time. So what you're doing is you're taking steps into the unknown and every single, it's like there's a generation discrimination asymmetry, right? So we can discriminate well, but you know, we can't generate yet. But we take these steps and then when we get there, we now kind of collapse that into a model. And then that's the artifact of the intelligence.

• 14:48Speaker 00

  Right, it's like a star search or something where you kind of um you like you prune your search tree as you go and like um what what seems most successful so far like.

• 14:57Tim Scarfe?

  Exactly, but to your point, every single step of the way, we're using the toolbox. So you know, there are some folks that are really good at riddles or intelligence tests, and a lot of it is skill, right, because they they have a toolbox of abstract tricks that they use. And but but then there's this question of, well, maybe that's all it is. Maybe there are these natural patterns, these abstractions that we can compose together and handle any kind of novelty in the intelligence setting. So therefore, maybe language models could do this autonomously. I I I think they possibly could, yeah.

• 15:27Speaker 00

  This is a good point, like, because um I I tried to get an answer, I think, from uh Noam Brown at some point on Twitter about this, because you see how the the better pre-trained model you start with, and then they start reinforcement learning on it, and it seems like it gets up to some, like, the reinforcement learning works better and better depending on how good the model was to begin with, in a sense.

• 15:51Tim Scarfe?

  Yeah, it's super interesting. I mean, I agree with you. I I think it's wrong to say that L L M's are not intelligent, right? Because there is some kind of a combinational closure, and that means from the primitives in an L L M, we can do hill climbing and we can build some computational structure to solve problems, but that's not quite it. And and it can happen at different levels of abstraction. So if the L L M's have higher abstractions, then they can, you know, traverse the common combinational closure of the higher abstractions and they can solve the problem. What seems to happen, though, is, I mean, there's no continual learning, so those don't get, you know, added to a library and reused later, but there's also no abstraction. So what humans would do is they would they would look at this computational graph and they would say, ah, I see that that's just um an analog of this thing over here, and

• 16:34Tim Scarfe?

  I and I'm now going to compress it into a new variable that screens off all of that complexity. Why do language models not do that?

• 16:40Speaker 00

  I think I think you're getting into like continual learning type thing, which is is obviously a big, a thing we lack. I think, I mean, I do think language models do that during pre-training. I do think like that's why, for example, Mythos is so good at at doing stuff in our code bases is because it has somehow seen a lot of code and it it just seems to have this sort of intuition for bugs and problems and so on, and that must be, you know, kind of like that, you know, it's it's seen the patterns before, it has some kind of abstraction. But but it's true, like, when you actually are doing sort of running them more live. They don't do it very well. Like, they don't. And I think a lot of people these days are thinking about this.

• 17:24Speaker 00

  How can we do better continual learning? So it can just build all of these abstractions and these things really well on the fly. I mean, I know some companies are actively against trying to do that also. Why? Like, I think Anthropic, right? I think Dario said, like, he considers it like a big safety issue too. Because you're gonna lose, you could easily lose all of the work that has gone into alignment. If the agent is learning too much on the fly, then it gets further and further away from the sort of safe checkpoint. But I think there are enough other people working on it that it'll probably happen. But it's bad. It's definitely like a big unknown, right? And I think it'll also have to change a lot of things in how we serve models, for example.

• 18:07Speaker 00

  Because suddenly you need to be able, like, if you, if we mean by continual learning that we actually update the weights live, it's gonna, it causes a lot of trouble, problems for the current paradigm. Because then suddenly you can't use the same weights for all customers too. I mean, I guess Thinking Machines has this thing where they have one shared model and then like some lauras on top. So maybe something like that can work. But it's still like you have to somehow, yeah, keep doing this all the time. And so we're also working in normal computing on like alternative forms of computation. Yeah. Like these thermodynamic chips or just sort of unconventional computing.

• 18:51Speaker 00

  It actually becomes sometimes hard to keep the memories in these analog resistors unless you keep learning at the same time as you're doing inference. Like, you have to use these fancy substrate like memory stores or something if they have to be permanent. But if you're just using like sort of basic capacitors, like you have in DRAM or something, they require constant refreshing. So either you just have to to spend a lot of energy on on that, or you just want to keep the the learning going forever. That way, they they kind of automatically refresh. And that's probably the more similar to also how brains work, right? Like, they don't, they never, they never like, just, I don't know what Chomsky or somebody would say about it,

• 19:33Speaker 00

  if they were just freezes. I think like the the synapses and stuff, they're always adapting.

• 19:38Tim Scarfe?

  Yes, exactly. I think out of all of the words we can use to analogize intelligence, adaptivity is the number one. And and in a sense, when we look at Claude, you can look at, you know, is Claude the model? Is it the ecosystem? I think it's the ecosystem, right? So it it is adaptive, because

• 19:53Speaker 00

  You say it's the personality or the persona or something?

• 19:56Tim Scarfe?

  Well, you know, there's a tendency to anthropomorphize it. But no, like, millions of people are using Claude code, because this is tangentially related to how we, you know, how we come up with causal abstractions in the world. So, you know, the way we do it is we are in the world, and we are agents, and we can make decisions, and we can like, you know, and reconcile uncertainty, and we can say, what would have happened if I did this? And I can share it with my friends. And and there's this wonderful percolation process where the abstraction has just become embedded. Now, that does happen with with Claude code, right? Because there are people using it on their machines, they're actually running tests, they're doing counterfactuals, and then all of this gets retrained in the in the next version of Claude, and then someone else will reuse that abstraction. So we we have the adaptivity as a system.

• 20:40Speaker 00

  Like this brain, shared brain, where all of the experiences go, what's called the bork or something, go back off and then, yeah.

• 20:49Tim Scarfe?

  Yeah, so but it's interesting to make, you know, to to discuss, is that effectively the same? Like, if we actually had some hypothetical, real time adaptive divergent Claude, you know, would it be much better than the Claude that we already have? And it's also related to the to the work that you guys do, because, you know, the process of intelligence, in in my view, is the creation of these coarse grannings, you know, skills. And that's kind of like what you guys are doing with ASIC. So you're you're building this customized hardware for making certain types of computation go really, really quickly. And it's almost like, that's the result of intelligence. So you say, I'm gonna take a very, very complicated thing, and I'm going to whittle it down and represent it in the best way I can. And then

• 21:31Tim Scarfe?

  I'm gonna bake it into a non adaptable hardware substrate. Is that fair?

• 21:36Speaker 00

  I think that is one, that is what we're working on right now, is this

• 21:42Speaker 00

  Is this idea of of trying to to build hardware that best fits uh like the models we have right now and just like really uh make um yeah a super a super efficient inference. You could say like the in the past, at least, the issue uh has been you stop yourself from innovating on the software side, but if you lock down your hardware too much, right? Like the Nvidia chips has been pretty good for innovation, like they're pretty flexible. Um of course, they also have have guided uh the way we do AI in a lot of ways, like towards matrix multiplications and so on, but but still people have been able to innovate. But on the other hand, I think also hardware is getting easier and easier to make with these kind of uh AI for uh E D A tools.

• 22:24Speaker 00

  So it's sort of shortening the like maybe now people are thinking about like making their CUDA kernels, right? It's um like it's not so unreasonable to think that soon we'll just be doing our AI for making like instead of CUDA kernels. We'll just like make some custom circuits for every single thing we want. So if you come up with a if you want your new algorithm to run really fast, you just design like a specialized circuit for that. Um and the AI helps you like optimize it and check that it's correct. And um of course, you still have the FAP, um but people are we're getting better at like batching things for the FAP. And but I mean, I I also think having the really flexible hardware is gonna be very interesting.

• 23:06Speaker 00

  Like the stuff where it's learning on chip and ideally like maybe the more adaptability that it has and the less we need to bake in. It's I mean, I don't know, it's just more cool, I think.

• 23:17Tim Scarfe?

  Yeah, but it isn't that a wonderful example of this recursive self improvement? Because as you say, like we're we're building the AI and then the AI is helping us build better kernels, better software, better hardware, which then in turn makes the AI better. And then, you know, you get this this kind of loop.

• 23:30Speaker 00

  I understand recursive self improvement in a way, right?

• 23:33Tim Scarfe?

  Exactly, exactly. But we should bring this to life. So there's this concept called autoformalization. And you guys on your website, you say basically that you have done something similar to alpha proof in respect of building chips. And roughly speaking, alpha proof is when, you know, they it was they won silver at the IMO in 2024. And what they did back then was they used a language model to generate a bunch of lean code. And then it obviously was a little bit messy. So some of the formalization was by hand and they did multiple renditions and so on. And then they would do verification with lean. And you're kind of doing something like that for chips.

• 24:11Speaker 00

  Yeah, yeah. So it's interesting because there is the autoformalization, which we define as taking human specifications and writing up and turning them into formal specifications in lean, for example. And then, but then, of course, you also need the proof step where you provide the, yeah, prove that your code, whatever you have, actually satisfies that specification. And I think some companies like Axiom, for example, they're very focused on this part, right? Like, and also, in some sense, alpha proof, that's also the main thing it did was it started with a formalization. And then the hard part was training the model to provide a proof or disprove.

• 24:54Speaker 00

  I think it's actually a really nice trick in alpha proof was that when they did the formalization of the proof, it didn't really matter if they got it right or wrong, because if they just asked the model to provide a proof or disprove. So if they if they got it wrong and it was no longer true, then it would just prove that it was not true. Or like, it would, that was like, you could still use it. Of course, like when they actually did the IMO challenges, they wanted the autoformalization to be correct. So then they did it by hand. But they didn't need it for the training, which I think helps scale it up. I think, yeah, so we can do a similar thing with hardware, by the way.

• 25:36Speaker 00

  It's pretty easy to just take some chip design and then, you know, you can basically just come up with some properties that may or may not be true. And then you can train the model to try and prove a disprove that this thing holds. So then, but that's all about creating the proof. But then the autoformalization, in some sense, it's harder because Um. Yeah, it's it's all like because it's harder to to create the the training data for it, right? Like, I think that's kind of also a story about AI in the last two years since reinforcement learning. Like, anything you can create good RL environment for, you can probably learn. But anything else is like out of reach right now. And so some of these chips have thousands of pages of specifications.

• 26:21Speaker 00

  And if you want to turn that, you yeah, you're turning that into a into a formal model. Um. It's not, it doesn't really like if you got just a couple of words wrong somewhere or a couple of numbers.

• 26:33Speaker 00

  Then it doesn't work like then what you prove is not uh is not important or is not relevant. And I think, I mean, it's always been an issue for in the chip industry like. That's the and they've kind of tried to solve it by having orthogonal teams. So they have one team that's designing the chip and one team that's designing the tests. And another team that's designing kind of tests of the tests. Like where they they they uh they they kind of like coverage. They call it functional coverage where they they measure what the tests test and then check everything off. And so, um, hopefully, like, um. If if all of the three teams have read something the same way and understood it the same way. It's they hopefully they have the right idea of it.

• 27:18Speaker 00

  I mean, you can try and do something similar with AI. You can argue whether it's really orthogonal if it's the same model that are doing each of the three jobs.

• 27:28Speaker 00

  I don't think it is. It is quite a thing like I do think there is enough entropy in these models when you do long runs.

• 27:36Speaker 00

  And you can definitely find a lot of bugs if by just doing things many times and see if if if there is agreement between them. But it's something it's all it but it's definitely like a trust exercise to you and a and a human exercise to figure out. How do we get the hardware engineers to trust and like how do we make it easy for them to verify that our formal model fits with what they? What they thought like. And you can come up with, yeah, that's all kind of different tricks you can come up with, both to make it more visual, like what your your understanding is and like whether it matches and like ask questions and see if you agree with the questions or show examples or you can also try and do some kind of back and I don't know, lots lots of tricks you can try,

• 28:19Speaker 00

  but it's it's an interesting problem. And I feel like no one like the Alpha proof and all of these other people, they never really solve this because their math statement for just one paragraph, they were not like thousands of pages long.

• 28:31Tim Scarfe?

  Oh, yes. Yeah, interesting. Yeah, because with Alpha proof, I think they wanted they wanted to use Lean four and there was hardly any stuff for Lean four. So they they created a converter from Lean three to Lean four and they needed lots of human, you know, people to fix it. And but but I guess my point is that they needed to fine tune a language model on a ridiculous amount of Lean code. And then they were using Lean as as an intermediate. Interestingly, like with their new model that they won the gold on IMO, they weren't doing any verification at all, not not not in a formal sense. But but then is there a spectrum? Because I don't, the way you were just describing it, it's not like it's not like it's a binary, right? So you were you were talking about test coverage and, you know, different perspectives, you know, the blind men and the elephant, you know, so there there are these functional tests and

• 29:15Tim Scarfe?

  these descriptions and we can do visual inspection and so on. So will it will it end up being a case where we're always wrestling with something we don't completely understand, but we're using as many signals as possible to get there?

• 29:27Speaker 00

  Yeah, I think I think where we're going now is also trying to encompass more of the of the spec creation, right? Like, obviously, when we start out, people already have written down all of these specs and we want to help them out with those. But when you do that, you also lack, you miss out on the whole intent that got into and the whole process of creating the spec. You don't know, you know, if there's just some numbers somewhere in there, you don't know why they chose those numbers and not some other numbers. Um. And I think you sort of by internalizing more of the process. At some point, you can at least be as safe as any as any human could have been about this chip, right? And and like, there might also just be some ambiguity that no one cares about.

• 30:12Tim Scarfe?

  The ambiguity thing is is interesting. There's a wonderful talk by Eric Kuriel called Math Does Not Represent. And, you know, he was talking about generalized relativity and he was talking about four four different, you know, completely orthogonal representations of that. And it was a similar thing, actually, with Alpha proof. So, you know, like, how many ways are there in lean to represent non-negative numbers? Apparently, there's quite a few. And so the Google guys were just just to stimulate the model. They were representing the problems in in different ways. And is is this, it it seems like this is almost an.

• 30:42Speaker 00

  Their training data in a way like, right, if they if they auto formalize the same problem in different ways, they actually get different problems.

• 30:48Tim Scarfe?

  Yeah, both both in in terms of the intelligence. So how can we kind of bootstrap the model to do better intelligence? But also in terms of the legibility and abstraction of the final output. So I I guess when people think of auto formalization, we we have this almost, you know, kind of idealist view that there is a one true representation and it's just going to be legible and and everything, but but it seems quite vague.

• 31:13Speaker 00

  Yeah, it's a one true representation. No, I I guess definitely definitely there's not one true representation. With with smaller chips, like, say you have like, just like floating point or crypto chip or something. I mean, the specification is actually pretty simple for those. Uh, it's more when you come up to like the big like system level stuff. I think software is in many ways ahead of hardware. I mean, in terms of formalization, they're behind. But in terms of thinking about these like architecture and architecture together with AI, right? I think a lot of people now, they'll run their architecture documents by the by Claude or somebody and being like, hey, what do you think of this? Should we move things around here or boom, boom, boom?

• 31:54Speaker 00

  And I think this whole discussion, like, it sort of helps the models understand like what your intents are and what you care about and what you don't care about.

• 32:02Tim Scarfe?

  And and just to give us an example to bring it to life, there was that DRAM article you you published. And the the article was talking about these timed Petri nets. And I did look this up on the internet. Apparently, it's a thing from the nineteen sixties for describing distributed systems. Explain that.

• 32:17Speaker 00

  What we talked about before with the formalizations is very.

• 32:22Speaker 00

  Um. It's like at the RTL level, at the very sort of cycle level where you you care about. Yeah, you want to prove that the exact thing happens at every single clock cycle.

• 32:33Speaker 00

  But of course, there is another kind of formal, and that's very important for things like adders or like arithmetic circuits or crypto. But a lot of the hard problems people have are more these, you can say, like kind of system problems, more like protocol level stuff like. Um. The things actually maybe also more popular in software has been like proving things like there's, oh, this system can never deadlock or live lock or. Sort of like protocol level properties.

• 33:01Speaker 00

  And like all of the sort of timing requirements between different things makes sense and there's no internal inconsistencies and. And there, so there currently there exists different. Formal languages for these things, like for the cycle level stuff, people use these system very like assertions, SVA type things. For the higher level protocol things, they're more classic things like the TLA plus, I think by. Valiant or no, or Laporte or something.

• 33:30Speaker 00

  And, yeah, so we we try and formalize things in both ways because they can have different. It's useful for different things. It's possible at some point they can all merge if you supply, it's kind of like you're doing very high level math and then you you can. You can reduce it all the way to the actions if you want to, but I think it's also interesting. Yeah, I mean, it's a very new field, so we're trying to explore different ways and these time picture nets is is one way to represent like these super parallel systems. That you have, for example, in these memories where all these different banks, they can like you can do activate like.

• 34:11Speaker 00

  Like, for example, if you activate one of these roles, you have to wait for the data to run down to the bottom before you can read it, for example. Then after a while you have to like refresh it because again, it's like these capacitor DRAM cells, they have to be refreshed all the time, but. You can also be working in a different memory bank, there might be like lots of them on this chip. At the same time, so there's certain like, but then there might be some circuitry that's shared between the banks and so. Certain things that are like interbank dependencies and intra-bank dependencies and also bank groups and people build really crazy stuff actually in there.

• 34:43Tim Scarfe?

  Very cool, very cool. I mean, what's really exciting to me is that it's possible to build chips that can do certain types of things orders of magnitude faster. And that's why I want to talk a little bit about thermodynamic computing, right? So, you know, so apparently, instead of forcing transistors to settle at zero or one, you let noise do a random walk and bias it. So the chip is a stochastic differential equation, right? I mean, that that that sounds crazy. Like, how does that work?

• 35:12Speaker 00

  Yeah, I mean, this was one of the things that really that got me to normal in the first place. Before that, before normal, I was at at Facebook, as we called them, in the like, the research group that does probabilistic computing, like we were doing like these spatial neural networks, where you assume like probability distributions over all your weights, and you're trying to infer like the posterior from like the prior data that you look at. But a lot of these techniques were kind of slow because you had to do, you had to like either try and do lots

• 35:52Speaker 00

  and lots of repetitions with with different random seeds, or you were trying to do it analytically. I mean, that kind of maybe takes a little bit of the point out of the probability. But then, you could also just, but then, but then it's funny, because you have these chips, and like, the chip manufacturers, they spend so much time like getting out every single little piece of noise out of their systems, and like having these extremely sharp margins for everything, like so much, you know, precision is probably like the most precise business in the world. And then what do we do with them? We just like add a lot randomness everywhere. And yeah, so why not try and build a chip that's just inherently random?

• 36:34Speaker 00

  Like, I mean, yeah, I think the brain probably has a bunch of randomness. But here, the first step we made was then this, you basically, you have this array of capacitors and you have certain resistances between them that you can program. And then you infuse all of this noise and it'll start to behave according to these stochastic differential equations. And then you think, okay, what can we do with that? It's sort of, it's a new computational paradigm that we've found very interesting to explore, where you can say, one of the things, for example, you could do with it is, it actually

• 37:13Speaker 00

  turns out that the matrix that you put onto the chip in the weights differential, or the stochastic differential equation, it actually behaves sort of according to the inverse of that matrix.

• 37:28Tim Scarfe?

  Yeah.

• 37:29Speaker 00

  And so then we could try and capture and average it out.

• 37:32Tim Scarfe?

  And when we spoke about this on the phone, you said something very interesting. Because, you know, we often talk a good game about this. I was talking with Michael Jordan the other day, and you know, like, yeah, we need uncertainty quantification, we need adaptive computation, and...

• 37:45Speaker 00

  Yeah, and I think this was kind of one of the issues we had, like, because I think Bayesian machine learning was really strong for a certain amount of time, like, at a certain point in time, before the generative AI, because you had like the one output and then it made sense to have this sort of distribution as the output. But now you have these sequences, yeah, as you're saying, like, you keep putting these tokens out, and I think no one really cares about what is the uncertainty about, like, one particular token and having a better distribution and that. You really want to know, after the model have thought about 10 different options, and you know it's backtracked and all this stuff, and it comes out with a final, final answer, what is, like, how much can I trust this answer?

• 38:31Speaker 00

  You either have to go like really deep on mechanistic interpretability to try and really carry all of the uncertainty all the way through that, or you have to try and use some more maybe anthropomorphic methods, I think, that are based on like how would humans estimate their uncertainty and you know, and try and apply that at really high level, but yeah, and you lose some of that beautiful math in there.

• 38:51Tim Scarfe?

  Because it's actually really cool that you've got a Bayesian background, because the way I introspect about this is, you know, like when you, when you have a thought and you have some intuitive notion of how confident you are, and it seems to be because you have a deep structure. So you can introspect and you can rationalize and you can say, okay, well, there's this component and this component and there are these constraints, I'm not quite sure about that bit. And that seems to be the missing link.

• 39:15Speaker 00

  Yeah. Yeah, we actually did some experiments back also when transformers first became popular, where we tried to do, it's before we knew exactly what the company was going to do, that it was going to be AI for hardware. So we wanted to do like predictions and we just started building base law into the model. So for, for some particular question, it would try and find like lots of pieces of evidence and then it would say, what is the probability that this, if, if the answer is yes, and if the answer is like different things, like what is the probability that I would see this evidence? And it would do that lots of times. And then at the end, you know, you could use base law to say, okay,

• 39:56Speaker 00

  then what is the probability that the original statement was true or false? It actually worked really well. Like we did this, I did some like internal like prediction game and it, and it, it beat everyone. I'd, we had two, multiple versions. One of the versions, we sort of, it was more neurosymbiotic, you could say, where you would just cal, like have the model come up with all of these probabilities and then you would manually calculate it. And then I also tried another version where it, I just told the model now use base law and do it or something. And somehow it actually did a little bit better. So I don't know how it, how it did that, or maybe it just was able to, yeah. Maybe it's because it

• 40:39Speaker 00

  was able to look back and think, actually, a couple of these values, I probably bullshit it and I should, I'll just ignore that. Or, but yeah, it's interesting. I, I know there are some people training, like there are some benchmarks now for, where people are trying to predict polymarket and this kind of stuff with. Um with L L M's and they have benchmarks for that, but I'm not quite sure if they use these sort of techniques, so it's all just end to end reinforcement learning and and they hope it just picks up a good methodology by itself.

• 41:12Tim Scarfe?

  But it's a wonderful example of this kind of um um adaptivity specialization loop. So you know, um for the first, and this is a common with vibe coding, so for the first month, um there was a false positive every single day. And you know, so I I just created a skill and then Claude would just retrain it and then eventually it just kind of converges. And then this is, this is the the bull case of vibe coding, right? But you know, like you just, every single day you fix it, fix it, fix it, fix it, and eventually you'll you'll come into the landing track and and it works really well. But in a way, this is similar to what you guys are doing, right? Because you you you have this kind of outer loop, which takes something complex and then you kind of um compress it and you optimize it and then you bake it into a kind of crystallized hardware.

• 41:53Speaker 00

  Yeah, I I was thinking about, there is this older tweet by Elon Musk, I don't know if people were laughing at him, I mean, I don't know, he he tweets a lot, but it was, he was saying like, um, why don't L L M's just write the binaries directly or the assembly?

• 42:09Tim Scarfe?

  Oh, yeah, I saw that, yeah.

• 42:11Speaker 00

  I I don't see why we wouldn't be able to do it, I just, it's a question of if we would want to do it or like, like, do we think? Because like, I think there's some fundamental computational problems always and in like everywhere in the world, we don't always like, recent years, we don't focus so much on them because we're so excited by AI and we wanna, um, we just interested in all the stuff that AI can do really well, but I mean, obviously, things like cryptography or like some of these like basic algorithms, like you never wanna want, gonna want the L L M to just do it, even if they can do very large number of multiplications, it's just super inefficient or like, um, you might as well optimize like a circuit or or piece of code

• 42:55Speaker 00

  for that and compilation has some of the same problems where you want to, um, and also end ship synthesis, where you're trying to, yeah, explore all these different designs and so on. So you don't necessarily want to um have the L L M do it because it's so slow versus some super optimized loop.

• 43:15Speaker 00

  Yeah, not to jump too much in things, but it's interesting to think about chess again. Like, of course, you have like the AlphaGo thing where it was like very, everything ran through a neural network, right? But, but today, the state of the art is in like Stockfish, of course, is that they took, they did more like hybrids, so they took the neural networks and they made these like, like a certain type of neural network that can update really fast when you change the state. And then they, they combine it with like just super fast search. And it actually outperforms the best like open source like AlphaGo type chess engines.

• 43:51Tim Scarfe?

  Oh, really? Using like adaptive fine tuning and structured inference?

• 43:58Speaker 00

  I don't know if you call it that. It's more like they took the classic chess search engine and they replaced the evaluation function with a neural net, but like kind of a very shallow wide neural net that they can, that, that is really, really fast to evaluate. And yeah, I think it could be that for something like synthesis and compilation, there's a similar thing where it's like,

• 44:24Speaker 00

  you could try and do it all with L L M's, but at some point that's the speed is a bottleneck and like you can throw, you, you get a benefit from having more knowledge and more intuition on all of this stuff. But at some point, there's also just a hard computation problem where you just want to brute force some stuff. And at that point, you want to be able to switch to like more classical algorithm.

• 44:44Tim Scarfe?

  Absolutely. Now, before we were talking about, you know, thermo computing. And so you, you, you folks have, have done some work that is incredibly like, has huge potential for things like, you know, Markov chain Monte Carlo, I think, and diffusion models. But you, you did say to me when we spoke last time that in some cases, it can be a false economy. Like, for example, you could have a diffusion model which might have like a different type of neural network on the end of it. And, and you might find that the benefit that you have doing the diffusion might be bottlenecked by another part of the model. So, so in, in, in practice, where can we see a huge uplift?

• 45:18Speaker 00

  I think it's, it's always interesting when you build hardware because you're, there's always this code sign problem with this, with the algorithms, right? The algorithms are, are so based around the, the GPUs and the hardware we have now. And so you can try and target some of those bottlenecks, like you can make hardware like we talked about with the with the thermal DRAM that's super efficient for for the memory. Like that might speed up inference, but it can only speed it up. Like, say we have there's some like 10% GPU utilization now for inference, like you could then you can hope to have like 10x there, but you don't know if you suddenly have access to that

• 45:59Speaker 00

  much like that different architecture, what like new algorithms could you build? Like, if you really went all in that. And that's some similar thing with the diffusion stuff, right? It's like now the architecture is not that eff- efficient in terms of like randomness, like the GPUs, it's kind of people don't really do want to sample like tons of Gaussian random variables everywhere. And and so they maybe also build architectures where they sort of try to remove that bottleneck by not focusing too much in these things. And then instead, so we can build new hardware that that makes that more efficient and that has some performance gain, but to really make the most of it, you then also have to

• 46:44Speaker 00

  come up with the new models that that sort of go all in on that. It's interesting, these Notion and apps. Have you thought about this? How all of the apps now, they want to be like your central AI, like Notion has this, they want to integrate with the other apps and your linear have an AI and they want to integrate with the other apps and like everyone is trying to like capture like being your central AI assistant. And then all the other apps will just be tool calls.

• 47:12Tim Scarfe?

  I know, I have to be careful because Notion are now sponsoring some ads, but no, they, I actually use it a lot because it's got an amazing agentic interface. It's got like a CLI interface. So I use it from, you know, from Claude. But what they want you to do is to pay them to use the agents that are built in at API prices. And I don't really see the reason in doing that when I've just got a Notion MCP, I've got a Notion CLI.

• 47:34Speaker 00

  API prices stuff is really killing innovation, I think, in that that space, right? I mean, I think. I mean, I think Codex, I think they are actually opening up more that you can use your accounts. I saw just yesterday, I think maybe also Anthropic opened up some that you could use some more like the SDK you can use with your accounts. But it's just like the price difference is so big that if you have to use API pricing, like nothing is competitive.

• 48:00Tim Scarfe?

  Well, I mean, you know, we don't have to go too deep into this, but I think creativity is all about respecting constraints. And I mean, you studied linguistics at Oxford and Chomsky always says that there's a difference between linguistic competence and linguistic performance. So, you know, he is using this bulldozer analogy for ages, you know, said that I love bulldozers too. They're great for clearing this snow, they're not a contribution to science. And he even said about Deep Blue that a computer winning at Deep Blue in the way it did is a little bit like a bulldozer winning the weightlifting competition at the Olympics.

• 48:34Speaker 00

  I think it was in a way like with Deep Blue, I mean, now maybe modern chess AI is a bit more, it's a bit different. I actually worked on chess engines for 15 years. But I actually, I remember him saying that too, and I was like a bit surprised because you'd think that if like, sure, like if your science is biology or you want to understand how humans do language. Sure, like then maybe the L L M's is kind of not so relevant how they learn language. But if your science is more the abstract of what is language, I thought you would be really interested in seeing like different systems developing language and you can comparing and see what's common, what's the same, what's different and so on. That would give you like a wider understanding of what is the concept of this thing.

• 49:19Speaker 00

  I mean, of course, it has to, you have to have some kind of respect for AI language to even like include it. If you just think it's like completely, you know, just some, I don't know, stochastic parrot thing. Maybe you're like, I don't really care about it. I want to include it in in my model of language. But if you do think it's actually doing language, then I think it doesn't really matter if it does it the same way as humans or not. Maybe it's more interesting if it's in a different way.

• 49:45Tim Scarfe?

  I know, I know. You, you mentioned chain of thought, by the way. How much can we read into chain of thought? Like, you know, like, some people just call it chain of thoughtlessness, like, you know, Sabaro Kamahati and... But actually, it is probably the modus operandi now for doing interpretability, right? For actually understanding what they're, what they're thinking. But, you know, you, you could argue that chain of thought is like the press secretary, not the orchestrator. So it's, it's almost a post hoc confabulation. And, but that does, that's not quite right, is it? Because that sounds a little bit like there's no causal link between the chain of thought and what the language model outputs. That's not true. So how much can we read into it?

• 50:22Speaker 00

  Yeah, it's like you want to give the model somewhere to think, right? Like, are you, when you do reinforcement learning, I mean, the chain of thought before the reinforcement learning and after reinforcement learning, I think is very different. Because before it was kind of, you try and prompt it and some tricks, they kind of work and kind of doesn't work. But once you do the reinforcement learning, you need, um, like, it's like a Turing machine, right? Like, it needs to have infinite memory and being able to have something to operate on. Whereas when you just had the transformer and just like single shot output, it's, it's like, I mean, probably in the Chomsky hierarchy, it would be a completely different type of system. Like, I don't know, an automata or something, right? There's like only finite amount of computation it can do, but now it can do as much computation as it wants.

• 51:06Speaker 00

  And it just has to learn to figure out how to do it. Like, you could imagine building a really simple LLM type system. And with access to chain of thought, it would be a universal Turing machine. So now at that point, it's just, no, because it can, it can have this tape and it can keep reading and putting... I think, I think that would be pretty easy to make a structure like that. But then the question is whether it can learn it. But at least now it has the, like, representation capacity, so it can do it. And clearly, something is improving and working.

• 51:36Tim Scarfe?

  This is actually the bigger problem like with the ecosystem, which is that software was always designed to be a thing that that reduces complexity and introduces canalization. So spreadsheets, they're a great example of this. And now, you know, accountants use spreadsheets and financial, you know, like everyone's using spreadsheets. And it creates an interface that everyone uses and it reduces complexity in the system. And this this agentic AI, it just creates spaghetti everywhere. And this is part of the reason why people aren't shipping, because, you know, it creates ephemeral, you know, complex, it's a little bit like bash scripting on steroids. So I've now created this web that only I understand, and it's becoming more and more specialized over time. So I can't share it with other people. And and the entire ecosystem is becoming very messy.

• 52:18Speaker 00

  Yeah, no, I definitely think a lot of things are

• 52:24Speaker 00

  upbreaking now because of that. I mean, a lot of the open source stuff is is like everyone just also like writes new code from scratch instead of trying to to get come together and hone these like shared libraries. But I mean, it is just for a lot of things more efficient than than also going through and you can get everything just the way you want it. But yeah, and and I actually think it's very interesting what you're talking about with the spreadsheets and like this channeling, right? Because there's a lot of kind of domain knowledge inside of these tools. And and that's actually also what I think like people might be worried about who build these tools, like how easy it like

• 53:05Speaker 00

  it is to kind of extract that knowledge and like people building clones and so on of their tools. Like if you have like everyone these days are like locking down all of the data, right? Because they're realizing data is becoming so valuable. They want to keep it themselves. So build something themselves rather than have other people use it. And and I think it could be a similar thing with with a lot of like specialized tools, because the tools basically are data like they're developed or so much time like founding all the right patents, everything is built in there. So how do you avoid other people from? Um. Going in and and and sort of, yeah. Agentially extracting, distilling it, kind of.

• 53:40Tim Scarfe?

  I'm sure this has happened to you. Random people on the internet will like say, I've just generated this paper. I've just generated this code. Have a look at it. And, you know, there's massive amounts of AI psychosis out there, which is that like you you do things that are slightly outside your domain of expertise and Claude will convince you that, you know, your stuff is not mediocre. It's great. And then you you share it with other people and other people immediately see through it. And this is a bit of a serious problem as well, in in in my opinion, because, you know, I I think there are experts out there who have really, really clear ideas about things. They've been doing software engineering and, you know, they've been in science and when they use Claude, it's brilliant if if they're diligent, right? Because they can actually use good abstractions and representations. But there's now a tsunami of pollution out there.

• 54:21Speaker 00

  Yeah, I don't, um, yeah, and it breaks this social contract, right? Like in the past, if if I wrote something and asked you to read it, you could at least have assumed that I would have spent ten times more times writing it than you reading it. But now now you're really skeptical about anything because like, why would I want to spend time reading some stuff that you didn't even read yourself, maybe?

• 54:44Speaker 00

  Yeah, like, I mean, but a lot of this is like social problems, right? Like, how do we protect also the open source ecosystem from AI-generated PRs where like no one has ever read them and then these like volunteer maintainers have to like read through all the slop. And, yeah, it's it's not really fun.

• 55:07Speaker 00

  Yeah. Do you have you talked with anyone about that? Like, people talking about like, we need like a GitHub, like a social credit system, like a commerce system, so so people can like downgrade you and like if if you don't have a high enough comma, maybe they'll just not read your PRs or.

• 55:23Tim Scarfe?

  We do need that. Yeah. Yeah. And Archive recently put gates on people uploading things there as well.

• 55:30Speaker 00

  Right, yeah. And they had this ban. It's like a one-year ban if if you have an hallucinated citation. But it's, yeah, it's sad in a way because it makes it harder, especially for for new people and like young people to to break in. Uh to that stuff like because then they they don't have any any karma or anything to show.

• 55:48Tim Scarfe?

  I I know, but I think the the the broad reason we have this problem is that this technology is the most deceptive thing ever created in human history, right? And it's a serious problem because it it's it's all about epistemic subjectivity, which is that you generate things that you don't understand and it convinces you that it's correct. And you can't see the glitches and obviously an expert can look at it and see the glitches straight away, but and it creates dependency. You know, when you start posting stuff that you that you don't, you know, you don't understand. Um. You want to be consistent, right? You you you've now made a statement that I know about this thing, so I'm going to keep doing it. And and then weirdly, um, people are very defensive about it as well, because if you criticize work that they've done with Claude, they they they take it personally. So it just creates this perpetuating cycle.

• 56:34Speaker 00

  Yeah, and create a feeling of understanding that you might not actually have, right? And um, it's like, I don't know, doing an exam or copying somebody else's work, like you might feel like you wrote it, but you don't like your brain didn't go through the motions. And yeah, I think it's dangerous also for like, if you're worried about um, sort of AI taking over, you know, because it's not like, it's not just that it's getting smarter, it's also that humans are getting dumber, like we no longer um, like no one like we get, we get lazy in terms of understanding stuff. We don't read the papers, you just put them in AI and be like, oh, explain this paper to me or something.

• 57:16Speaker 00

  But yeah, it's it's it's strange, right? Because on the other hand, I mean, it is, it can be like this big um level like speed, like it can speed you up so much. So it's like, it's it's hard to not use it. But like finding out when you should stop uh and when you should start using it again.

• 57:34Tim Scarfe?

  I I know, I mean, it's reminiscent of the Elon Musk tweet, you know, he said there there are no researchers at Tesla, that there's only engineers. And this for me is is the big problem, actually. It's it's a paradox. Because you can use language models to increase your knowledge. That's a fact, right? If the purpose is to increase your knowledge, then, you know, if you're a curious person, you can just dig and dig and dig and and you can learn a hell of a lot. So why is it the case that on average they erode our knowledge? And I think. I think it's Elon's fault, not his fault, but you know, he says that engineering is like, you know, this is a means to an end. So we are building this thing and it needs to pass these tests. And in a sense, I don't care if your knowledge erodes during the process because

• 58:17Tim Scarfe?

  that's not what I'm measuring you on. And, you know, we shouldn't be binary about it because clearly engineers, they trip up on things and they learn a lot along the way. But it seems to be quite convergent, you know, like when you're pursuing knowledge for its own purpose, you seem to, you seem to build deeper foundations and discover new things.

• 58:34Speaker 00

  Yeah, I guess that's like a tension with like in capitalism or something, you know, that, that, that the companies, they, they're not trying to necessarily develop their employees. I mean, maybe if they can see a profit motive in it, but at the end of the day, they just wanna get the job done. Yeah. And like, of course, if you spend a lot of energy developing your employees and then they leave and stuff, it's, it's always, it's always a bit tough there. I don't know if there's a way to, to force, to force it. But I think it's also a little bit self inflicted because, I mean, learning stuff is just hard and like, it can be like frustrating and, and it doesn't always get you in the same kind of flow as just prompting

• 59:19Speaker 00

  or something, right? And it's like, I think, yeah, I've been trying to use this. I think it was Kapathi who, who suggested this, like when he was learning some new stuff from LLMs, he didn't like copy paste it, he would have like side by side windows, but he would always like write all of the code by hand. I, I made a internal app to try and, because we hire a lot of, of AI engineers, like it's, it's hard to find people who are both like really good hardware engineers, really good AI engineers and also software engineers. Of course, you have to be that. Um. So we we have to scale up people, we have to scale up hardware people and AI, we have to scale up AI people and hardware. So I made like internal like um uh training tools and so on.

• 1:00:04Speaker 00

  Where I tried to have the same like uh blocks in there if you like trying block, copy and paste and the least like if people are warning and saying like uh you should maybe try and type it yourself like eh somehow it like you know you wouldn't think so like it doesn't feel like anything like if I'm just looking at it then typing myself like why would I learn it better but it's just empirical. That somehow like our neurons and stuff like it's important like to to go through the moments to the movements. Have to figure out what projects you you need to understand in depth and which ones you're just making like like where where it doesn't matter matter as much. I think we also we get tempted with the AI to just start way more projects.

• 1:00:48Speaker 00

  Uh in parallel, right? Because like, oh, I could just start another one and while it's working that I'll start another one, another one. And then suddenly you're like, well, there's obviously no way I could actually understand all of these in depth because now I started so many projects. Uh so then then you have to tempt like to stop yourself and being like maybe instead of starting the fifth project, I'll go back and try and understand what's actually going on and in the in the first couple of projects. Um I think maybe there'll be some evolution like we're still learning all the social stuff around using these tools and and what is effective and what's not effective hopefully will. And maybe we can even build some stuff into the tools. Is that what you're saying? Well, so with the scoping like to to try and make them uh better.

• 1:01:28Speaker 00

  And it's hard. I mean, another really hard social problem, I think, right now is how do you do um teamwork? Like, that's something I also think about as a manager, like if everyone on my team is like staring at their ten agents or something, working on some stuff. Um when are they gonna go and talk to their colleagues about this stuff or like if they don't understand the code themselves, how are they gonna explain to the other people in the company what the code does um and sort of and build together? And I don't think anyone has really solved it well at like at scale. I had some podcasts also with the Anthropic

• 1:02:05Speaker 00

  co-working team, and at least the way I remember it was that the podcast, they say, hey, how did you make this so good? And they were like, yeah, just everyone on the team coded their own version and then we picked the best one. And I was like, damn. If that's the best we can do in teamwork, you know, it's kind of, I mean, I, you know, it's, it's cool because it's like, it's like the ensemble method just applied to people and, and you know, it's, it's cool. You can explore so much more. But it's also like, it does remove all of the teamwork. At that point, it's just everyone working in isolation. You're just duplicating. Yeah. So I'm curious how we're gonna solve that.

• 1:02:42Tim Scarfe?

  And it's performance versus competence. And I guess we're kind of making a bet collectively that performance is all that matters. Thomas, it's been amazing having you on the show.

• 1:02:53Speaker 00

  Yeah, it's been so much fun. Thank you, Tim.