# Specs have bugs too Source: https://www.youtube.com/watch?v=ZZ19zhYnDKY Machine-generated transcript; recognition errors remain. Source-recording timestamps. Boundary-crossing subtitle ends are clipped to this session. [01:50:48](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6648s) I'm part of the automated reasoning [01:50:50](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6650s) group at AWS and today I'm going to talk [01:50:53](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6653s) about a project I worked on recently [01:50:56](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6656s) called KO specification analyzer and u [01:51:00](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6660s) we use certain techniques which involves [01:51:02](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6662s) formal methods and automated reasoning [01:51:04](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6664s) to prove specification that goes to your [01:51:07](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6667s) coding agent before it writes code. [01:51:16](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6676s) So let's take a certain bug right [01:51:20](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6680s) this is a specification [01:51:23](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6683s) uh snippet and there are two rules for [01:51:26](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6686s) example and uh the rule two says when an [01:51:29](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6689s) order is submitted and this is for a a [01:51:32](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6692s) general e-commerce website let's say [01:51:35](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6695s) when an order is submitted and the [01:51:36](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6696s) inventory is unavailable we place the [01:51:39](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6699s) order as a back order which makes sense [01:51:41](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6701s) when you read it individually and [01:51:43](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6703s) there's also another rule in the same [01:51:45](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6705s) specification file uh which you hand to [01:51:47](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6707s) the coding agent which says u no order [01:51:50](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6710s) shall be placed as a back order and this [01:51:52](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6712s) is a rule we've set so individually read [01:51:56](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6716s) these two lines make sense right but in [01:52:00](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6720s) when an LLM reads this reads both the [01:52:02](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6722s) rules together both cannot hold true at [01:52:05](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6725s) the same time so we need to make sure [01:52:08](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6728s) the we resolve this ambiguity that the [01:52:10](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6730s) LLM is observing [01:52:14](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6734s) and uh [01:52:17](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6737s) the scope and the reason we [01:52:22](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6742s) uh put an effort into this project is [01:52:24](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6744s) based on public research and recent [01:52:27](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6747s) research we've observed there's a 20 to [01:52:28](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6748s) 40% drop with unclear prompts on the [01:52:32](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6752s) accuracy the LLM uh generates on the [01:52:35](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6755s) code accuracy right and 60 to 90% % of [01:52:38](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6758s) valid code is still wrong after it [01:52:40](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6760s) writes it and also in that case we [01:52:43](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6763s) observe two times the more more [01:52:45](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6765s) regressions when we uh deploy that code [01:52:51](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6771s) so where do bugs like these hide right [01:52:54](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6774s) we want to detect these bugs before they [01:52:56](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6776s) reach the code base and the way only way [01:52:59](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6779s) to do that it's similar to how we write [01:53:01](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6781s) design docs similar to how we draw [01:53:04](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6784s) diagrams and flowcharts to make sure the [01:53:06](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6786s) flow is set before we write any code. We [01:53:08](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6788s) want to verify that without a human or [01:53:12](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6792s) anyone reading these files as the first [01:53:15](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6795s) reviewer. [01:53:17](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6797s) In one sentence, let's say the ambiguity [01:53:20](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6800s) and wording wrong level of detail, but [01:53:23](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6803s) across sentences, we can observe [01:53:25](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6805s) conflicts and gaps in the specification [01:53:28](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6808s) or rules, right? Sentences need reveals [01:53:31](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6811s) that need search and between them and [01:53:34](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6814s) ambiguity searches. [01:53:36](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6816s) So we have a three-step process to do [01:53:39](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6819s) this where the LLM will first refine it. [01:53:42](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6822s) It will try to clean up the wording on [01:53:43](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6823s) its own and um if it succeeds then well [01:53:47](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6827s) and good but if it cannot we then [01:53:49](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6829s) formalize [01:53:50](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6830s) the um English language into SMT [01:53:54](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6834s) formulas. So SMT lib is a certain set of [01:53:59](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6839s) type of function which we pass to a SAT [01:54:01](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6841s) solver a satisfiability checker where [01:54:04](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6844s) it's going to give out a boolean saying [01:54:06](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6846s) this expression that you've given me is [01:54:09](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6849s) valid true or false invalid [01:54:13](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6853s) and then once the solver gets back to us [01:54:15](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6855s) if that expression is valid then we [01:54:17](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6857s) don't do anything. But if it detects any [01:54:19](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6859s) ambiguity between two sentences or [01:54:21](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6861s) within a sentence where there's two [01:54:23](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6863s) meanings to a sentence, then we detect [01:54:25](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6865s) that and tell the LLM to recheck that [01:54:29](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6869s) sentence and it's going to reiterate on [01:54:31](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6871s) that. [01:54:33](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6873s) For example, the rules we saw, [01:54:37](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6877s) we've seen when order is submitted and [01:54:39](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6879s) inventory is unavailable, we shall place [01:54:41](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6881s) the order as a back order. And in SMT [01:54:45](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6885s) format, it kind of looks like this. This [01:54:47](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6887s) is like a mass formula, right? [01:54:54](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6894s) Once we go deeper, we [01:54:57](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6897s) once we detect this, we also do a [01:55:00](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6900s) three-step process again where we sample [01:55:03](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6903s) the translations again and again. We ask [01:55:05](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6905s) the LLM to translate it seven times or [01:55:07](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6907s) 10 times and to understand whether this [01:55:10](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6910s) LLM is behaving this way uh based on [01:55:15](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6915s) its inherent capabilities or is [01:55:17](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6917s) something affecting it to behave this [01:55:18](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6918s) way and then based on logical [01:55:21](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6921s) equivalence of these seven or 10 um [01:55:24](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6924s) different set of interpretations by the [01:55:26](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6926s) LLM we cluster them on logical [01:55:28](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6928s) equivalence which sets which uh um [01:55:33](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6933s) entries came under which uh assumptions [01:55:36](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6936s) that the LLM made for itself and then we [01:55:39](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6939s) accept or ask the user to clear out the [01:55:42](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6942s) ambiguity or abstain from implementing [01:55:44](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6944s) that in the codebase. [01:55:51](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6951s) This is an example of asking the human [01:55:55](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6955s) um what you want to do with that spec [01:55:59](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6959s) rule that was um perhaps contradicting. [01:56:02](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6962s) remove the record is very a very vague [01:56:04](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6964s) statement. The LLM cannot can interpret [01:56:07](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6967s) anything it wants but we shouldn't allow [01:56:09](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6969s) that to happen and we either give two [01:56:12](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6972s) options we keep it as is the record is [01:56:14](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6974s) deleted or we retain it and but hide it [01:56:17](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6977s) from the users which one does the user. [01:56:23](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6983s) Um [01:56:25](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6985s) a conflict is when the examples we [01:56:27](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6987s) example we saw rule one it's conflicting [01:56:29](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6989s) with rule three and a gap is where no [01:56:32](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6992s) rule covers an idle order in this [01:56:35](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6995s) example where the LLM detected an actual [01:56:39](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=6999s) sorry [01:56:41](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7001s) process or pipeline detected there's no [01:56:44](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7004s) um entry for this rule where you are [01:56:47](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7007s) missing something [01:56:52](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7012s) all in Well, it cannot do a lot of [01:56:54](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7014s) things. End of the day, we want to make [01:56:58](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7018s) sure there is no oracle uh for for [01:57:01](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7021s) specification correctness other than the [01:57:03](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7023s) user. User needs to make sure to check [01:57:06](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7026s) every part of the snippet part of the [01:57:09](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7029s) rule book before sending it to the LLM. [01:57:11](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7031s) And um we as a tool only can help them [01:57:17](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7037s) and the user is more important here [01:57:20](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7040s) because of implicit domain knowledge. [01:57:22](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7042s) The LLM doesn't know a lot of domain [01:57:24](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7044s) knowledge and there's no guarantee I [01:57:26](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7046s) mean LLM only uh user can give that [01:57:30](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7050s) guarantee right and there's thin [01:57:32](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7052s) evidence right now for formalization and [01:57:34](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7054s) how it can be used in agents we are [01:57:36](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7056s) emerging in this technology [01:57:42](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7062s) what do we take back from this um talk [01:57:46](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7066s) check the spec always before you pass it [01:57:48](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7068s) down to the agent uh cluster the [01:57:51](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7071s) translation We what we do is we cluster [01:57:53](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7073s) the translation by logical equivalent to [01:57:57](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7077s) determine the different LLM [01:57:59](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7079s) interpretations and where it's genuinely [01:58:01](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7081s) going wrong. The LLM translates the [01:58:04](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7084s) solver checks and the human decide. We [01:58:07](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7087s) give give the human uh options and if [01:58:10](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7090s) there's no answer to that we use LLM [01:58:13](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7093s) judges or abstain from implementing that [01:58:15](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7095s) piece. [01:58:18](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7098s) Here are the references and um this work [01:58:21](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7101s) has been majorly contributed by my team [01:58:24](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7104s) um Anda Jin, Stefan, Nia and Delmos. You [01:58:28](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7108s) can check out their blog in the website [01:58:30](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7110s) link provided and um del deeper into [01:58:34](https://www.youtube.com/watch?v=ZZ19zhYnDKY&t=7114s) this. Thank you.