1 01:50:48,639 --> 01:50:50,390 I'm part of the automated reasoning 2 01:50:50,400 --> 01:50:53,430 group at AWS and today I'm going to talk 3 01:50:53,440 --> 01:50:56,310 about a project I worked on recently 4 01:50:56,320 --> 01:51:00,149 called KO specification analyzer and u 5 01:51:00,159 --> 01:51:02,149 we use certain techniques which involves 6 01:51:02,159 --> 01:51:03,990 formal methods and automated reasoning 7 01:51:04,000 --> 01:51:07,350 to prove specification that goes to your 8 01:51:07,360 --> 01:51:16,709 coding agent before it writes code. 9 01:51:16,719 --> 01:51:20,709 So let's take a certain bug right 10 01:51:20,719 --> 01:51:23,750 this is a specification 11 01:51:23,760 --> 01:51:26,470 uh snippet and there are two rules for 12 01:51:26,480 --> 01:51:29,830 example and uh the rule two says when an 13 01:51:29,840 --> 01:51:32,629 order is submitted and this is for a a 14 01:51:32,639 --> 01:51:35,189 general e-commerce website let's say 15 01:51:35,199 --> 01:51:36,950 when an order is submitted and the 16 01:51:36,960 --> 01:51:39,669 inventory is unavailable we place the 17 01:51:39,679 --> 01:51:41,830 order as a back order which makes sense 18 01:51:41,840 --> 01:51:43,669 when you read it individually and 19 01:51:43,679 --> 01:51:45,030 there's also another rule in the same 20 01:51:45,040 --> 01:51:47,510 specification file uh which you hand to 21 01:51:47,520 --> 01:51:50,070 the coding agent which says u no order 22 01:51:50,080 --> 01:51:52,790 shall be placed as a back order and this 23 01:51:52,800 --> 01:51:56,310 is a rule we've set so individually read 24 01:51:56,320 --> 01:51:59,990 these two lines make sense right but in 25 01:52:00,000 --> 01:52:02,790 when an LLM reads this reads both the 26 01:52:02,800 --> 01:52:05,030 rules together both cannot hold true at 27 01:52:05,040 --> 01:52:08,709 the same time so we need to make sure 28 01:52:08,719 --> 01:52:10,870 the we resolve this ambiguity that the 29 01:52:10,880 --> 01:52:14,390 LLM is observing 30 01:52:14,400 --> 01:52:17,270 and uh 31 01:52:17,280 --> 01:52:22,310 the scope and the reason we 32 01:52:22,320 --> 01:52:24,870 uh put an effort into this project is 33 01:52:24,880 --> 01:52:27,109 based on public research and recent 34 01:52:27,119 --> 01:52:28,870 research we've observed there's a 20 to 35 01:52:28,880 --> 01:52:32,709 40% drop with unclear prompts on the 36 01:52:32,719 --> 01:52:35,589 accuracy the LLM uh generates on the 37 01:52:35,599 --> 01:52:38,709 code accuracy right and 60 to 90% % of 38 01:52:38,719 --> 01:52:40,470 valid code is still wrong after it 39 01:52:40,480 --> 01:52:43,750 writes it and also in that case we 40 01:52:43,760 --> 01:52:45,750 observe two times the more more 41 01:52:45,760 --> 01:52:51,669 regressions when we uh deploy that code 42 01:52:51,679 --> 01:52:54,629 so where do bugs like these hide right 43 01:52:54,639 --> 01:52:56,950 we want to detect these bugs before they 44 01:52:56,960 --> 01:52:59,669 reach the code base and the way only way 45 01:52:59,679 --> 01:53:01,430 to do that it's similar to how we write 46 01:53:01,440 --> 01:53:04,149 design docs similar to how we draw 47 01:53:04,159 --> 01:53:06,709 diagrams and flowcharts to make sure the 48 01:53:06,719 --> 01:53:08,950 flow is set before we write any code. We 49 01:53:08,960 --> 01:53:12,470 want to verify that without a human or 50 01:53:12,480 --> 01:53:15,270 anyone reading these files as the first 51 01:53:15,280 --> 01:53:17,189 reviewer. 52 01:53:17,199 --> 01:53:20,790 In one sentence, let's say the ambiguity 53 01:53:20,800 --> 01:53:23,669 and wording wrong level of detail, but 54 01:53:23,679 --> 01:53:25,589 across sentences, we can observe 55 01:53:25,599 --> 01:53:28,149 conflicts and gaps in the specification 56 01:53:28,159 --> 01:53:31,510 or rules, right? Sentences need reveals 57 01:53:31,520 --> 01:53:33,990 that need search and between them and 58 01:53:34,000 --> 01:53:36,550 ambiguity searches. 59 01:53:36,560 --> 01:53:39,350 So we have a three-step process to do 60 01:53:39,360 --> 01:53:42,390 this where the LLM will first refine it. 61 01:53:42,400 --> 01:53:43,750 It will try to clean up the wording on 62 01:53:43,760 --> 01:53:47,510 its own and um if it succeeds then well 63 01:53:47,520 --> 01:53:49,350 and good but if it cannot we then 64 01:53:49,360 --> 01:53:50,870 formalize 65 01:53:50,880 --> 01:53:54,629 the um English language into SMT 66 01:53:54,639 --> 01:53:59,109 formulas. So SMT lib is a certain set of 67 01:53:59,119 --> 01:54:01,589 type of function which we pass to a SAT 68 01:54:01,599 --> 01:54:04,070 solver a satisfiability checker where 69 01:54:04,080 --> 01:54:06,310 it's going to give out a boolean saying 70 01:54:06,320 --> 01:54:09,109 this expression that you've given me is 71 01:54:09,119 --> 01:54:13,109 valid true or false invalid 72 01:54:13,119 --> 01:54:15,589 and then once the solver gets back to us 73 01:54:15,599 --> 01:54:17,750 if that expression is valid then we 74 01:54:17,760 --> 01:54:19,430 don't do anything. But if it detects any 75 01:54:19,440 --> 01:54:21,510 ambiguity between two sentences or 76 01:54:21,520 --> 01:54:23,750 within a sentence where there's two 77 01:54:23,760 --> 01:54:25,750 meanings to a sentence, then we detect 78 01:54:25,760 --> 01:54:29,589 that and tell the LLM to recheck that 79 01:54:29,599 --> 01:54:31,830 sentence and it's going to reiterate on 80 01:54:31,840 --> 01:54:33,750 that. 81 01:54:33,760 --> 01:54:37,270 For example, the rules we saw, 82 01:54:37,280 --> 01:54:39,430 we've seen when order is submitted and 83 01:54:39,440 --> 01:54:41,910 inventory is unavailable, we shall place 84 01:54:41,920 --> 01:54:45,589 the order as a back order. And in SMT 85 01:54:45,599 --> 01:54:47,350 format, it kind of looks like this. This 86 01:54:47,360 --> 01:54:54,550 is like a mass formula, right? 87 01:54:54,560 --> 01:54:57,270 Once we go deeper, we 88 01:54:57,280 --> 01:55:00,470 once we detect this, we also do a 89 01:55:00,480 --> 01:55:03,189 three-step process again where we sample 90 01:55:03,199 --> 01:55:05,750 the translations again and again. We ask 91 01:55:05,760 --> 01:55:07,669 the LLM to translate it seven times or 92 01:55:07,679 --> 01:55:10,870 10 times and to understand whether this 93 01:55:10,880 --> 01:55:15,589 LLM is behaving this way uh based on 94 01:55:15,599 --> 01:55:17,350 its inherent capabilities or is 95 01:55:17,360 --> 01:55:18,950 something affecting it to behave this 96 01:55:18,960 --> 01:55:21,189 way and then based on logical 97 01:55:21,199 --> 01:55:24,790 equivalence of these seven or 10 um 98 01:55:24,800 --> 01:55:26,470 different set of interpretations by the 99 01:55:26,480 --> 01:55:28,950 LLM we cluster them on logical 100 01:55:28,960 --> 01:55:33,030 equivalence which sets which uh um 101 01:55:33,040 --> 01:55:36,149 entries came under which uh assumptions 102 01:55:36,159 --> 01:55:39,589 that the LLM made for itself and then we 103 01:55:39,599 --> 01:55:42,470 accept or ask the user to clear out the 104 01:55:42,480 --> 01:55:44,950 ambiguity or abstain from implementing 105 01:55:44,960 --> 01:55:51,750 that in the codebase. 106 01:55:51,760 --> 01:55:55,189 This is an example of asking the human 107 01:55:55,199 --> 01:55:59,109 um what you want to do with that spec 108 01:55:59,119 --> 01:56:02,950 rule that was um perhaps contradicting. 109 01:56:02,960 --> 01:56:04,870 remove the record is very a very vague 110 01:56:04,880 --> 01:56:07,189 statement. The LLM cannot can interpret 111 01:56:07,199 --> 01:56:09,910 anything it wants but we shouldn't allow 112 01:56:09,920 --> 01:56:12,709 that to happen and we either give two 113 01:56:12,719 --> 01:56:14,629 options we keep it as is the record is 114 01:56:14,639 --> 01:56:17,430 deleted or we retain it and but hide it 115 01:56:17,440 --> 01:56:23,589 from the users which one does the user. 116 01:56:23,599 --> 01:56:25,350 Um 117 01:56:25,360 --> 01:56:27,910 a conflict is when the examples we 118 01:56:27,920 --> 01:56:29,830 example we saw rule one it's conflicting 119 01:56:29,840 --> 01:56:32,950 with rule three and a gap is where no 120 01:56:32,960 --> 01:56:35,589 rule covers an idle order in this 121 01:56:35,599 --> 01:56:39,510 example where the LLM detected an actual 122 01:56:39,520 --> 01:56:41,189 sorry 123 01:56:41,199 --> 01:56:44,709 process or pipeline detected there's no 124 01:56:44,719 --> 01:56:47,189 um entry for this rule where you are 125 01:56:47,199 --> 01:56:52,149 missing something 126 01:56:52,159 --> 01:56:54,550 all in Well, it cannot do a lot of 127 01:56:54,560 --> 01:56:57,990 things. End of the day, we want to make 128 01:56:58,000 --> 01:57:01,350 sure there is no oracle uh for for 129 01:57:01,360 --> 01:57:03,030 specification correctness other than the 130 01:57:03,040 --> 01:57:06,310 user. User needs to make sure to check 131 01:57:06,320 --> 01:57:09,270 every part of the snippet part of the 132 01:57:09,280 --> 01:57:11,910 rule book before sending it to the LLM. 133 01:57:11,920 --> 01:57:17,430 And um we as a tool only can help them 134 01:57:17,440 --> 01:57:19,990 and the user is more important here 135 01:57:20,000 --> 01:57:22,310 because of implicit domain knowledge. 136 01:57:22,320 --> 01:57:23,990 The LLM doesn't know a lot of domain 137 01:57:24,000 --> 01:57:26,070 knowledge and there's no guarantee I 138 01:57:26,080 --> 01:57:30,149 mean LLM only uh user can give that 139 01:57:30,159 --> 01:57:32,310 guarantee right and there's thin 140 01:57:32,320 --> 01:57:34,310 evidence right now for formalization and 141 01:57:34,320 --> 01:57:36,709 how it can be used in agents we are 142 01:57:36,719 --> 01:57:42,950 emerging in this technology 143 01:57:42,960 --> 01:57:46,310 what do we take back from this um talk 144 01:57:46,320 --> 01:57:48,709 check the spec always before you pass it 145 01:57:48,719 --> 01:57:51,589 down to the agent uh cluster the 146 01:57:51,599 --> 01:57:53,910 translation We what we do is we cluster 147 01:57:53,920 --> 01:57:57,030 the translation by logical equivalent to 148 01:57:57,040 --> 01:57:59,350 determine the different LLM 149 01:57:59,360 --> 01:58:01,589 interpretations and where it's genuinely 150 01:58:01,599 --> 01:58:04,470 going wrong. The LLM translates the 151 01:58:04,480 --> 01:58:07,750 solver checks and the human decide. We 152 01:58:07,760 --> 01:58:10,629 give give the human uh options and if 153 01:58:10,639 --> 01:58:13,109 there's no answer to that we use LLM 154 01:58:13,119 --> 01:58:15,669 judges or abstain from implementing that 155 01:58:15,679 --> 01:58:17,990 piece. 156 01:58:18,000 --> 01:58:21,430 Here are the references and um this work 157 01:58:21,440 --> 01:58:24,629 has been majorly contributed by my team 158 01:58:24,639 --> 01:58:28,149 um Anda Jin, Stefan, Nia and Delmos. You 159 01:58:28,159 --> 01:58:30,790 can check out their blog in the website 160 01:58:30,800 --> 01:58:34,470 link provided and um del deeper into 161 01:58:34,480 --> 01:58:35,589 this. Thank you.