Automated Reasoning to Prevent LLM Hallucination with Byron Cook - #712

0:00There's this difficulty where the people who are the experts in the area haven't quite crystallized their view of what should be true and should be true. And so we basically go around and around and around, and that loop has been really the expensive part. That's actually why formal reasoning has been unapproachable to all but the largest of enterprises with the most important problems. Okay, so great. How do we make that approachable for a much larger addressable market? That's what automated reasoning checks is trying to help customers do.

0:42All right, everyone. Welcome to another episode of the TwiML AI podcast. I am your host, Sam Charrington. And today I'm here at AWS reInvent with Byron Cook. Byron is vice president and distinguished scientist of the Automated Reasoning Group at AWS. Before we get going, be sure to take a moment to hit that subscribe button wherever you're listening to today's show. Byron, welcome to the podcast. Thanks very much. I'm really looking forward to digging into our conversation. We'll be talking about automated reasoning, the foundational technology behind a really interesting new tool announced at the conference yesterday that uses automated reasoning, the technology, to help LLM users safeguard against hallucinations.

1:24To get us started, though, I'd love to have you share a little bit about your background. I'm a scientist. I've worked in for 25 or 30 years in the space of programming languages, type systems, formal reasoning, logic, these kinds of things. And I've been an academic and worked in research labs and worked in startups and worked in Amazon. I've been to Amazon for 10 years. Oh, wow. Nice. So you've been to a few reinvents. Yeah. Awesome. You know, I wanted to start out really introducing the idea of automated reasoning. And it occurred to me that there's maybe a bit of a name collision around reasoning.

2:08A lot of people listening to this episode might hear that and think, oh, LLM reasoning. That's a popular topic nowadays. But automated reasoning is a distinct field that's been around for a while. Can you talk a little bit about the field broadly in that context? Yeah, sure. I mean, I think that things are kind of shifting around. So when we kind of look back on this time in a couple of years, probably we'll be using different names and actually the ideas will blur. But traditionally, if you look at artificial intelligence, that name was coined in the 1950s. There was this Dartmouth workshop where there were people from cognitive sciences, mathematical logic.

2:48Claude Shannon was there and so on. And there was a lot of excitement about the digital computer had come out and it was now available to folks. And I was like, well, what can we do with this? And how do we sort of make intelligence? And a number of different branches sort of formed out of that. So you have symbolic reasoning, cognitive reasoning, and you have Bayes theorem and these kinds of things. And then kind of what happened was there was a series of like, there was AI winter, right? There was various, the pendulum swings on funding. People were excited about it. People think it won't ever be able to do anything.

3:31People get really excited about it. And so what happened is these different branches began to like lower their ambitions and find niche problems that they could solve. And so you would have traditionally called it symbolic logic or symbolic AI or good old-fashioned AI or these kinds of things. That's a form of reasoning, logical reasoning, and you can write algorithms to automate your reasoning. And so that's one branch. And it has a lot of commercial impact in proving the correctness of programs. And we can talk about in a moment kind of how we're using that and have been using Amazon for 10 years.

4:13Meanwhile, the other branches went off to, you know, like, make predictions or, you know, identify images and things and images and so on. And then what's really happened is with the rise of interest in generative AIs, it's really brought the communities actually back together. So you have this idea of neurosymbolic AI, which is basically blurring back kind of what the original folks had in mind. where you combine the cognitive ideas and symbolic ideas together. In some sense, the thing that was announced yesterday is a neurosymbolic AI approach. Maybe I've answered your question, but I'll maybe stop there and see how to go.

5:01take it from there? Yeah, yeah. So when I think about automated reasoning, I think about it in the context of approaches like formal methods and things like that. Maybe just give us a broad brush grounding in automated reasoning. So very broadly, like reasoning, right? Like is the art, when you're talking about something intractably large or infinite, say like all possible triangles, triangles, right? That's going to be an uncountable set. So you're not going to be able to enumerate all possible triangles to answer a question about all possible triangles. For example, the Pythagorean theorem. It's a Pythagorean theorem.

5:41If you have a right-angled triangle, there's a certain thing that holds over all of the right-angled triangles, and that's infinite, so you're not going to be able to try them all out. So what you're going to want to do is you're going to want to make a finite argument, an argument in finite space, like a whiteboard or a paper, and time. Like this interview is an hour, so that would give us, if we wanted to talk about that and end it up, we would only have an hour. We're talking about triangles. So what you're going to do is you're going to want to try and use a well-accepted set of rules. And think like chess, right?

6:16Chess has only, there's only so many moves possible. and so you're trying to show what's true by finding a series of moves in that game that allows you to go from things that everyone believes are true from the start those would be the axioms to the deduction and so reasoning is finding those moves in that rule system to get to an answer and then automated reasoning is merely just the algorithmic the writing of software to find those proof. So that's sort of traditionally. So what's pretty amazing is actually there's been a series of really remarkable breakthroughs over the past 15 years in that space.

7:02So some really incredible ideas that allow you to solve absolutely enormous problems in those spaces and to find satisfying assignments in those very complex spaces or to show that there is no set of sign assignment to those rule systems. And so that's really given rise to a bunch of applications, but they've been largely hidden from customers. In Amazon, we have exposed a number of capabilities to customers, but we didn't really show how those things were working. And so the observation that was made when people began getting really excited about generative AI, and particularly for me because I'm in New York City, so I started talking to customers about these topics, was the realization actually that there's a lot we could do in the space of helping customers identify incorrect statements in the space of generative AI.

8:01Well, let's talk a little bit about some of the traditional applications of automated reasoning at AWS just to make the conversation more concrete. I know security is a big area. Yeah, so I mean, when I first joined, Amazon actually reported to Steve Schmidt, who's a CISO of now all of Amazon at the time, AWS. And the idea was, so the AWS organization and now Amazon has a very unique way of seeing security. Their goal, the phrase is, we don't say no, we say here's how. So they're really looking and investing a lot in ways of not shutting teams down when they're trying to do something innovative, but to work with them to identify ways to deal with the potential threats in the security space when they're trying to build a product.

8:54And so the decision there was to invest in informal verification. So we very early on began to identify stuff we could do and worked on five or six things at the start. And all of them have gone extremely well. So that is reasoning about AWS policies. So it turns out when you're writing systems in AWS that you are identifying configurations of resources and on the internet, which sorts of principles can touch those resources and take what kinds of actions, and those are expressed as resource policies. And they're very flexible, and so with flexibility comes, you can write down policies that might not be great.

9:41So helping customers understand those policies was one of the first applications of automated reasoning, and that shows up nowadays in S3 block public access, IMXS Analyzer, AWS Config Rules. There's a bunch of places that that, there's an internal thing called Zopkova which reasons about policies and that's, I've been pretty successful. So then we also did similar work for networking. So reasoning about your networks and what was possible in the network and what was reachable in the network. Reasoning about the correctness of the cryptography, both post quantum and traditional cryptography. Reasoning about virtualization.

10:16This is in the design of cryptographic systems or at runtime in some way? So the code that implements the cryptography, but also the cryptographic protocols that one uses to establish security across a distributed network. Okay. So we have a number of research papers and tools and so on. And this is over the past 10 years, so I'm describing quite a bit of work. Storage systems, virtualization systems, you name it. Okay. And so when we talk about policies, the way to think about that is a rule set? Yeah. I mean, so, right. So I remember once I was at a major bank in New York and the customer pointed out the window and he said, you realize that the vast majority of these windows have people in them writing AWS policies.

11:10because a lot of the people had moved to the cloud. And the realization was that one of the hard parts of writing a distributed system is deciding which other machines and principles across the network are allowed to access the resources and under what conditions. And so that's the policy language. And it's, I mean, this is technically not quite true, but morally true. It's isomorphic to first-order logic, right? The AWS policy language has disjunction, conjunction, negation, all of the concepts. It has quantifiers. So all of the concepts you have in mathematical logic are in the AWS policy language.

11:59So basically, AWS customers are writing first-order logic. code to validate access rules, for example. To decide, yeah. And so that was a perfect application. Yeah, yeah. Absolutely. Interesting. You mentioned that over the past N years, there have been 10 breakthroughs, or 10 years there have been N breakthroughs. What have been those big breakthroughs that have made automated reasoning more practical? So I'll begin answering, but I'm sure I'll forget some of them, so you can keep pulling on it if you want. but sort of in no particular order. So one of the, so the problems in automated reasoning are typically MP complete, or if not undecidable, right?

12:46And MP complete or worse. And so what that means practically is that the search space has so much branching. And so that ultimately the problem is, can you find a satisfying assignment? Can you find in this incredibly large tree a node where a certain constraint is met? Or can you show that no such one exists? That's what the reasoning challenge is. And how the tools work is they will begin exploring that space somewhat randomly and then learning lessons that have the effect of pruning away the search space. so they like the analogy I have is like you know like I remember I walked you know when I was really young I walked to school and I tripped and fell and it was because I hadn't tied my shoelaces and and so from that point on I checked to make sure that my you know shoes were were appropriately tied but what I didn't do is I didn't try all other routes to school right so what I did was I learned I root caused what the problem was okay and and so that problem of figuring out why you fell has massive branching factors, but you can kind of do a bit of root causing, figure it out, and then apply that heuristic, and then that prunes away the search space.

14:10And so that's kind of how they work. So they're enumerating, they're identifying root causes. And then one of the kind of really amazing tricks was to the database that maintains those lessons to build it in such a way that it aligns well with caches. So it turns out there was all these, this paper came, it was like in 1999 or so. So there was a bunch of professors and postdocs and so on that had these beautiful algorithms. And then these two undergraduates at Princeton made a tool that in theory was actually worse because the number of operations that were going to be performed was actually higher, but the performance of the tool was just outrageous because now the caches were...

14:59And so suddenly a lot of people began moving to those tools and then began to building on it. So that's one of the examples. Another example is this idea of restarts. So when you're doing the search, you what what the tools do is they often will stop the search and just restart from the beginning but keep the lessons learned so it's something like think about like maze solving like you can go to the end you realize you're at a dead end if you start from the beginning you want to capture you know something about exactly maze or start from a place where you could have branched differently exactly yeah yeah so so that's another trick and then what's happened recently it's something I'm very excited about is how to distribute solving.

15:42So basically the funding model for these tools has always been something like the National Science Foundation funding academics. You'd have a professor of three PhD students and a postdoc or something like that. So it was all like work done on a sequential microprocessor. And so there's an international competition of these tools. So like for example, this is something called the International SAT competitions we've been running for 20 something years and the tools are raced against each other but only quite recently have the rules allowed distributed or parallel research and so so now that there's this amazing sort of breakout of like because you could imagine if you're allowing a thousand machines to all independently search search spaces on the same problem and share the lemmas or share the lessons learned share the root causes across a network that that could that that could really be quite explosive.

16:37And so that has turned out to be true. And so, yes, we're really excited about those results. A couple of questions maybe relating this to machine learning. One is, have there been any attempts to kind of relate the foundational math that's required to solve these problems to things that lend themselves to GPU acceleration? Yeah, there's papers. I don't think there's been enough work to really be, to authoritatively say whether or not that in in there's a bunch of algorithms that are essentially matrix operations in there so i would think that we could but and then i'm there's i can point to some papers but like we'll sort of see where stuff lands the um the the there was a a blog post two or three years ago that showed that the fastest solver was actually on an iphone because the speed of the memory on the iPhone was the best.

17:37So by basically jailbreaking an iPhone and putting a solver on that, that was actually the fastest solver. So there's going to be something to do with what operations do you need to make things fast and what do you need for planning, basically. And so we'll see where things net out in the coming years. Okay. The other question was, you know, talking about exploring a search space and, you know, storing, you know, learnings brought to mind reinforcement learning. Has that approach been attempted? Yeah. So the alpha proof work, for example, is using reinforcement learning with the Lean theorem prover.

18:22and the Lean Theraimprover actually is developed by people on Amazon. So you're basically combining those two approaches together. So yeah, there's a lot of really interesting work happening now in the combinations of those tools. Interesting. So if you kind of, you know, if you, depending on sort of like people are like framing how they're talking about these things depending on who they think their audience is. So when you see stuff that's sort of more to a general purpose audience, people are talking about combining models, but a bunch of those models are actually automated reasoning-powered pieces.

18:58So I think kind of where we'll end up in the future is different algorithms, transformer-based things, constraint-based tools, and a lot of them being combined in different ways just tailored to solve different kinds of problems. Okay, awesome. Awesome. Let's talk a little bit about the automated reasoning and bedrock guardrails as a way to make the conversation very tangible. Yeah. And we can dig back into some of what makes it interesting from a scientific and technical perspective. Yeah. Tell us a bit about the product and what it's trying to help folks achieve. Yeah. Well, I'll say, first of all, kind of what it is, and then I'll say how we got there.

19:46Yeah. Okay. It's essentially two capabilities. The first capability is an experience involving a subject matter expert in a particular domain, say like zoning or like electrical codes, where they can define in mathematical logic the set of true and untrue statements in that domain. in a way that they don't need to understand mathematical logic.

20:21So then that formalization, the second capability is the ability to take that formalization and essentially sidecar it next to any other algorithm or human that's generating statements and then the ability to prove or disprove those statements according to the formalization. So that's what it is. Can I take a crack at restating that? Yeah, sure. So the way I understand the product is like you've got some document that defines some policy. I think in your blog post, you talk about like airline ticket refunds, but zoning laws or HR rules. There's a lot of rules that are in documents. Yes. And the way someone might approach building like a chat bot now is rag.

21:15And so you take this document, you break it up into a bunch of chunks. You use some kind of retrieval algorithm to get relevant chunks relating to a query. And then you tell an LLM to answer a question based on those chunks. And, you know, that works well, but there's no like guarantees about correctness. LMs make things up. We can try to enforce that they stick to the content they're given. But, you know, there's still no guarantees there. And my impression of this capability is that by applying these rules, we've got essentially another tool for kind of enforcing correctness. That's right. Yeah.

21:57Yeah. Yeah. So in those particular domains, we can reason about why a statement is true and provide an argument that can be audited independently of why that's true. In some sense, it's the rise of expert systems again. And it's really an interesting case where often old ideas are great. They're just kind of ahead of their time. And you need some other technology to come in and catalyst that possibility. And so I think that, I mean, we're very excited about generative AI because it allows us to build capabilities to help people build formalizations in logic. So when I saw, you know, over the past, I don't know, six or seven years when I sort of became aware of, I can't remember exactly when the Transformer paper came out.

22:47But when I began to see those models getting bigger and bigger, I was like, oh, great. We can use that to help people use their improvers, right? Which is not probably what most people are thinking. So it makes this area that was much less accessible much more accessible, I think. And part of that accessibility is this experience that you described is essentially taking that existing document and turning it into a sequence of rules. That's right. Without someone having to code those in some kind of way. Yeah, exactly. Exactly. And, you know, I think about or looked at like the steps of using the product.

23:23It's like generate this policy from this document, test and refine the policy, and then use the policy to validate LLM. That middle step of testing and refining seems like it's doing a lot of heavy lifting.

23:37Tell us about the effort involved in validating those policies. Yeah, yeah. So, I mean, first of all, I should say, like, you know, this product is going to grow and refine in response to how customers are using it. So we'll see kind of where we land in the future. But the idea that the big inspiration for us was previous work in IM Access Analyzer. So an IM Access Analyzer, it's actually a free product for AWS customers. It takes your policies. It takes all of the nouns, basically, all of the logical constants, and I'd say in logic, and assembles a set of questions and then asks you whether or not you think this policy should be guaranteeing those conditions.

24:27and you can say yes or no. And then when you say no, then basically it's helped you formalize the thing that you want to hold over your policies. And then as your policies evolve over time, it's able to now reestablish that the things that you wanted to hold, hold. So it sort of helps you figure out what your intent was with your policies. So is Policy Analyzer itself creating those questions and either identifying areas of ambiguity or areas that are likely important and asking you to put a stake in the ground? Exactly, yeah. So there's a bunch of tricks we can use. So for example, when we have a formula that describes truth, the set of true or untrue statements, that has logical structure, Boolean structure, and you can actually disassemble that Boolean structure.

25:21You can take all the convex holes. There's various operations you can do over that. and then find satisfying assignments in each of the convex slices of it and then ask the customer. So it's kind of like a coverage metric. It's saying, we explored all the weird corners of this. Now, there may be other values that are sort of neighbor, but you have at least checked all of the sort of representative corners. Okay. Yeah. And then you can imagine, the thing that we're also excited about is you can also use generative AI, right? That was going to be the next part of my question. I think the way folks would approach that today, a lot of folks are generating test sets for their LLME valves and they're using LLMs to help them generate these test sets.

26:16I didn't see that the automated reasoning tool was doing that middle part today, but it seemed like an easy extension if it's not. Yeah, so I mean, the product is very much aimed at people who are in the insurance industry or city zoning, right? We want to just make this super easy for people who are maybe interested but might probably not even interested in Gen.AI. Meaning if you already know about building test sets and running evals and that kind of thing, you might not be the target user? Yeah, that's right. The target user is the person who owns sprinklering in buildings in New York City.

27:05But your organization is trying to deploy a Gen. AI based solution to help your constituents get answers rather than having to queue and only come like Tuesdays and Thursdays to meet with you in a room and there's a huge queue of people. So maybe that's a good segue to what I promised to tell you about was when the general public began to get really excited about generative AI and everyone over the holiday break began using it, what I found in New York City is that many organizational leaders came back from the holiday with their boards telling them, like, what is your Gen.AI story, right? And so a bunch of people got excited about the idea of like, oh, well, fundamentally what we're doing is we're helping our customers make decisions or we're conveying information to our customers.

28:00So we want to provide that kind of information. And actually there's an inverse relationship where the customers that don't have money need that even more. They are trying to provide information and capabilities to their constituents or customers. And so they're excited about generative AI. But the problem was, and you see this a lot in the news, is that people began deploying those kinds of ideas and then they were misleading their customers. And when I looked at it, chatting with customers, I realized that in many cases there were formalizations underneath. Really in their mental model was there was a formalization.

28:37There were a set of rules. The other observation I have from my own personal experience, and we can talk about it even in Amazon, is that once you begin trying to actually formalize the rules, often a lot of like, you realize there's a lot of inconsistency, right? Like HR rules, and it's really funny because I work with, I have brought in many, many people from mathematical logic into Amazon and it's really funny to watch them interacting with HR people because they find all the weird corner cases of the rules, right? And so when you look at... Sounds like sales incentive plans also. Right, exactly, yeah.

29:16So when you begin looking at these organizational rules, they often don't compose well. They're often actually unsatisfiable. And so I personally think that there's a really amazing experience coming where we can use these tools to help organizations rationalize and understand and make decisions on which rules to add. Like they can now prototype, say, well, let's add this rule and then see what that's going to do. What are the answers to these questions? And what are all the questions that our customers have been asking for the past three years? Let's add this new rule and see how that would affect those questions.

29:51And maybe even there's some customers where we would have flipped the answer from yes to no. Well, let's go back to them and talk to them about, like, would that have been a problem for you? And that's all possible because of the sort of generative AI making these tools much more accessible. And then the rise of these tools that, you know, I don't think that P is equal to NP, but these tools sort of make, in many practical cases, MP feel like P, and you can use these tools now to solve these problems. So maybe pulling a little bit more on this compare and contrast between, I've got a document, use an LM to create a test set, run some evals, take the places where the LM got the answer wrong, put them back into your test set, fine.