Counterexample-Driven Synthesis for Probabilistic Program Sketches
This addresses the challenge of developing probabilistic programs for applications like controller synthesis, offering an automated solution to reduce complexity and errors, though it appears incremental as it builds on existing CEGIS methods.
The paper tackles the problem of synthesizing finite-state probabilistic programs, which are complex and error-prone to develop, by adopting counterexample-guided inductive synthesis (CEGIS) to automatically explore design spaces. Experiments show that millions of candidate designs can be fully explored using only a few thousand verification queries.
Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our approach leverages efficient model checking, modern SMT solving, and counterexample generation at program level. Experiments on practically relevant case studies show that design spaces with millions of candidate designs can be fully explored using a few thousand verification queries.