Welcome to the Meel Group’s web page. We are situated at National University of Singapore.
Broadly, our research group is focused on the development of a rigorous mathematical framework for provably verified, correct-by-construction, explainable probabilistic reasoning systems building on recent breakthroughs in formal methods and symbolic reasoning; and deployment of our algorithmic framework in the real world including applications in reliability estimation of critical infrastructure and computational sustainability. On a more technical level, we work at the intersection of formal methods and artificial intelligence. We seek to develop formal methods for AI techniques and also employ advances in AI techniques for development of formal method algorithmic and system frameworks.
This research theme is motivated by two observations:
O1 necessitates design of solvers that can exploit the rich structures of queries without losing the generality offered by CNF. Our recent work has proposed new paradigms for CNF+XOR constraints [aaai19] and CNF+ANF constraints [date19].
A consequence of O2 is that the development of new algorithmic insights has been largely restricted to expert intuitions and evaluation of the new insights have been restricted to performance measurement in terms of the runtime of solvers or a proxy for the runtime of solvers. In this project, our focus is to enable data-driven design and understanding of SAT Solvers. In particular, we view modern conflict-driven clause learning (CDCL) solvers as a composition of classifiers and regressors for different tasks such as branching, clause memory management, and restarting. We will employ supervised learning and uses extensive, multi-gigabyte data extracted from runs of a single SAT solver to perform predictive analytics. Our [SAT-19] paper presents the first version of the system, called CrystalBall, that we are building.
Constrained sampling and counting are two fundamental problems in data analysis. In constrained sampling the task is to sample randomly, subject to a given weighting function, from the set of solutions to a set of given constraints. This problem has numerous applications, including probabilistic reasoning, machine learning, statistical physics, and constrained-random verification. A related problem is that of constrained counting, where the task is to count the total weight, subject to a given weighting function, of the set of solutions of the given constraints. This problem has applications in machine learning, probabilistic reasoning, and planning, among other areas. Both problems can be viewed as aspects of one of the most fundamental problems in artificial intelligence, which is to understand the structure of the solution space of a given set of constraints. This work focuses on the development of new algorithmic techniques for constrained sampling and counting, based on a universal hashing – a classical algorithmic technique in theoretical computer science. Many of the ideas underlying the proposed approach were go back to the 1980s, but they have never been reduced to practice. Recent progress in Boolean reasoning is enabling us to reduce these algorithmic ideas to practice, and obtain breakthrough results in constrained sampling and counting, providing a new algorithmic toolbox in design verification, machine learning, probabilistic reasoning, and the like.
We are focused on
The unprecedented advances in the machine learning techniques have led to a proliferation of Artificial Intelligence(AI)-based devices in our day to day life. The AI-based tools are increasingly employed to make consequential decisions for human subjects, in areas such as credit lending, policing, criminal justice, and medicine. Decisions made by these AI-based predictive models often have a long-lasting impact on people’s lives. As such there is a strong need for the development of methodology for verification of AI systems.
The modern AI systems significantly differ from traditional systems in their reliance on probabilistic reasoning. Often statistical tests are employed to argue for the accuracy/robustness of these systems, but such statistical tests are usually performed on a tiny number of samples for which no theoretical guarantees exist for their accuracy. In contrast to testing for traditional hardware and software systems, where one trace is sufficient to prove the existence of a bug; such is not the case for samplers as one sample is typically not sufficient to prove non-conformity of the underlying systems.
Interpretability has become a central thread in ML research. As ML algorithms continue to permeate critical application domains such as medicine, legal, and transportation, it becomes increasingly important to allow human domain experts to understand and interact with ML solutions. Providing meaningful explanations for automated decisions is an increasingly important task. In this research theme, we are investigating techniques for two categories of explanations:
Kuldeep recieved notification of the award of NRF Fellowship for AI for the project: Provably Verified and Explainable Probabilistic Reasoning.9 May 2019
Two papers accepted to IJCAI.The first paper explores the phase transition behavior of conjunction of cardinality and XOR constraints. Authors: Yash Pote, Saurabh Joshi, Kuldeep Meel.
The second paper describes a radically new approach to exact counting wherein we compute estimates that are probabilistically exact! Authors: Shubham Sharma, Kuldeep Meel. Combined with our invited paper on #DNF , this makes 3 papers that we will be presenting at IJCAI
Two papers accepted to SAT 2019. The first paper introduces the first version of CrystalBall, a framework intended to allow gazing into the black box of SAT solving. Authors: Kuldeep, Mate Soos, Raghav Kulkarni.
The second paper discusses how model counting can be used to analyze explanations provided by tools such as ANCHOR. Authors: Kuldeep, Nina Narodytska, Aditya Shrotri, Alexey Ignatiev, and Joao Marques Silva
Kuldeep is appointed Visiting Assistant Professor in the Department of Computer Science and Engineering at IIT Bombay2 February 2019
Paper on network reliability is accepted to The 13th International Conference on Applications of Statistics and Probability in Civil Engineering Authors: Roger Paredes, Leonardo Duenas-Osorio, Kuldeep S. Meel, and Moshe Y. Vardi26 January 2019
Our paper on weighted and projected sampling is accepted at TACAS 2019. Authors: Shubham Sharma, Rahul Gupta,Subhajit Roy and Kuldeep S. Meel
We are always looking for highly motivated Ph.D. students, research assistants and summer internship for exceptional undergraduate interns in our group. We work at the intersection of algorithmic design and systems; therefore, an ideal candidate should have deeper expertise in one area and willingness to learn the other. A strong background in statistics, algorithms/formal methods and prior experience in coding is crucial to make a significant contribution to our research.