Eliciting Specifications: When Does Interactive Clarification Help?
LLMs can generate Lean specifications from task descriptions, but those descriptions are often underspecified or ambiguous and may omit verifier-relevant edge cases, yielding imperfect formal specifications. We study whether an elicitation agent (EA) can improve verifier-checked Lean specifications by seeking clarifica...
Mowafak Allaham, Aditya Vempaty, Ashish Jagmohan et al.
· 0 citations