WEBVTT 00:00:00.000 --> 00:00:10.200 This is Essays on AI. Fair warning, the voice reading this one is synthetic, an AI narrating 00:00:10.200 --> 00:00:16.639 an essay by Tabrez Syed. Fitting, maybe, for a piece about how we check a machine's work. 00:00:16.639 --> 00:00:23.360 It's called Hard to Do, Easy to Check. Isaac Newton, Warden of the Royal Mint, had a problem. 00:00:23.360 --> 00:00:29.120 A silver shilling was supposed to be a promise. This much silver, guaranteed. But the promise 00:00:29.120 --> 00:00:35.360 had a weak spot. Silver at the edge of a coin is still silver, so people shaved a thin sliver 00:00:35.360 --> 00:00:40.880 off the rim, spent the coin at full value, and kept the shavings. Melt enough of them 00:00:40.880 --> 00:00:47.599 together and you had free money. By the 1690s, England's coins had been clipped so thin, 00:00:47.599 --> 00:00:52.799 the currency was in real trouble. The strange part is that this was never impossible to 00:00:52.799 --> 00:00:57.919 catch. You could always check a coin. You put it on a scale, weighed it against the 00:00:58.000 --> 00:01:04.879 standard, and a clipped coin came up light. The check existed. It was just too much bother to use. 00:01:05.440 --> 00:01:12.000 Nobody weighs their change in the middle of a market, or at a stall, or over a pint. So nobody 00:01:12.000 --> 00:01:18.959 checked, and because nobody checked, clipping paid. The fraud didn't survive because the coins 00:01:18.959 --> 00:01:25.360 couldn't be verified. It survived because verifying was expensive. And expensive checks 00:01:25.360 --> 00:01:31.199 don't get run. I've been thinking about that gap lately, because it sits right at the heart 00:01:31.199 --> 00:01:38.400 of how we're adopting AI. Last week, I set two agents running overnight. One took on a research 00:01:38.400 --> 00:01:45.279 project. The other built a feature in a piece of software I'm working on. By morning, both had 00:01:45.279 --> 00:01:51.040 handed me something that looked finished. And I sat there with the same question about each one. 00:01:51.680 --> 00:01:57.120 How do I know it's any good? I could go through all of it line by line, but that would take about 00:01:57.120 --> 00:02:03.599 as long as doing the work myself. And if checking the work costs as much as doing it, the agent 00:02:03.599 --> 00:02:10.160 hasn't really saved me anything. It's just handed me a big pile of output to inspect. So what you 00:02:10.160 --> 00:02:16.479 actually want from any worker, human or machine, isn't only that they're fast. It's that you can 00:02:16.479 --> 00:02:21.520 check their work cheaply. Some way to look at the finished thing and know it holds up, 00:02:22.080 --> 00:02:28.720 without retracing every step that got them there. The best kind of work has this built in. Hard to 00:02:28.720 --> 00:02:35.759 do. Easy to check. A finished jigsaw puzzle takes all afternoon to put together. But you can see 00:02:35.759 --> 00:02:42.800 it's done from across the room. The doing and the checking come apart. Most work isn't like that. 00:02:42.800 --> 00:02:49.440 And that's the trap. When the check is expensive, having a faster worker doesn't help much. Because 00:02:49.440 --> 00:02:54.320 now you're the bottleneck, standing over a growing pile you can't afford to look through. 00:02:55.119 --> 00:03:01.440 That's where a lot of AI use is right now. Agents everywhere, producing code and writing and 00:03:01.440 --> 00:03:08.160 analysis faster than any human could, and almost no cheap way to tell which of it is right. We got 00:03:08.160 --> 00:03:14.399 the fast worker. We didn't get the fast check. Newton's fix was to change the coin. Not the metal, 00:03:14.399 --> 00:03:20.800 not the law. The edge. The Mint started milling coins with a ring of fine ridges around the rim, 00:03:20.800 --> 00:03:26.880 and stamping a few with a raised inscription running all the way around. British pound coins 00:03:26.880 --> 00:03:34.080 carried the idea for centuries, spelled out in Latin along the edge. Decus et tutamen, an ornament 00:03:34.080 --> 00:03:41.039 and a safeguard. Here's why it worked. The ridges are hard to add. You need a real Mint, 00:03:41.039 --> 00:03:47.360 industrial pressure. Tooling a backroom clipper can't fake. But once they're there, checking them 00:03:47.360 --> 00:03:54.479 costs nothing. Clip the rim off a milled coin, and the ridges are gone. The edge goes smooth, 00:03:54.479 --> 00:04:00.240 where it should be grooved, and you can feel it with a thumb without even looking. The check went 00:04:00.240 --> 00:04:06.479 from weighing every coin to running a finger along the edge. From a chore nobody bothered with, 00:04:06.479 --> 00:04:12.240 to something you barely notice doing. That's the whole idea. A bit of work added up front, 00:04:12.240 --> 00:04:18.160 built into the thing itself, that tells you when something's wrong. Engineers have a name for this. 00:04:18.720 --> 00:04:24.880 A checksum. A small, cheap tag that travels with the thing and gives it away if it's been 00:04:24.880 --> 00:04:31.600 tampered with. Newton put one into a coin 300 years before computers gave it a name. 00:04:32.239 --> 00:04:39.679 And notice what it does. The ridge doesn't make the coin honest. It just makes a dishonest coin 00:04:39.679 --> 00:04:47.040 easy to spot. So you stop having to trust it and start being able to check it. A coin is the small 00:04:47.040 --> 00:04:57.600 version. One object, one thumb, one check. But the same trick scales. Take accounting. In 1494, 00:04:57.600 --> 00:05:04.720 a Franciscan friar named Luca Pacioli wrote down a method Venetian merchants were already using, 00:05:04.720 --> 00:05:11.920 and we've barely improved on it since. Double-entry bookkeeping. Every transaction gets written down 00:05:11.920 --> 00:05:18.640 twice. Once as a debit, and once as a matching credit. And at the end of the day, the two columns 00:05:18.640 --> 00:05:24.799 have to come out equal. If they don't, you made a mistake somewhere, and the books tell you before 00:05:24.799 --> 00:05:32.000 anyone else finds out. The merchant doesn't have to remember every deal. The structure remembers, 00:05:32.000 --> 00:05:37.359 and it complains when the numbers don't line up. Scale it up again, and you get something like a 00:05:37.359 --> 00:05:44.720 tax return. A return isn't one number. It's a stack of forms that feed into each other. A figure 00:05:44.720 --> 00:05:51.359 on one form has to match the figure it came from on another. Columns have to add up the same way, 00:05:51.359 --> 00:05:58.799 down and across. Accountants call it tying out. Two numbers worked out separately have to agree. 00:05:59.760 --> 00:06:05.839 Nobody holds a whole tax return in their head, and they don't need to. The checks are built into the 00:06:05.839 --> 00:06:11.519 shape of the paperwork, so a mistake has nowhere to hide. There's a catch, though, and it's worth 00:06:11.519 --> 00:06:18.000 noticing now, because it comes back later. These checks catch the wrong form, not the wrong idea. 00:06:18.640 --> 00:06:24.640 Balance your books perfectly, but put a payment in the wrong account, and everything still adds up. 00:06:25.200 --> 00:06:31.440 The columns agree. The mistake sails right through. The check tells you the arithmetic is consistent. 00:06:32.079 --> 00:06:38.320 It has no opinion about whether you did the right thing. Push this idea as far as it goes, and you 00:06:38.320 --> 00:06:43.679 end up in mathematics, where the thing being checked isn't a coin or a ledger, but a proof. 00:06:44.320 --> 00:06:50.559 A careful argument that something is definitely true. For most of history, a proof was checked 00:06:50.559 --> 00:06:57.839 the way a contract is. An expert sat down, read it line by line, and vouched for it. That worked, 00:06:57.839 --> 00:07:03.440 until the proofs got too big to read. When Thomas Hales proved the Kepler conjecture in the late 00:07:03.440 --> 00:07:09.920 1990s about the most efficient way to stack spheres, the reviewers spent years on it and 00:07:09.920 --> 00:07:17.519 finally gave up, saying they were 99% certain it was right. Mathematicians don't usually settle 00:07:17.519 --> 00:07:25.440 for 99%. Being sure is the whole point of the field. So Hales, and a lot of people after him, 00:07:25.440 --> 00:07:30.399 went looking for a check that didn't depend on a tired human reading carefully. 00:07:31.200 --> 00:07:36.480 They found it in software called a proof assistant, and the one that broke through 00:07:36.480 --> 00:07:45.040 is called Lean. The idea is close to Newton's. At the center of Lean is a tiny, paranoid program, 00:07:45.040 --> 00:07:51.359 small enough that you can trust it completely, and its only job is to confirm that each step 00:07:51.359 --> 00:07:56.959 of a proof really does follow from the step before. You do the hard work of writing the 00:07:56.959 --> 00:08:03.920 argument in a form the program can read. In return, you get a yes or a no. Here's what 00:08:03.920 --> 00:08:10.559 that looks like up close. Say you want to record the simple fact that a plus b is always the same 00:08:10.559 --> 00:08:17.519 as b plus a. In Lean, you'd write a line that reads, in plain English, for any two whole numbers 00:08:17.519 --> 00:08:25.040 a and b. a plus b equals b plus a. Then you have to supply the steps that prove it, and the program 00:08:25.040 --> 00:08:30.480 checks every one. It won't take your word for it. And it won't accept, looks right to me. 00:08:31.279 --> 00:08:37.359 Math gets a compiler. The payoff is real. Terence Tao, who is about as good a checker as mathematics 00:08:37.359 --> 00:08:43.520 has, was formalizing one of his own published papers in Lean, a result that had already been 00:08:43.520 --> 00:08:49.760 reviewed and printed. Partway through, the process turned up a bug, an expression that 00:08:49.760 --> 00:08:56.559 quietly broke in one small case. Nothing fatal, and he patched it. But it was the kind of gap 00:08:56.559 --> 00:09:03.200 the best reader in the field had read straight past, because on paper, it looked fine. Lean has 00:09:03.200 --> 00:09:09.599 a limit, though. Writing a proof in a form the machine can read is a huge amount of work, often 00:09:09.599 --> 00:09:16.159 10 or 20 times the effort of just proving it the normal way. That's why most of math still isn't 00:09:16.159 --> 00:09:22.559 done this way. And there's a deeper problem underneath. Lean checks that your proof follows 00:09:22.559 --> 00:09:29.200 from your definitions. It doesn't check that your definitions are the ones you meant. State the wrong 00:09:29.200 --> 00:09:35.039 theorem, and Lean will cheerfully confirm a perfect proof of the wrong thing. It's the same as the 00:09:35.039 --> 00:09:40.239 balanced books with the payment in the wrong account. The check tells you the answer is valid. 00:09:40.880 --> 00:09:46.000 It can't tell you the answer is right, and it definitely can't tell you the answer was worth 00:09:46.000 --> 00:09:52.239 having. That's true of every check in this story, from the coin to Lean. It looks at the form, 00:09:52.239 --> 00:09:58.000 not the meaning. It can catch a mistake, but it can't tell you that you asked the wrong question, 00:09:58.000 --> 00:10:02.960 or that nobody needed the answer. Somebody still has to decide what's worth doing, 00:10:03.520 --> 00:10:07.119 and there's no ridge you can run a thumb along to know you chose right. 00:10:08.000 --> 00:10:13.520 Which brings me back to that morning, and the two agents. The one that wrote code, 00:10:13.520 --> 00:10:18.960 I can check. There's a compiler that makes sure it runs it all. There's a test suite that checks 00:10:18.960 --> 00:10:25.840 the parts I care about. I can set up a small mock and watch it behave. None of that is free, 00:10:25.840 --> 00:10:30.960 but it's cheap enough that I can look at a night of work and know where I stand in a few minutes. 00:10:31.760 --> 00:10:38.479 The ridge is already built. The research is the hard one. The agent came back with an answer, 00:10:38.479 --> 00:10:43.599 and the answer sounds reasonable. And that's exactly the problem. How do I know it didn't 00:10:43.599 --> 00:10:48.400 miss the one document that would have changed the conclusion? How do I know it isn't just 00:10:48.400 --> 00:10:55.119 confidently wrong? There's no compiler for a five-page argument. To really check it, 00:10:55.119 --> 00:11:00.000 I'd have to go do the research myself, which is the thing I was trying to hand off. 00:11:00.080 --> 00:11:05.760 So that's roughly where AI stands. It ran ahead in the places where we'd already built the check. 00:11:05.760 --> 00:11:13.039 Code, math, anything a machine can test. It's slow everywhere the only check is a person reading 00:11:13.039 --> 00:11:20.159 carefully. The question I keep coming back to isn't how smart the models get. It's how much 00:11:20.159 --> 00:11:26.400 of the world we can actually make checkable, and what's left when we've built every check we can, 00:11:27.119 --> 00:11:29.919 still holding the one thing no check will catch. 00:11:30.719 --> 00:11:33.440 Whether we asked for the right thing in the first place. 00:11:34.080 --> 00:11:38.719 That's the essay. You can find the written version, with links to every source, 00:11:38.719 --> 00:11:44.400 at mandalivia.com. And if you'd like future essays read to you as they're published, 00:11:44.400 --> 00:11:50.400 subscribe wherever you listen. Essays on AI is a Mandalivia production.