# Your Spec Has Bugs. Catch Them Before Your Agent Codes. - Rajath Mahendrappa Kotyal, AWS

Rajath Mahendrappa Kotyal, AWS

[Talk page](https://ai.engineer/talks/0EnLxIbAvYk-your-spec-has-bugs-catch-them-before) · [Video](https://www.youtube.com/watch?v=0EnLxIbAvYk)

## Your Spec Has Bugs. Catch Them Before Your Agent Codes.

Kiro’s specification analyzer asks an LLM to translate a requirement several times, then uses a solver to check whether the translations mean the same thing. When they imply different product behavior, the user has a decision to make.

### One order that exposes two incompatible rules

[0:00](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=0s)

A customer submits an order for an item that is out of stock. What should the store do? One rule in the e-commerce specification says to place the order on backorder. Elsewhere in the same file, another rule forbids placing any order on backorder. Each reads clearly on its own. Give them the same submitted, out-of-stock order and every implementation has to violate one of them.

Rajath Mahendrappa Kotyal, who worked on Kiro’s specification analyzer in the automated reasoning group at AWS, wants to catch that decision before it reaches a coding agent. He cites research reporting a 20–40% drop in generated-code accuracy with unclear prompts, 60–90% of valid code still being wrong, and twice as many regressions on deployment. He gives no task definitions or comparison baselines for those figures, so they motivate checking the input without quantifying what Kiro fixes.

The analyzer acts as a first reviewer. Within one sentence it can look for a word with two meanings or a requirement written at the wrong level of detail. Across sentences it has a different job. It needs to find situations where two rules demand incompatible outcomes, or where the author has left a case uncovered. Polishing the two backorder rules individually would leave the store with exactly the same problem.

### Give the solver a case it can check

[2:50](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=170s)

Kiro first gives the LLM a chance to clean up the wording. If that leaves a question unresolved, the model translates the English into formulas in SMT-LIB, a language for expressing logical constraints. An SMT (satisfiability modulo theories) solver can then check whether any assignment of values satisfies the constraints under consideration. When the check exposes a problem, the analyzer sends the relevant sentence back to the LLM for another pass. A passing check needs no such revision.

What has to survive the translation of the inventory rule? In compact notation, its meaning is `(submitted AND inventory_unavailable) ⇒ backordered`. Both conditions belong on the left. Consider an order for which both are true. The implication now requires `backordered` to be true, while the blanket prohibition requires it to be false. Fixing the input case matters. With inventory available, the conditional rule makes no demand, so that case alone would never expose the conflict.

### Translate the same sentence seven or ten times

[4:08](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=248s)

A single translation quietly commits to one reading of the English. To see where that choice matters, Kiro asks the LLM to translate the same requirement repeatedly. Kotyal gives seven or ten samples as examples. The analyzer groups the resulting formulas by *logical equivalence*. Two translations belong together if they agree for every assignment of values, even when their expressions look different. Separate groups mean there is at least one case in which the translations disagree.

That disagreement gives the reviewer something specific to investigate. The model may have supplied different assumptions on different attempts. A solver can establish that the resulting formulas differ in meaning, but the split alone cannot tell which assumption the author intended. Kiro can accept an interpretation, ask the user to clarify, or leave that part unimplemented.

### Does removing a record delete it?

[5:05](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=305s)

Consider the instruction “remove the record.” What should remain afterward? Under one interpretation the system deletes the record. Under another it retains the record and hides it from users. A user looking at the list could see the same result either way, yet the two implementations leave different data behind. Kiro puts that concrete choice to the user.

Reviewing a set of rules produces two other kinds of question.

- **Conflict.** For the submitted, out-of-stock order, two rules apply and demand incompatible results. The author has to settle which behavior the store should implement.
- **Gap.** In the order example, no rule covers an idle order. There is no competing instruction to discard. The missing decision is what, if anything, the system should do in that state.

### Who decides what the specification should say?

[6:06](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=366s)

Even a consistent set of rules can describe the wrong product. A team may know what removal means in its domain and never have written that knowledge down. Reviewing the whole specification before handing it to the coding agent still falls to someone who knows the domain. Kotyal also describes the evidence for using this kind of formalization in agents as thin.

Kotyal sums up the division of work: “The LLM translates, the solver checks and the human decides.” Logical equivalence gives the solver a precise question it can settle about the translations. Choosing whether a record ought to survive deletion from the user’s view requires product judgment. If the user leaves that question unanswered, the workflow can fall back to an LLM judge or abstain from implementing that piece. Abstaining keeps an unresolved choice visible before it becomes code.

## Key takeaways

- Check requirements against the same concrete input. A submitted order with unavailable inventory activates the backorder rule and exposes its conflict with the blanket prohibition.
- Group repeated translations by logical equivalence. A split identifies readings that could change behavior and gives the user a specific decision to resolve.

## Slides

### Specs Have Bugs Too

[0:03](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=3s) [Opening slide credits Rajath Kotyal of Amazon Web Services’ Automated Reasoning Group.](https://assets.ai.engineer/sites/aiecode2025/sha256/19658f2516e2bb248dc443d026f4d9edc77087649b12cb0682ed175bc2b0cd0d.webp)

Specs Have Bugs Too. Catching them with an SMT solver before your agent writes code. Rajath Kotyal, Automated Reasoning Group, Amazon Web Services.

### Two fine rules, one bug

[0:30](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=30s) [One rule requires a backorder, while the second forbids every backorder.](https://assets.ai.engineer/sites/aiecode2025/sha256/d0f12f349b823d31b62c6f6ae07c4de6ab128b91b42e4c427ecee1a8f07ecc91.webp)

Two fine rules, one bug. R2: WHEN order submitted AND inventory unavailable SHALL place the order on backorder. R3: SHALL NOT place any order on backorder. Abridged.

### Unclear specs cost real accuracy

[1:36](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=96s) [Three reported measurements on unclear prompts, incorrect code and regressions.](https://assets.ai.engineer/sites/aiecode2025/sha256/c4c6dfc42c155701f86aefc4f5842d1b9ffef93577ff6621cb2d4a413e8038f2.webp)

Unclear specs cost real accuracy. 20–40% Pass@1 drop with unclear prompts. 60–90% of valid code still wrong. ~2× more regressions across versions. Larbi 2025 · Yang 2025.

### Two places spec bugs hide

[2:03](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=123s) [Two columns distinguish defects in a single sentence from conflicts or gaps across a set of rules.](https://assets.ai.engineer/sites/aiecode2025/sha256/a548a07866825eed050bb420df346e9ba5978a4aac73607c3280f920d0e60479.webp)

Two places spec bugs hide. In one sentence: ambiguity, wrong level of detail. Across the set: conflicts, gaps. Sentences need review. Sets need search.

### LLM translates, solver checks

[2:51](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=171s) [Three steps run from refining a requirement to checking its formal translation with a solver.](https://assets.ai.engineer/sites/aiecode2025/sha256/1365077fccf5a141a380136b63814bb415a72126d83b049ec439f083e999c397.webp)

LLM translates, solver checks. 1. LLM: Refine, clean up the wording. 2. LLM: Formalize, EARS to SMT-LIB. 3. SMT solver: Analyze conflicts, gaps, scenarios. Runs on requirements.md, before any code.

### Rules become logic

[3:48](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=228s) [A plain-language backorder rule appears above its logical implication.](https://assets.ai.engineer/sites/aiecode2025/sha256/6947c58fcc56b972b8c1b2f8853ffce4990d73f501c2856b3979759cb7532177.webp)

Rules become logic. WHEN order submitted AND inventory unavailable SHALL place the order on backorder. (=> (and submitted (not in_stock)) backordered). Illustrative encoding of R2.

### Sample, then cluster

[4:06](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=246s) [Three steps show how disagreement among translations can surface ambiguity.](https://assets.ai.engineer/sites/aiecode2025/sha256/9049850720d98962c6ae5bea90443e2167317221801f723b16e467d75b2b0760.webp)

Sample, then cluster. Sample several translations. Cluster by logical equivalence. Decide: accept, ask or abstain. Disagreement means ambiguity.

### Ask one clear question

[5:03](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=303s) [The example asks for a choice between deletion and retention of a hidden audit record.](https://assets.ai.engineer/sites/aiecode2025/sha256/7e4bf68f6ce951b3e0f320153999e53f891054f1caf15e785575e4c1e3b3f0c2.webp)

Ask one clear question. “remove the record”: gone, or kept for audit? A. Keep as-is: the record is gone. B. Change: retained, hidden from users.

### Check every rule at once

[5:36](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=336s) [The solver finds both a clash when stock runs out and a case the rules never cover.](https://assets.ai.engineer/sites/aiecode2025/sha256/f2dcc6424577b7b25bc0646bb066e79a1cb24544b5f1b50ef2e3a3c5835460e2.webp)

Check every rule at once. Conflict: R2 and R3 clash when stock runs out. Gap: no rule covers an idle order. A search problem, not a prediction problem.

### What it can’t do

[6:03](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=363s) [Three limits concern hidden domain knowledge, nondeterminism and the evidence for formalization.](https://assets.ai.engineer/sites/aiecode2025/sha256/43cb56f8056942b44339e149bc297ec66d2567c57733e267d83a2d6521d894d6.webp)

What it can’t do. “There is no oracle for specification correctness other than the user.” Dark matter: implicit domain knowledge. No guarantee: nondeterministic. Thin evidence for formalization.

### What to take back

[6:54](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=414s) [Closing slide lists four practices for reviewing requirements.](https://assets.ai.engineer/sites/aiecode2025/sha256/a655addae9f84b51eaab6f7377addf5888fe1a995e1383b7f79a103165d5620c.webp)

What to take back. 1. Check the spec before the code. 2. Cluster translations by logical equivalence. 3. LLM translates, solver checks, human decides. 4. Ask two-option questions; allow abstaining.

### References

[7:30](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=450s) [Resource slide lists the deep spec analysis article, AWS Automated Reasoning and Kiro.](https://assets.ai.engineer/sites/aiecode2025/sha256/e689217f8b31359127c4abef8e3e6d2bcf44adef39e87b2f515b8aed0165ffb2.webp)

References. How it works: kiro.dev/blog/deep-spec-analysis. Automated Reasoning: aws.amazon.com/security/provable-security. Kiro: kiro.dev.

## Full transcript

[0:00](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=0s) Hi everyone, my name is Rajat Kotial.

[0:02](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=2s) Hi everyone, my name is Rajat Kotial.

[0:02](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=2s) Hi everyone, my name is Rajat Kotial. I'm part of the automated reasoning

[0:04](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=4s) I'm part of the automated reasoning

[0:04](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=4s) I'm part of the automated reasoning group at AWS. And today I'm going to

[0:07](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=7s) group at AWS. And today I'm going to

[0:07](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=7s) group at AWS. And today I'm going to talk about a project I worked on

[0:09](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=9s) talk about a project I worked on

[0:09](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=9s) talk about a project I worked on recently called KO specification

[0:11](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=11s) recently called KO specification

[0:11](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=11s) recently called KO specification analyzer. And um we use certain

[0:14](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=14s) analyzer. And um we use certain

[0:14](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=14s) analyzer. And um we use certain techniques which involves formal methods

[0:16](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=16s) techniques which involves formal methods

[0:16](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=16s) techniques which involves formal methods and automated reasoning to prove

[0:19](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=19s) and automated reasoning to prove

[0:19](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=19s) and automated reasoning to prove specification that goes to your coding

[0:21](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=21s) specification that goes to your coding

[0:21](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=21s) specification that goes to your coding agent before it writes code.

[0:30](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=30s) So let's take a certain bug right

[0:34](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=34s) So let's take a certain bug right

[0:34](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=34s) So let's take a certain bug right this is a specification

[0:37](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=37s) this is a specification

[0:37](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=37s) this is a specification uh snippet and there are two rules for

[0:40](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=40s) uh snippet and there are two rules for

[0:40](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=40s) uh snippet and there are two rules for example and uh the rule two says when an

[0:43](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=43s) example and uh the rule two says when an

[0:43](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=43s) example and uh the rule two says when an order is submitted and this is for a a

[0:46](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=46s) order is submitted and this is for a a

[0:46](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=46s) order is submitted and this is for a a general e-commerce website let's say

[0:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=49s) general e-commerce website let's say

[0:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=49s) general e-commerce website let's say when an order is submitted and the

[0:50](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=50s) when an order is submitted and the

[0:50](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=50s) when an order is submitted and the inventory is unavailable we place the

[0:53](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=53s) inventory is unavailable we place the

[0:53](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=53s) inventory is unavailable we place the order as a back order which makes sense

[0:55](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=55s) order as a back order which makes sense

[0:55](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=55s) order as a back order which makes sense when you read it individually and

[0:57](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=57s) when you read it individually and

[0:57](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=57s) when you read it individually and there's also another rule in the same

[0:59](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=59s) there's also another rule in the same

[0:59](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=59s) there's also another rule in the same specification file uh which you hand to

[1:01](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=61s) specification file uh which you hand to

[1:01](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=61s) specification file uh which you hand to the coding agent which says u no order

[1:04](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=64s) the coding agent which says u no order

[1:04](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=64s) the coding agent which says u no order shall be placed as a back order and this

[1:06](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=66s) shall be placed as a back order and this

[1:06](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=66s) shall be placed as a back order and this is a rule we've set so individually read

[1:10](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=70s) is a rule we've set so individually read

[1:10](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=70s) is a rule we've set so individually read these two lines make sense right but in

[1:13](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=73s) these two lines make sense right but in

[1:14](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=74s) these two lines make sense right but in when an LLM reads this reads both the

[1:16](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=76s) when an LLM reads this reads both the

[1:16](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=76s) when an LLM reads this reads both the rules together both cannot hold true at

[1:19](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=79s) rules together both cannot hold true at

[1:19](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=79s) rules together both cannot hold true at the same time so we need to make sure

[1:22](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=82s) the same time so we need to make sure

[1:22](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=82s) the same time so we need to make sure the we resolve this ambiguity that the

[1:24](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=84s) the we resolve this ambiguity that the

[1:24](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=84s) the we resolve this ambiguity that the LLM is observing.

[1:28](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=88s) LLM is observing.

[1:28](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=88s) LLM is observing. And uh

[1:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=91s) And uh

[1:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=91s) And uh the scope and the reason we

[1:36](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=96s) the scope and the reason we

[1:36](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=96s) the scope and the reason we uh put an effort into this project is

[1:38](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=98s) uh put an effort into this project is

[1:38](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=98s) uh put an effort into this project is based on public research and recent

[1:41](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=101s) based on public research and recent

[1:41](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=101s) based on public research and recent research, we've observed there's a 20 to

[1:42](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=102s) research, we've observed there's a 20 to

[1:42](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=102s) research, we've observed there's a 20 to 40% drop with unclear prompts on the

[1:46](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=106s) 40% drop with unclear prompts on the

[1:46](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=106s) 40% drop with unclear prompts on the accuracy the LLM uh generates on the

[1:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=109s) accuracy the LLM uh generates on the

[1:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=109s) accuracy the LLM uh generates on the code accuracy, right? and 60 to 90% of

[1:52](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=112s) code accuracy, right? and 60 to 90% of

[1:52](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=112s) code accuracy, right? and 60 to 90% of valid code is still wrong after it

[1:54](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=114s) valid code is still wrong after it

[1:54](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=114s) valid code is still wrong after it writes it. And also in that case we

[1:57](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=117s) writes it. And also in that case we

[1:57](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=117s) writes it. And also in that case we observe two times the more more

[1:59](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=119s) observe two times the more more

[1:59](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=119s) observe two times the more more regressions when we uh deploy that code.

[2:05](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=125s) So where do bugs like these hide? Right?

[2:08](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=128s) So where do bugs like these hide? Right?

[2:08](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=128s) So where do bugs like these hide? Right? We want to detect these bugs before they

[2:10](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=130s) We want to detect these bugs before they

[2:10](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=130s) We want to detect these bugs before they reach the codebase. And the way only way

[2:13](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=133s) reach the codebase. And the way only way

[2:13](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=133s) reach the codebase. And the way only way to do that it's similar to how we write

[2:15](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=135s) to do that it's similar to how we write

[2:15](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=135s) to do that it's similar to how we write design docs. Similar to how we draw

[2:18](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=138s) design docs. Similar to how we draw

[2:18](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=138s) design docs. Similar to how we draw diagrams and flowcharts to make sure the

[2:20](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=140s) diagrams and flowcharts to make sure the

[2:20](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=140s) diagrams and flowcharts to make sure the flow is set before we write any code. We

[2:22](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=142s) flow is set before we write any code. We

[2:22](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=142s) flow is set before we write any code. We want to verify that without a human or

[2:26](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=146s) want to verify that without a human or

[2:26](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=146s) want to verify that without a human or anyone reading these files as the first

[2:29](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=149s) anyone reading these files as the first

[2:29](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=149s) anyone reading these files as the first reviewer

[2:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=151s) reviewer

[2:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=151s) reviewer in one sentence. Let's say the ambiguity

[2:34](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=154s) in one sentence. Let's say the ambiguity

[2:34](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=154s) in one sentence. Let's say the ambiguity and wording wrong level of detail but

[2:37](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=157s) and wording wrong level of detail but

[2:37](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=157s) and wording wrong level of detail but across sentences we can observe

[2:39](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=159s) across sentences we can observe

[2:39](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=159s) across sentences we can observe conflicts and gaps in the specification

[2:42](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=162s) conflicts and gaps in the specification

[2:42](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=162s) conflicts and gaps in the specification or rules. Right? sentences need reviews

[2:45](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=165s) or rules. Right? sentences need reviews

[2:45](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=165s) or rules. Right? sentences need reviews that need search in between them and

[2:47](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=167s) that need search in between them and

[2:48](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=168s) that need search in between them and ambiguity searches.

[2:50](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=170s) ambiguity searches.

[2:50](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=170s) ambiguity searches. So we have a three-step process to do

[2:53](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=173s) So we have a three-step process to do

[2:53](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=173s) So we have a three-step process to do this where the LLM will first refine it.

[2:56](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=176s) this where the LLM will first refine it.

[2:56](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=176s) this where the LLM will first refine it. It'll try to clean up the wording on its

[2:57](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=177s) It'll try to clean up the wording on its

[2:58](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=178s) It'll try to clean up the wording on its own and u if it succeeds then well and

[3:01](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=181s) own and u if it succeeds then well and

[3:01](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=181s) own and u if it succeeds then well and good but if it cannot we then formalize

[3:04](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=184s) good but if it cannot we then formalize

[3:04](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=184s) good but if it cannot we then formalize the um English language into SMT

[3:08](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=188s) the um English language into SMT

[3:08](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=188s) the um English language into SMT formulas. So, SMT lib is a certain set

[3:12](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=192s) formulas. So, SMT lib is a certain set

[3:12](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=192s) formulas. So, SMT lib is a certain set of type of function which we pass to a

[3:15](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=195s) of type of function which we pass to a

[3:15](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=195s) of type of function which we pass to a SAT solver a satisfiability checker

[3:17](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=197s) SAT solver a satisfiability checker

[3:17](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=197s) SAT solver a satisfiability checker where it's going to give out a boolean

[3:19](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=199s) where it's going to give out a boolean

[3:19](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=199s) where it's going to give out a boolean saying this expression that you've given

[3:22](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=202s) saying this expression that you've given

[3:22](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=202s) saying this expression that you've given me is valid true or false invalid

[3:27](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=207s) me is valid true or false invalid

[3:27](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=207s) me is valid true or false invalid and then once the solver gets back to us

[3:29](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=209s) and then once the solver gets back to us

[3:29](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=209s) and then once the solver gets back to us if that expression is valid then we

[3:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=211s) if that expression is valid then we

[3:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=211s) if that expression is valid then we don't do anything. But if it detects any

[3:33](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=213s) don't do anything. But if it detects any

[3:33](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=213s) don't do anything. But if it detects any ambiguity between two sentences or

[3:35](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=215s) ambiguity between two sentences or

[3:35](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=215s) ambiguity between two sentences or within a sentence where there's two

[3:37](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=217s) within a sentence where there's two

[3:37](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=217s) within a sentence where there's two meanings to a sentence, then we detect

[3:39](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=219s) meanings to a sentence, then we detect

[3:39](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=219s) meanings to a sentence, then we detect that and tell the LLM to recheck that

[3:43](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=223s) that and tell the LLM to recheck that

[3:43](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=223s) that and tell the LLM to recheck that sentence and it's going to reiterate on

[3:45](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=225s) sentence and it's going to reiterate on

[3:45](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=225s) sentence and it's going to reiterate on that.

[3:47](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=227s) that.

[3:47](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=227s) that. For example, the rules we saw

[3:51](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=231s) For example, the rules we saw

[3:51](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=231s) For example, the rules we saw we've seen when order is submitted and

[3:53](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=233s) we've seen when order is submitted and

[3:53](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=233s) we've seen when order is submitted and inventory is unavailable, we shall place

[3:55](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=235s) inventory is unavailable, we shall place

[3:55](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=235s) inventory is unavailable, we shall place the order as a back order. And in SMT

[3:59](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=239s) the order as a back order. And in SMT

[3:59](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=239s) the order as a back order. And in SMT format, it kind of looks like this. This

[4:01](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=241s) format, it kind of looks like this. This

[4:01](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=241s) format, it kind of looks like this. This is like a math formula, right?

[4:08](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=248s) Once we go deeper, we

[4:11](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=251s) Once we go deeper, we

[4:11](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=251s) Once we go deeper, we once we detect this, we also do a

[4:14](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=254s) once we detect this, we also do a

[4:14](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=254s) once we detect this, we also do a three-step process again where we sample

[4:17](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=257s) three-step process again where we sample

[4:17](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=257s) three-step process again where we sample the translations again and again. We ask

[4:19](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=259s) the translations again and again. We ask

[4:19](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=259s) the translations again and again. We ask the LLM to translate it seven times or

[4:21](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=261s) the LLM to translate it seven times or

[4:21](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=261s) the LLM to translate it seven times or 10 times and to understand whether this

[4:24](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=264s) 10 times and to understand whether this

[4:24](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=264s) 10 times and to understand whether this LLM is behaving this way uh based on its

[4:29](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=269s) LLM is behaving this way uh based on its

[4:29](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=269s) LLM is behaving this way uh based on its inherent capabilities or is something

[4:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=271s) inherent capabilities or is something

[4:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=271s) inherent capabilities or is something affecting it to behave this way and then

[4:34](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=274s) affecting it to behave this way and then

[4:34](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=274s) affecting it to behave this way and then based on logical equivalence of these

[4:36](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=276s) based on logical equivalence of these

[4:36](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=276s) based on logical equivalence of these seven or 10 um different set of

[4:39](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=279s) seven or 10 um different set of

[4:39](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=279s) seven or 10 um different set of interpretations by the LLM we cluster

[4:41](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=281s) interpretations by the LLM we cluster

[4:41](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=281s) interpretations by the LLM we cluster them on logical equivalence which sets

[4:44](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=284s) them on logical equivalence which sets

[4:44](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=284s) them on logical equivalence which sets which uh um entries came under which uh

[4:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=289s) which uh um entries came under which uh

[4:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=289s) which uh um entries came under which uh assumptions that the LLM made for itself

[4:52](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=292s) assumptions that the LLM made for itself

[4:52](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=292s) assumptions that the LLM made for itself and then we accept or ask the user to

[4:55](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=295s) and then we accept or ask the user to

[4:55](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=295s) and then we accept or ask the user to clear out the ambiguity or abstain from

[4:58](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=298s) clear out the ambiguity or abstain from

[4:58](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=298s) clear out the ambiguity or abstain from implementing that in the codebase.

[5:05](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=305s) This is an example of asking the human

[5:09](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=309s) This is an example of asking the human

[5:09](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=309s) This is an example of asking the human um what you want to do with that spec

[5:13](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=313s) um what you want to do with that spec

[5:13](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=313s) um what you want to do with that spec rule that was um perhaps contradicting.

[5:16](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=316s) rule that was um perhaps contradicting.

[5:16](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=316s) rule that was um perhaps contradicting. remove the record is very a very vague

[5:18](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=318s) remove the record is very a very vague

[5:18](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=318s) remove the record is very a very vague statement. The LLM cannot can interpret

[5:21](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=321s) statement. The LLM cannot can interpret

[5:21](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=321s) statement. The LLM cannot can interpret anything it wants but we shouldn't allow

[5:23](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=323s) anything it wants but we shouldn't allow

[5:23](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=323s) anything it wants but we shouldn't allow that to happen and we either give two

[5:26](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=326s) that to happen and we either give two

[5:26](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=326s) that to happen and we either give two options we keep it as is the record is

[5:28](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=328s) options we keep it as is the record is

[5:28](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=328s) options we keep it as is the record is deleted or we retain it and but hide it

[5:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=331s) deleted or we retain it and but hide it

[5:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=331s) deleted or we retain it and but hide it from the users which one does the user

[5:33](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=333s) from the users which one does the user

[5:33](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=333s) from the users which one does the user prefer.

[5:37](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=337s) Um

[5:39](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=339s) Um

[5:39](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=339s) Um a conflict is when the examples we

[5:41](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=341s) a conflict is when the examples we

[5:41](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=341s) a conflict is when the examples we example we saw rule one is conflicting

[5:43](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=343s) example we saw rule one is conflicting

[5:43](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=343s) example we saw rule one is conflicting with rule three and a gap is where no

[5:46](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=346s) with rule three and a gap is where no

[5:46](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=346s) with rule three and a gap is where no rule covers an idle order in this

[5:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=349s) rule covers an idle order in this

[5:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=349s) rule covers an idle order in this example where the LLM detected an actual

[5:53](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=353s) example where the LLM detected an actual

[5:53](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=353s) example where the LLM detected an actual sorry

[5:55](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=355s) sorry

[5:55](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=355s) sorry process or pipeline detected there's no

[5:58](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=358s) process or pipeline detected there's no

[5:58](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=358s) process or pipeline detected there's no um entry for this rule where you are

[6:01](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=361s) um entry for this rule where you are

[6:01](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=361s) um entry for this rule where you are missing something

[6:06](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=366s) all in Well, it cannot do a lot of

[6:08](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=368s) all in Well, it cannot do a lot of

[6:08](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=368s) all in Well, it cannot do a lot of things. End of the day, we want to make

[6:12](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=372s) things. End of the day, we want to make

[6:12](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=372s) things. End of the day, we want to make sure there is no oracle uh for for

[6:15](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=375s) sure there is no oracle uh for for

[6:15](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=375s) sure there is no oracle uh for for specification correctness other than the

[6:17](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=377s) specification correctness other than the

[6:17](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=377s) specification correctness other than the user. User needs to make sure to check

[6:20](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=380s) user. User needs to make sure to check

[6:20](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=380s) user. User needs to make sure to check every part of the snippet part of the

[6:23](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=383s) every part of the snippet part of the

[6:23](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=383s) every part of the snippet part of the rule book before sending it to the LLM.

[6:25](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=385s) rule book before sending it to the LLM.

[6:25](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=385s) rule book before sending it to the LLM. And um we as a tool only can help them

[6:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=391s) And um we as a tool only can help them

[6:31](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=391s) And um we as a tool only can help them and the user is more important here

[6:33](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=393s) and the user is more important here

[6:34](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=394s) and the user is more important here because of implicit domain knowledge.

[6:36](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=396s) because of implicit domain knowledge.

[6:36](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=396s) because of implicit domain knowledge. The LLM doesn't know a lot of domain

[6:37](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=397s) The LLM doesn't know a lot of domain

[6:38](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=398s) The LLM doesn't know a lot of domain knowledge and there's no guarantee I

[6:40](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=400s) knowledge and there's no guarantee I

[6:40](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=400s) knowledge and there's no guarantee I mean LLM only uh user can give that

[6:44](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=404s) mean LLM only uh user can give that

[6:44](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=404s) mean LLM only uh user can give that guarantee right and there's thin

[6:46](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=406s) guarantee right and there's thin

[6:46](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=406s) guarantee right and there's thin evidence right now for formalization and

[6:48](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=408s) evidence right now for formalization and

[6:48](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=408s) evidence right now for formalization and how it can be used in agents we are

[6:50](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=410s) how it can be used in agents we are

[6:50](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=410s) how it can be used in agents we are emerging in this technology

[6:56](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=416s) what do we take back from this um talk

[7:00](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=420s) what do we take back from this um talk

[7:00](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=420s) what do we take back from this um talk check the spec always before you pass it

[7:02](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=422s) check the spec always before you pass it

[7:02](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=422s) check the spec always before you pass it down to the agent uh cluster the

[7:05](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=425s) down to the agent uh cluster the

[7:05](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=425s) down to the agent uh cluster the translation We what we do is we cluster

[7:07](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=427s) translation We what we do is we cluster

[7:07](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=427s) translation We what we do is we cluster the translation by logical equivalent to

[7:11](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=431s) the translation by logical equivalent to

[7:11](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=431s) the translation by logical equivalent to determine the different LLM

[7:13](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=433s) determine the different LLM

[7:13](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=433s) determine the different LLM interpretations and where it's genuinely

[7:15](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=435s) interpretations and where it's genuinely

[7:15](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=435s) interpretations and where it's genuinely going wrong. The LLM translates, the

[7:18](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=438s) going wrong. The LLM translates, the

[7:18](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=438s) going wrong. The LLM translates, the solver checks and the human decides. We

[7:21](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=441s) solver checks and the human decides. We

[7:21](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=441s) solver checks and the human decides. We give the human uh options and if there's

[7:24](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=444s) give the human uh options and if there's

[7:24](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=444s) give the human uh options and if there's no answer to that, we use LLM judges or

[7:27](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=447s) no answer to that, we use LLM judges or

[7:27](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=447s) no answer to that, we use LLM judges or abstain from implementing that piece.

[7:32](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=452s) abstain from implementing that piece.

[7:32](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=452s) abstain from implementing that piece. Here are the references and u this work

[7:35](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=455s) Here are the references and u this work

[7:35](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=455s) Here are the references and u this work has been majorly contributed by my team

[7:38](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=458s) has been majorly contributed by my team

[7:38](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=458s) has been majorly contributed by my team um Andrea Jin Stefan and Delmos. You can

[7:42](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=462s) um Andrea Jin Stefan and Delmos. You can

[7:42](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=462s) um Andrea Jin Stefan and Delmos. You can check out their blog in the website link

[7:45](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=465s) check out their blog in the website link

[7:45](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=465s) check out their blog in the website link provided and um del deeper into this.

[7:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=469s) provided and um del deeper into this.

[7:49](https://www.youtube.com/watch?v=0EnLxIbAvYk&t=469s) provided and um del deeper into this. Thank you.