Rajath Mahendrappa Kotyal of AWS’s automated reasoning group presents a seven-minute AI Engineer talk about checking requirements before an agent implements them.
A bug in the instructions
- One e-commerce rule says to backorder an item when inventory is unavailable; another forbids all backorders. Each reads sensibly alone, but both cannot hold together.
- An instruction like “remove the record” could mean delete it or hide it from users. The owner must choose the intended behavior.
- Rules can also leave a gap: no rule covers an idle order in his example.
The proposed check
- Ask an LLM to clarify the language; translate stubborn cases into logical constraints for an SMT solver, a tool that checks whether constraints can all hold together.
- Sample several translations and cluster logically equivalent interpretations. Disagreement helps locate assumptions the wording left open.
- Show the conflicting options to the person who owns the requirement; clarify it or abstain before writing code.
Limit
- Kotyal emphasizes that domain knowledge lives with the user. The solver checks the formalized rules, but a mistranslation or missing business rule can still slip through.
- This talk demonstrates a proposed workflow and examples; it does not establish a measured success rate for the analyzer.
“The LLM translates, the solver checks and the human decides.”