Human Judgment as a Specification

Brown PLT's PICK tackles the by-construction trap in LLM-generated formal specifications: if the spec encodes a misconception, the synthesized program is faithfully wrong, and stacking more LLMs on top adds agreement rather than the redundancy verification actually needs. Their fix routes validation through human judgment made cheap — instead of asking users to parse formal statements, PICK generates concrete disambiguating examples to upvote or downvote, sharpening vague intent into commitments and exposing the assumptions the prompt left unstated. The same algorithm covers regexes, linear temporal logic, and access-control policies; and when no candidate spec survives the feedback, that is itself the finding — the stated commitments can't be satisfied, better learned before shipping than after.

Visit Original Article →