1st Workshop on Probabilistic Reasoning and Formal Methods
Dec 11, 2017
IIT Kanpur
Co-located with FSTTCS 2017
Dec 11, 2017
IIT Kanpur
Co-located with FSTTCS 2017
(Please scroll down to see the abstracts)
9:00 -- 9:15 Opening Remarks
9:15 -- 10:45 Prof. Adnan Darwiche
On the Role of Logic in Probabilistic Inference and Machine Learning [Slides] [Video]
10:45 -- 11:15 Coffee Break
11:15 -- 12:30 Prof. Mahesh Viswanathan
Probabilistic Automata on Finite and Infinite Words [Slides]
12:30 -- 14:00 Lunch
14:00 -- 15:30 Prof. Joost-Pieter Katoen
Bayesian Network Analysis by Program Verification [Slides]
15:30 -- 15:55 Coffee Break
15:55 -- 16:55 Prof. Rüdiger Ehlers
Computing Control Policies for Enforcing Omega-regular Control Objectives in MDPs: A Non-classical Perspective [Slides]
17:00 -- 18:00 Panel Discussion (Moderator: Prof. Orna Kupferman)
Speaker: Prof. Adnan Darwiche
Abstract:
I will discuss in this tutorial some fundamental roles of logic in probabilistic inference and machine learning. In particular, I will discuss four key probabilistic queries that are complete for the complexity classes NP, PP, NP^PP and PP^PP, showing how each of these queries can be reduced to logical manipulations. The treatment of these queries will be systematic and based on compiling corresponding problems into Boolean circuits with increasingly strong properties that guarantee linear-time probabilistic inference. I will also link the proposed approach to the recent “Beyond NP” initiative that calls for a similar systematic treatment when handling computational problems that are harder than NP. On the machine learning front, I will show how the proposed approach can be used to: (a) learn statistical models from a combination of data and background knowledge (expressed using logical constraints); (b) learn from a new class of more expressive datasets; and (c) estimate parameters in closed-form in some cases. The tutorial will include a number of case studies and experimental results, showing the broad scope and competitiveness of the proposed techniques, while also highlighting situations where they are now the state of the art.
Bio:
Adnan Darwiche is a professor and chairman of the computer science department at UCLA. He earned his PhD and MSc degrees in computer science from Stanford University in 1993 and 1989, respectively. His research focuses on the theory and practice of symbolic and probabilistic reasoning, with applications to machine learning. Professor Darwiche served as editor-in-chief of the Journal of Artificial Intelligence Research (JAIR) and is a AAAI fellow. He is also author of “Modeling and Reasoning with Bayesian Networks”, published by Cambridge University Press in 2009.
Speaker: Prof. Mahesh Viswanathan
Abstract:
Probabilistic automata are finite state machines that roll dice in each step to decide the next state on reading an input symbol. Such machines were first introduced by Rabin in the 1960s as a computational model on finite words, and, more recently, the theory has been extended to consider infinite length inputs. This talk will survey results about such machines, contrasting it with the theory of regular languages, and discuss open problems and applications to model checking.
Results presented will include joint work with Rohit Chadha, Dileep Kini, and Prasad Sistla.
Bio:
Mahesh Viswanathan obtained his bachelor's degree in computer science from the Indian Institute of Technology at Kanpur, and his doctorate from the University of Pennsylvania. He was a post-doctoral fellow at DIMACS with a joint appointment with Telcordia Technologies in 2000-01. Since 2001, he has been on the faculty at the University of Illinois at Urbana-Champaign. His research interests are in the core areas of logic, automata theory, and algorithm design, with applications to the algorithmic verification of cyber-physical and stochastic systems.
Speaker: Prof. Joost-Pieter Katoen
Abstract:
I will introduce a weakest preconditioning-style reasoning framework for probabilistic programs. This can be used for correctness analysis as well as the analysis of run times. I will show that wp-reasoning of probabilistic programs corresponding to (discrete) Bayesian networks equals exact Bayesian reasoning. I will discuss how run-time analysis by formal verification can be used to analyse the expected simulation time of Bayesian networks. If time permits, I'll show how randomised algorithms can be analysed as well.
Bio:
Joost-Pieter Katoen is professor at the RWTH Aachen University, Germany and holds a part-time professorship at the University of Twente, the Netherlands. His research interests include formal methods, model checking, concurrency theory, and probabilistic computation. Prof. Katoen is member of the steering committee of ETAPS (chair), CONCUR, QEST, and FORMATS. He received a honorary doctorate degree from Aalborg University, Denmark and is member of Academia Europea.
Speaker: Prof. Rüdiger Ehlers
Abstract:
Computing control policies (also called schedulers) that enforce omega-regular
specifications to hold along the executions of a Markov Decision Process (MDP) with the highest possible probability is a well-studied problem in both control theory and formal methods. The problem can be solved efficiently if the MDP is given in explicit form and the specification is represented as a deterministic automaton. MDPs are a natural model for many real-world systems that have probabilistic components or for which the environment is non-antagonistic and the likelihood of environment actions can be abstracted probabilistically.
Despite this success, classical MDP control against omega-regular specifications is often inapplicable in practical setups. Only in some cases, complete information about the probabilities and the costs/pay-offs of actions is available, so that no optimal control policy can be computed upfront. Furthermore, in many settings, almost-sure eventual violation of the specification cannot be avoided, so that all control policies are equally bad. Still, engineers write good control policies for these cases by hand, and there should be a way to do so automatically.
This talk gives an overview of some recent ideas to solve such obstacles to applying formal methods for probabilistic systems in practice. To account for a partially unknown environment, we show how reinforcement learning can be combined with correct-by-construction controller computation. Reinforcement learning has been shown to be useful for letting a control policy adapt to unknown (or gradually changing) environment conditions at runtime, and we present two approaches to make use of its strengths while ensuring that a given temporal specification is (surely) satisfied. For settings in which no control policy can avoid the almost-sure eventual violation of the specification, we give an alternative definition of the control objective. It coincides with the classical control objective for non-probabilistic environments, and we show experimentally that it faithfully models the intuitive aim of letting the controller work towards the satisfaction of the specification as well and as long as possible.
The talk is based on joint work with Min Wen, Ufuk Topcu, Bettina Koenighofer, Mohammed Alshiekh, Roderick Bloem, Scott Niekum, and Salar Moarref.
Bio:
Ruediger Ehlers is a Junior Research Group Leader at the University of Bremen since 2014, cooperating with the German Research Center for Artificial Intelligence (DFKI). He received a Diploma in Computer Science from the Technical University of Dortmund, an M.Sc. in Mathematics & the Foundations of Computer Science from the University of Oxford, UK, and a Dr. in Computer Science from Saarland University, Germany. He was shared researcher between the University of California at Berkeley and Cornell University, USA, from 2012-2013, and a postdoc at the University of Kassel, Germany, from 2013 to 2014.
His research deals with synthesizing and verifying cyber-physical systems, including efficient symbolic reasoning engines and the combination of formal methods with artificial intelligence.