FMitF: Track I: Verified Probabilistic Programming for Hybrid Systems

The project is developing a probabilistic programming framework for expressing differential equations and hybrid system models that combine the continuous evolution of state with instantaneous state and mode changes through discrete actions. The probabilistic programming framework is being applied to modeling in key areas, including epidemiology, medical devices, and autonomous systems.

The project's novelties include the development of the modeling formalism that incorporates models of continuous-time systems, systematic model transformation techniques, and the use of formal techniques to verify these transformations rigorously. The project's impacts include a useful modeling framework that will help the cause of rigorous model-based decision-making in diverse areas ranging from public policy to robotics and medicine.

The project is recruiting a diverse cohort of undergraduate researchers through summer research experience for undergraduate programs at the University of Colorado Boulder. In addition to engaging students in the research, the project conducts workshops to help students develop writing and presentation skills to ensure their future success in academia as well as industry.

Differential Equations and hybrid system models are exceedingly common across science and engineering applications. However, inference of these models from data is quite challenging. The project develops rigorously verified model transformation methods, including projection operators to remove latent/unobservable state variables, the use of approximate solutions, and the reduction of the complexity of inference by guessing the correlation between posterior parameters.

These transformations are formalized and verified using theorem-proving approaches to avoid errors that can often be catastrophic in the context of safety-critical systems. The project develops an integrated programming model and formal methods that will allow the expression of probabilistic models and their transformation in a provably safe manner.

The approach is being applied to challenging inference problems involving models and datasets from domains such as modeling epidemics and estimating the impact of public policy decisions on the parameters that affect their spread, developing personalized models for people with type-1 diabetes, and modeling driving strategies for testing autonomous vehicles.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.