Uniform sampling is a fundamental algorithmic problem with far-reaching implications: given a set of constraints, generate solutions uniformly at random from the solution space. The problem has garnered significant attention owing to its diverse applications spanning functional verification, security analysis, and artificial intelligence. This diversity in applications has led to the development of several sampling techniques, which typically fall into two categories: those with strong theoretical guarantees that often lack scalability, and scalable techniques that offer weak or no theoretical guarantees of uniformity. This gap between theory and practice mirrors a similar divide in software engineering – between the poor scalability of classical program synthesis techniques and the widespread use of billions of deployed programs. In software engineering, program testing helped bridge this divide. However, unlike deterministic program testing where a single trace can demonstrate a bug, one sample is usually insufficient to determine a sampler’s non-conformity to the desired distribution. This raises the question: can we design a testing methodology to verify if a sampler’s output distribution is close to uniform? In this tutorial paper, we reflect on the journey of designing Barbarik, the first system capable of testing whether a sampler’s distribution is close to uniform. We discuss how Barbarik’s availability sparked a virtuous cycle: it enabled the development of CMSGen, a state-of-the-art sampler whose design was guided by Barbarik, which in turn motivated further improvements in Barbarik through ScalBarbarik. This cycle demonstrates how testing can drive the development of practical tools that achieve an attractive balance between theoretical guarantees and empirical performance.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Testing and Design of Uniform CNF Samplers: A Virtuous Cycle Enabled by Distribution Testing

  • Mate Soos,
  • Sourav Chakraborty,
  • Kuldeep S. Meel

摘要

Uniform sampling is a fundamental algorithmic problem with far-reaching implications: given a set of constraints, generate solutions uniformly at random from the solution space. The problem has garnered significant attention owing to its diverse applications spanning functional verification, security analysis, and artificial intelligence. This diversity in applications has led to the development of several sampling techniques, which typically fall into two categories: those with strong theoretical guarantees that often lack scalability, and scalable techniques that offer weak or no theoretical guarantees of uniformity. This gap between theory and practice mirrors a similar divide in software engineering – between the poor scalability of classical program synthesis techniques and the widespread use of billions of deployed programs. In software engineering, program testing helped bridge this divide. However, unlike deterministic program testing where a single trace can demonstrate a bug, one sample is usually insufficient to determine a sampler’s non-conformity to the desired distribution. This raises the question: can we design a testing methodology to verify if a sampler’s output distribution is close to uniform? In this tutorial paper, we reflect on the journey of designing Barbarik, the first system capable of testing whether a sampler’s distribution is close to uniform. We discuss how Barbarik’s availability sparked a virtuous cycle: it enabled the development of CMSGen, a state-of-the-art sampler whose design was guided by Barbarik, which in turn motivated further improvements in Barbarik through ScalBarbarik. This cycle demonstrates how testing can drive the development of practical tools that achieve an attractive balance between theoretical guarantees and empirical performance.