Disagreement between repeated AI translations can flag a vague requirement

Rajath Mahendrappa Kotyal of AWS argued on the AI Engineer show that a language model's tendency to answer differently each time can be put to use. Ask the model to turn the same requirement into formal logic several times. If its answers split, the requirement is probably vague. He also said the evidence behind this kind of approach is still thin.

What was said

Kotyal described Kiro, an AWS tool that checks a software specification before any design or code exists. A model translates each plain-English rule into a mathematical formula. A solver, a program that tests whether formulas can all be true together, then checks them.

His first example was a pair of order rules. Each reads sensibly alone, he said, but when the model reads them together, they cannot both be true.

For a sentence that may carry two meanings, the system goes further. It asks the model to translate the sentence seven or ten times. It then groups the results by logical equivalence, so answers that mean the same thing land together. Separate groups show where the model made its own assumptions. The user can then clear up the point, or the system holds back from building that piece.

His example was an instruction to remove a record. Kotyal called it "a very vague statement" and said a model should not be left free to pick a meaning. The tool offers the user two choices: delete the record, or keep it and hide it.

Why it matters

Our reading: a coding agent builds whatever the spec says, and a vague sentence gets one interpretation, picked silently. Repeated sampling makes that hidden choice visible before code exists. The model's inconsistency, usually a flaw, becomes a warning light.

For anyone buying or running agent tools, the question to ask is whether the tool surfaces ambiguity or quietly resolves it. Kotyal summed up the division of labour: "The LLM translates, the solver checks, and the human decide."

The other side

Kotyal was open about the limits. He said nothing other than the user can confirm that a specification is correct, so the user must check every part of the rule book. The model lacks domain knowledge, he said, and only the user can give a guarantee.

He added that little evidence yet exists for applying formal checking to agents. The excerpts give no figures on how often the method catches real ambiguity. They also do not say whether a model that agrees with itself is actually right.

When the user does not answer, the decision either goes to an LLM judge or the piece is not built. In the first case no human decides. The method can point at doubt, not settle it.