Property-based testing validates software against an executable specification by evaluating it on randomly generated inputs. The standard way that PBT users generate test inputs is via generators that describe how to sample test inputs through random choices. To achieve a good distribution over test inputs, users must tune their generators, i.e., decide on the weights of these individual random choices. Unfortunately, it is very difficult to understand how to choose individual generator weights in order to achieve a desired distribution, so today this process is tedious and limits the distributions that can be practically achieved. In this paper, we develop techniques for the automatic and offline tuning of generators. Given a generator with undetermined symbolic weights and an objective function, our approach automatically learns values for these weights that optimize for the objective. We describe useful objective functions that allow users to (1) target desired distributions and (2) improve the diversity and validity of their test cases. We have implemented our approach in a novel discrete probabilistic programming system, Loaded Dice , that supports differentiation and parameter learning, and use it as a language for generators. We empirically demonstrate that our approach is effective at optimizing generator distributions according to the specified objective functions. We also perform a thorough evaluation on PBT benchmarks, demonstrating that, when automatically tuned for diversity and validity, the generators exhibit a 3.1–7.4× speedup in bug finding.

Probabilistic programming languages (PPLs) are an expressive means for creating and reasoning about probabilistic models. Unfortunately hybrid probabilistic programs that involve both continuous and discrete structures are not well supported by today’s PPLs. In this paper we develop a new approximate inference algorithm for hybrid probabilistic programs that first discretizes the continuous distributions and then performs discrete inference on the resulting program. The key novelty is a form of discretization that we call bit blasting , which uses a binary representation of numbers such that a domain of 2 b discretized points can be succinctly represented as a discrete probabilistic program over poly b Boolean random variables. Surprisingly, we prove that many common continuous distributions can be bit blasted in a manner that incurs no loss of accuracy over an explicit discretization and supports efficient probabilistic inference. We have built a probabilistic programming system for hybrid programs called HyBit , which employs bit blasting followed by discrete probabilistic inference. We empirically demonstrate the benefits of our approach over existing sampling-based and symbolic inference approaches

Harman Singh, Poorva Garg, Mohit Gupta, Kevin Shah, Ashish Goswami, Satyam Modi, Arnab Mondal, Dinesh Khandelwal, Dinesh Garg, Parag Singla. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing. 2023.

Distributions on integers are ubiquitous in probabilistic modeling but remain challenging for many of today’s probabilistic programming languages (PPLs). The core challenge comes from discrete structure: many of today’s PPL inference strategies rely on enumeration, sampling, or differentiation in order to scale, which fail for high-dimensional complex discrete distributions involving integers. Our insight is that there is structure in arithmetic that these approaches are not using. We present a binary encoding strategy for discrete distributions that exploits the rich logical structure of integer operations like summation and comparison. We leverage this structured encoding with knowledge compilation to perform exact probabilistic inference, and show that this approach scales to much larger integer distributions with arithmetic.

This poster describes a low-cost and robust embedded platform, designed for vehicle mounted sensing of particulate matter (PM2.5 and PM10). The prototype is specifically designed to be mounted on the Delhi Integrated Multi-Modal Transit System (DIMTS) buses. Movement of the buses adds noise to pollution data. Error in GPS measurement causes issues in detecting moving vs. stationary state of the buses, useful to filter out noisy pollution data collected in the moving state. Intermittent cellular network connectivity causes frequent disconnects with the remote server. Our prototype is designed to handle such real world deployment challenges. Pilot deployment with this platform is currently ongoing. Preliminary data analysis from the pilot deployment will be discussed as part of the poster presentation, along with demonstration of the prototype sensor platform. This hardware prototype has the potential of creating locality wise, dense air pollution data providing crucial insights into the causes of air pollution.