Howdy y’all,
Next Monday (the 8th of April) at noon in CS 4310, Sam Drews will be speaking on a complexity analysis of the probabilistic synthesis algorithm presented in the MadPL CAV17 paper. We’ve been hyping this
talk for weeks now, so we hope to see you all there!
- Calvin
Abstract: Our CAV17 paper presented "DIGITS," which synthesizes {0,1}-valued programs that meet some probabilistic correctness property. The algorithm iteratively queries an SMT solver to produce candidate
programs consistent with finite sets of input-output constraints; somewhat surprisingly, DIGITS provably converges to near-optimal solutions by making only polynomially many such queries. In this talk, I plan to (1) give a brief overview of how our algorithm
operates, (2) highlight a few concepts from Computational Learning Theory on which our proof is based--namely "VC Dimension" and the "Sauer-Shelah Lemma"--, and finally (3) prove our polynomial bound (which is practically an immediate consequence of the aforementioned
lemma).