Your Spec Has Bugs. Catch Them Before Your Agent Codes. - Rajath Mahendrappa Kotyal, AWS Transcript, AI Summary & Key Points

00:00 Hi everyone. My name is Rajat Kotyal. I'm part of the automated reasoning group at AWS. And today I'm going to talk about a project I worked on recently called Keto Specification Analyzer. And we use certain techniques which involves formal methods and automated reasoning to prove specification that goes to your coding agent before it writes code. So let's take a certain bug, right?

00:34 This is a specification uh snippet and there are two rules for example and the rule two says when an order is submitted and this is for a a general e-commerce website, let's say. When an order is submitted and the inventory is unavailable, we place the order as a back order which makes sense when you read it individually. And there's also another rule in the same specification file which you hand to the coding agent which says no order shall be placed as a back order and this is a rule we'll set.

01:09 So individually read these two lines make sense, right? But in when an LLM reads this, reads both the rules together, both cannot hold true at the same time. So we need to make sure the we resolve this ambiguity that the LLM is observing. And uh the scope and the reason we uh put an effort into this project is based on public research and recent research we've observed there's a 20 to 40% drop with unclear prompts on the accuracy the LLM generates and the code accuracy, right?

01:50 And 60 to 90% of valid code is still wrong after it writes it. And also in that case we observed two times the more more regressions when we deploy that code. So where do bugs like these hide, right? We want to detect these bugs before they reach the code base and the way only way to do that it's similar to how we write design docs, similar to how we draw diagrams and flow charts to make sure the flow is set before we write any code.

02:21 We want to verify that without a human or anyone reading these files as the first reviewer. In one sentence let's say the ambiguity and wording wrong level of detail, but across sentences we can observe conflicts and gaps in these specification or rules, right? Sentences need review, such need search in between them and ambiguity searches. So we have a three-step process to do this where the LLM will first refine it.

02:55 It will try to clean up the wording on its own and if it succeeds then well and good, but if it cannot we then formalize the English language into SMT formulas. So SMT lib is a certain set of type of function which we pass to a SAT solver or satisfiability checker where it's going to give out a Boolean saying this expression that you're giving me is valid, true or false, invalid.

03:27 And then once the solver gets back to us if that expression is valid then we don't do anything, but if it detects any ambiguity between two sentences or within a sentence where there's two meanings to a sentence then we detect that and tell the LLM to recheck that sentence and it's going to re-iterate on that. For example, the rules we saw we've seen when order is submitted and inventory level unavailable we shall place the order as a back order and in SMT format it kind of looks like this, this like a math formula,

04:01 right? Once we go deeper, we once we detect this, we also do three-step process again where we sample the translations again and again. We ask the LLM to translate seven times or 10 times and to understand whether this LLM is behaving this way based on its its inherent capabilities or is something affecting it to behave this way. And then based on logical equivalence of these seven or 10 different set of interpretations by the LLM, we cluster them on logical equivalence which sets which entries came under which

04:46 assumptions that their LLM made for itself. And then we accept or ask the user to clear out the ambiguity or abstain from implementing that in the codebase. This is an example of asking the human what you want to do with that rule that was perhaps contradicting. Remove the record is very very vague statement. The LLM cannot can interpret anything it wants, but we shouldn't allow that to happen.

05:23 And we either give two options. We keep it as is. The record is deleted or we retain it and but hide it from the users. Which one does the user prefer? A conflict is when the examples example we saw rule one is conflicting with rule three. And a gap is where no rule covers an idle order in this example where the LLM detected an actual sorry the process or pipeline detected there's no entry for this rule where you are missing something.

06:06 All in all, it cannot do a lot of things under the day. We want to make sure there is no oracle uh for for specification correctness other than the user. User needs to make sure to check every part of the snippet, part of the rule book before sending it to the LLM. And we as a tool only can help them. And the user is more important here because of implicit domain knowledge.

06:34 The LLM doesn't know a lot of domain knowledge and there's no guarantee from an LLM. Only uh user can give that guarantee, right? And there's thin evidence right now for formalization and how it can be used in agents. We are emerging in this technology. What do we take back from this talk? Check the spec always before you pass it down to the agent. Cluster the translation we what we do is we cluster the translation by logical equivalence to determine the different LLM interpretations and where it's genuinely going

07:14 wrong. The LLM translates, the solver checks and the human decides. We give to give the human options and if there's no answer to that, we use LLM judges or abstain from implementing that piece. Here are the references and this work has been majorly contributed by my team you can check out their blog and the website link provided and delve deeper into this. Thank you.