May 23, 2026
BALD-PS: Factored Bayesian Active Learning for Specification Elicitation, with Symmetric Mutation-Equivalence Validation
Barsat Khadka
BALD-PS is a framework for interactive formal specification elicitation from ambiguous natural-language requirements using factored Bayesian active learning. The key insight is that a specification naturally decomposes into two predicates , a precondition (requires) describing valid inputs and a postcondition (ensures) describing acceptable outputs , allowing disagreement among candidate specifications to factorize into independent axes. The system samples diverse specifications from multiple LLM personas, identifies high-information disagreements using a factored BALD objective, and queries an oracle/developer with maximally informative edge cases to efficiently resolve ambiguity. Unlike traditional version-space elimination, BALD-PS synthesizes new specifications by recombining surviving precondition and postcondition fragments, enabling recovery of correct specifications that no single agent originally proposed. To validate specification quality, the framework introduces symmetric mutation-equivalence tightness, a bidirectional mutation-testing criterion that checks both whether implementations refute mutated specifications and whether specifications reject mutated implementations. Empirically, the method achieves perfect recovery on a controlled benchmark and substantially outperforms interactive refinement baselines on live HumanEval-style tasks while requiring fewer oracle queries.
No reviews are available yet
Cite this work
@misc {
title={
(HckPrj) BALD-PS: Factored Bayesian Active Learning for Specification Elicitation, with Symmetric Mutation-Equivalence Validation
},
author={
Barsat Khadka
},
date={
5/23/26
},
organization={Apart Research},
note={Research submission to the research sprint hosted by Apart.},
howpublished={https://apartresearch.com}
}


