Eliciting Specifications: When Does Interactive Clarification Help?

arXiv:2610.22382v1 Announce Type: cross Abstract: 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