DiffSpec-PBT
Fatimah Emad Eldin
Prompt independent LLM spec authors for the same natural-language requirement. Use property-based testing on each spec pair to surface inputs/outputs where they disagree. Each disagreement is a concrete counterexample of intent drift, classified by type. Any OpenAI-compatible endpoint can serve as an author; the eval harness runs all pairs among committed fixture aliases.
This paper presents a very neat and cleanly implemented pbt-based validation methodology for LLM outputs. The proposal is such that given a natural language spec and an implementation, several llms are asked to generate pre/post specs for the program. The analysis then performs a pairwise comparison of the specs and uses random inputs to surface discrepancies between the specs.
One comment I would have is that the paper's motivation of sound/over/underspecified specifications might need a bit more iteration. From the paper, as I understand, the terms are defined as follows:
- for any input,output pair, if the input passes the precondition of all specs, then every spec should accept, and a rejection indicates that a spec is overconstrained
- for any input, output pair, if a mutated copy of the output is rejected by any spec, then every spec should reject, and an accepting spec is underconstrained.
This fails to handle cases when the specification generated by a tool is incorrect. Consider a sorting spec that asserts that all its outputs are positive, If a mutation replaces the first element of the output with a negative number, then the other specifications would accept, and the erroneous specification would reject, leading this methodology to mark the other specifications as underconstrained.
This is an interesting idea with a well-thought out execution and empirical examination. A difference between two independent specs provides assurances that at least one of them is wrong, escaping what might be thought a circularity in SPS generally needing a golden reference to have confidence in a written spec. The writeup was clear and honestly described strengths and weaknesses with the results and implementation, and allowed easy comprehension of what has been achieved.
It is implied in discussion, but the description of the LLM as an 'oracle' in this project overstates what purpose it serves - it's a disagreement detector, not an arbiter of truth. This is still pretty neat!
Using the unmodified 'real world' task was a nice confirmation of the methods and adds significant weight to the credibility.
I would be interested to see what the correlation is between frontier models - since a) this will remove all the Python coding issues, probably and b) I'm concerned that that shared training data + increasingly similar training methods might just make all the failures correlate highly, obviating the usefulness of this approach.
Cite this work
@misc {
title={
(HckPrj) DiffSpec-PBT
},
author={
Fatimah Emad Eldin
},
date={
},
organization={Apart Research},
note={Research submission to the research sprint hosted by Apart.},
howpublished={https://apartresearch.com}
}


