Research

Overview

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.

At 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 the development of formal method algorithmic and system frameworks.

Theme 1: Revisiting NP Revolution: New Paradigms for SAT/SMT/MaxSAT Solvers

Two observations motivate this research theme:

O1: The success of SAT/SMT/MaxSAT solvers has allowed researchers to employ them as “oracles” inside larger algorithmic components, which give rise to rich structure in the queries to the SAT solvers, and

O2: Modern SAT/SMT solvers achieve scalability and robustness with sophisticated heuristics that are challenging to understand and explain.

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.

Theme 2: Constrained Sampling and Integration/Counting

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 while for constrained counting, the task is to count the total weight, subject to a given weighting function, of the set of solutions of the given constraints. Both of these problems have applications in machine learning, probabilistic reasoning, planning, hardware, and software testing, among other areas.

Our focus in on the development of new algorithmic techniques for constrained sampling and counting, combining the classical technique of universal hashing with advances in Boolean reasoning. 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

  1. Algorithmic advances in sampling and counting [aaai19].
  2. Application of sampling and counting to problems arising in different domains [sat19] [vmcai19].
  3. Revisiting theoretical foundations in light of existence of solvers but not oracles.

Theme 3: 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. Our recent work [aaai19] showcased, to the best of our knowledge, the first algorithmic framework, Barbarik, to test whether the distribution generated is close to the uniform distribution.

Theme 4: Interpretable and Actionable Explanations for AI 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:

  1. Interpretable explanations such as those specified using a small set of rules/formulas. In particular, we have designed a MaxSAT based formulation for learning interpretable rules in CNF/DNF [cp18] and later extended this formulation by incorporating incremental learning of small rules [aies19].

  2. In settings where the cognitive burden of complete explanations is too high, people often do not seek to know why a particular event happened, but rather why an alternative one didn’t. Due to the heuristic nature of explanations produced by existing tools, it is necessary to validate them, and our approach applies the development in formal methods to aid validation. As an example, our recent work [sat19] proposed a counting-based method to assess the quality of explanations rigorously.

Publications

More Publications

. Embedding Symbolic Knowledge into Deep Networks . In Advances in Neural Information Processing Systems(NeurIPS), 2019.

PDF Code

. Quantitative Verification of Neural Networks And its Security Applications . ACM Conference on Computer and Communications Security (CCS)., 2019.

PDF Code

. Dual Hashing-based Algorithms for Discrete Integration . In Proceedings of International Conference on Constraint Programming (CP), 2019.

PDF

. Interpretable Classification Rules in Relaxed Logical Form . In IJCAI workshop on XAI (Explainable Artificial Intelligence) and DSO (Data Science meets Optimization), 2019.

PDF Code Slides

. Network Reliability Estimation in Theory and Practice . Journal of Reliability Engineering and System Safety(RESS), 2019.

PDF

Sep 30, 2019
Alexis will be presenting our work on unifying hashing-based approaches for discrete integration, and Bishwa will present on learning interpretable classifiers at CP2019.
Sep 1, 2019
Our Paper on embedding symbolic knowledge into Neural Networks is accepted to NeurIPS 2019.” Authors: Yaqi Xie, Ziwei Xu, Mohan S. Kankanhalli, Kuldeep S. Meel, Harold Soh
Aug 13, 2019
We presented three papers at IJCAI-19. 1) The first paper explores the phase transition behavior of conjunction of cardinality and XOR constraints. 2) The second paper describes a radically new approach to exact counting wherein we compute estimates that are probabilistically exact! 3) The third one is our invited paper on #DNF.
Aug 12, 2019
We have released the source code of GANAK.

Software

ApproxMC

A hashing-based algorithm for discrete integration over finite domains.

CrystalBall

A framework to provide white-box access to the execution of SAT solver.

UniGen

An algorithm to generate uniform samples subject to given set of constraints.

GANAK

GANAK: A Scalable Probabilistic Exact Model Counter

WAPS

WAPS: Weighted and Projected Sampling

Bosphorus

An ANF and CNF simplifier and converter.

KUS

Knowledge Compilation meets Uniform Sampling

MIS

An algorithm to compute minimal independent support for a given CNF formula.

SMTApproxMC

An approximate model counter for Bitvector theory.

WeightGen

A hashing-based approximate sampler for weighted CNF formulas.

WeightMC

A weighted model counter over Boolean domains.

People

Faculty

Kuldeep Kuldeep Meel

Postdoctoral Researchers

Yong Yong Lai

PhD Students

Masters Students

Rémi Rémi Delannoy

Research Interns

Alumni

Mahi Mohimenul Kabir
Himanshu Himanshu Arora
Alexis Alexis de Colnet
Andre Andre
Kurt Kurt Warren

Past visitors

2019

2018

Openings

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.

Application Procedure:

  • If you are a student at NUS, feel free to drop by Kuldeep’s office or schedule a meeting with him. (See his calendar).
  • Post-doc position: We have multiple post-doc positions available. Read advertisement for more details about the positions and application procedure.

  • Internship (>=6 months): We strongly prefer candidates who want to use their internship as a way to apply for PhD programs (@NUS or elsewhere; of course, if you are good, we would like you to remain at NUS). Email meel+interns@comp.nus.edu.sg with a PDF of your CV. Make sure your subject contains the word “olleh” and you should include reviews of two of the papers published in the previous 3 years at AAAI/IJCAI/CP/SAT/CAV conferences. The reviews should be in the body of the email (and not as pdf). Furthermore, the body of your email should contain the phrase: “Here are two papers that I have reviewed”. You should also provide reason for your choice of the papers.
  • Short term internship (=3 months): We may offer short term internship to exceptional undergraduates. Same process as above.
  • PhD positions: Admissions to School of Computing@NUS are handled via a central admission procedure: You can either apply via Department of Computer Science or the Institute of Data Science.
  • NUS and Singapore

    NUS is a world-class university that provides an outstanding and supportive research environment. Its School of Computing is highly ranked (within the top 15) among the computer science departments in the world. Singapore is a vibrant, well-connected city with low taxes and research hub in Asia.