## Short Bio

Kuldeep Meel is Sung Kah Kay Assistant Professor in the Computer Science Department of School of Computing at National University of Singapore. He is an affiliate at Institute of Data Science and also holds a long-term visiting appointment at Computer Science Department of IIT Bombay.

His research interests are at the intersection of artificial intelligence and formal methods, which also lies at the intersection of theory and practice. His group strongly believes (and acts upon the beliefs) in developing mathematical frameworks whose faithful implementations can handle practical applications. He is also a receipient of 2019 NRF Fellowship for AI.

### Open Positions

• Multiple post-doc positions available in the project "Provably Verified and Explainable Probabilistic Reasoning". Read advertisement for more details.
• One post-doc position (jointly advised with Prof. Roland Yap) available in the broad area of applying machine learning to SAT solvers, approximate counting techniques, and CP. Read advertisement for more details.
• Research Assistant position available for inter-disciplinary project on computational Sustainability (jointed advised with Massimo Lupascu from Department of Geography). Read advertisement for more details.
• We are always looking for highly motivated Ph.D. students, research assistants with time commitment of at least 6 months and summer internship for exceptional undergraduate interns in our group.
• Read this before sending me an email.

[top]

## Research Interests

Some of the recent papers are linked below. Full list of publications is available here

[top]

## Students & Postdocs

I am proud of my highly motivated students and postdocs:

### Alumni

• Dr. Mate Soos, Senior Research Fellow (Jul -- Sep 2019; Mar -- June 2018)

• Alexis de Colnet, MComp@NUS (Graduated: Dec 2018); now a PhD student at Centre de Recherche en Informatique de Lens
• Rahul Gupta, BTech+MTech@IITK (Graduated: June 2019) , co-advised with Subhajit Roy (IITK)
• Shubham Sharma, BTech+MTech@IITK (Graduated: May 2019), co-advised with Subhajit Roy (IITK)
• Delannoy Remi Christian, MComp@NUS, (Graduated: Dec 2019)
• Lorenzo Ciampiconi, MS@Politecnico di Milano (Graduated: Dec 2019)

• Bhavishya, Summer Intern (May 2018 - July 2018)
• Mohimenul Kabir, Research Intern (September 2018 - July 2018)
• Do Andre Khoi Nguyen, Undergraduate Researcher (May 2018 -- Apr 2019)
• Himanshu Arora, Research Intern (Feb 2019 -- July 2019)
• Durgesh Agrawal, Summer Intern (May 2019 -- July 2019)
• Kurt Warren, Research Intern (July 2019 - Sep 2019)

[top]

[top]

[top]

## Selected Recent Publications

Except for [1], the names of authors are sorted alphabetically and the order does not reflect contribution.
 1 BIRD: Engineering an Efficient CNF-XOR SAT Solver and its Applications to Approximate Model Counting Mate Soos and Kuldeep S. Meel Proceedings of AAAI Conference on Artificial Intelligence (AAAI), 2019. Given a Boolean formula F, the problem of model counting, also referred to as #SAT is to compute the number of solutions of F. Model counting is a fundamental problem in artificial intelligence with a wide range of applications including probabilistic reasoning, decision making under uncertainty, quantified information flow, and the like. Motivated by the success of SAT solvers, there has been surge of interest in the design of hashing-based techniques for approximate model counting for the past decade. We profiled the state of the art approximate model counter ApproxMC3 and observed that over 99.99% of time is consumed by the underlying SAT solver, CryptoMinisat. This observation motivated us to ask: Can we design an efficient underlying CNF-XOR SAT solver that can take advantage of the structure of hashing-based algorithms and would this lead to an efficient approximate model counter? The primary contribution of this paper is an affirmative answer to the above question. We present a novel architecture, called BIRD, to handle CNF-XOR formulas arising from hashing-based techniques. The resulting hashing-based approximate model counter, called ApproxMC3, employs the BIRD framework in its underlying SAT solver, CryptoMinisat. To the best of our knowledge, we conducted the most comprehensive study of evaluation performance of counting algorithms involving 1896 benchmarks with computational effort totaling 86400 computational hours. Our experimental evaluation demonstrates significant runtime performance improvement for ApproxMC3 over ApproMC2. In particular, we solve 648 benchmarks more than ApproMC2, the state of the art approximate model counter and for all the formulas where both ApproMC2 and ApproxMC3 did not timeout and took more than 1 seconds, the mean speedup is 284.40 -- more than two orders of magnitude. 2 Embedding Symbolic Knowledge into Deep Networks Yaqi Xie, Ziwei Xu, Mohan S. Kankanhalli, Kuldeep S. Meel, and Harold Soh Advances in Neural Information Processing Systems(NeurIPS), 2019. In this work, we aim to leverage prior symbolic knowledge to improve the performance of deep models. We propose a graph embedding network that projects propositional formulae (and assignments) onto a manifold via an augmented Graph Convolutional Network (GCN). To generate semantically-faithful embeddings, we develop techniques to recognize node heterogeneity, and semantic regularization that incorporate structural constraints into the embedding. Experiments show that our approach improves the performance of models trained to perform entailment checking and visual relation prediction. Interestingly, we observe a connection between the tractability of the propositional theory representation and the ease of embedding. Future exploration of this connection may elucidate the relationship between knowledge compilation and vector representation learning. 3 Quantitative Verification of Neural Networks And its Security Applications Teodora Baluta, Shiqi Shen, Shweta Shine, Kuldeep S. Meel, and Prateek Saxena ACM Conference on Computer and Communications Security (CCS), 2019. Neural networks are increasingly employed in safety-critical domains. This has prompted interest in verifying or certifying logically encoded properties of neural networks. Prior work has largely focused on checking existential properties, wherein the goal is to check whether there exists any input that violates a given property of interest. However, neural network training is a stochastic process, and many questions arising in their analysis require probabilistic and quantitative reasoning, i.e., estimating how many inputs satisfy a given property. To this end, our paper proposes a novel and principled framework to quantitative verification of logical properties specified over neural networks. Our framework is the first to provide PAC-style soundness guarantees, in that its quantitative estimates are within a controllable and bounded error from the true count. We instantiate our algorithmic framework by building a prototype tool called NPAQ that enables checking rich properties over binarized neural networks. We show how emerging security analyses can utilize our framework in 3 concrete point applications: quantifying robustness to adversarial inputs, efficacy of trojan attacks, and fairness/bias of given neural networks. 4 On testing of Uniform Samplers Sourav Chakraborty and Kuldeep S. Meel Proceedings of AAAI Conference on Artificial Intelligence (AAAI), 2019. Recent years have seen an unprecedented adoption of artificial intelligence in wide variety of applications ranging from medical diagnosis, automobile, security to aircraft collision avoidance. Probabilistic reasoning is a key component of such modern artificial intelligence systems. Sampling techniques form the core of the state of the art probabilistic reasoning systems. In contrast to testing for deterministic programs, 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 sampler to the desired distribution. This makes one wonder: whether it is possible to design testing methodology to test whether a sampler under test generates samples close to a given distribution. The primary contribution of this paper is a positive answer to the above question: We design, to the best of our knowledge, the first algorithmic framework, Barbarik, to test whether the distribution generated by $\varepsilon-$close or $\eta-$far from the uniform distribution. In contrast to the sampling techniques that require an exponential or sub-exponential number of samples for sampler whose support can be represented by $n$ bits, Barbarik requires only $\mathcal{O}(1/(\eta-\varepsilon)^2)$ samples. We present a prototype implementation of Barbarik and use it to test three state of the art uniform samplers over the support defined by combinatorial constraints. Barbarik is able to provide a certificate of uniformity to one sampler and demonstrate non-uniformity for the other two samplers. 5 On Computing Minimal Independent Support and Its Applications to Sampling and Counting Alexander Ivrii, Sharad Malik, Kuldeep S. Meel, and Moshe Y. Vardi Proceedings of International Conference on Constraint Programming (CP), 2015. Best Student Paper Award Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions for these problems rely on employing SAT solvers and universal hash functions that are typically encoded as XOR constraints of length n/2 for an input formula with n variables. As the runtime performance of SAT solvers heavily depends on the length of XOR constraints, recent research effort has been focused on reduction of length of XOR constraints. Consequently, a notion of Independent Support was proposed, and it was shown that constructing XORs over independent support (if known) can lead to a significant reduction in the length of XOR constraints without losing the theoretical guarantees of sampling and counting algorithms. In this paper, we present the first algorithmic procedure (and a corresponding tool, called MIS) to determine minimal independent support for a given CNF formula by employing a reduction to group minimal unsatisfiable subsets (GMUS). By utilizing minimal independent supports computed by MIS, we provide new tighter bounds on the length of XOR constraints for constrained counting and sampling. Furthermore, the universal hash functions constructed from independent supports computed by MIS provide two to three orders of magnitude performance improvement in state-of-the-art constrained sampling and counting tools, while still retaining theoretical guarantees.

[top]

## Service

• Co-organizer:
• Committee Member: The Committee on Probability and Statistics in the Physical Sciences, C(PS)^2 (2018-20)
• Program Committee: SAT 2020, CAV 2020, IJCAI 2020, ECAI 2020, CONCUR 2020, AAAI 2020, IJCAI 2019, SAT 2019,AAAI 2019, AIES 2019, ISAAC 2019, CoDS-COMAD 2019, IJCAI 2018, AAAI 2018, CP 2018, FAW 2018, CP 2017, CAV-16 Artifact Evaluation
• Awarded Distinguished Program Committee Member for IJCAI 2018.
• Reviewer: Artificial Intelligence, JAIR, CACM (2014, 2018), ACM TOPLAS (2017), IJCAR (2018), NFM (2018), SAT (2017, 2016) TACAS 2017, CAV 2015, FoSSaCS 2015, DAC 2014
• Part of 12 member AAAI 2015 Futures Focus Group tasked with creation of vision for AAAI

[top]

## News

• 21 May 2020

Paper (joint work with Eduard Baranov and Axel Legay) “Baital: An Adaptive Weighted Sampling Approach for Improved t-wise Coverage” is accepted to FSE 2020.

• 25 April 2020

Two papers accepted to SAT-2020 Conference.

The first paper (with my amazing interns Durgesh and Bhavishya) shows that the currently known bounds for sparse hashing are too weak to be used for algorithms such as ApproxMC. Our upcoming LICS Paper proposes new constructions for sparse hash functions to overcome this barrier.

The second paper (with my superstar current intern Arijit Shaw) proposes a new phase selection strategy for SAT solvers. Improving SAT solvers is just a very very hard job and we are excited about the improvements that our proposal brings to the world of SAT solving.

• 11 April 2020

Paper (joint work with S. Akshay) on Sparse Hashing for Counting accepted to LICS 2020

And the notification came with the following review: “Rarely it is that there is a paper that proves a beautiful new theoretical result, explaining and simplifying previous work, and on top of that shows how it can be used to improve state-of-the-art practical algorithms. The paper “Sparse hashing for scalable approximate model counting: theory and practice” achieves exactly that. “

• 08 April 2020

Our paper on formalization of Induction Models is accepted to LPAR-23. Co-authors: A Dileep and Ammar F. Sabili

All news…

Recent Profile: Kuldeep Meel: The New CS Professor
Old Profile: Kuldeep Meel: High-Risk, High-Reward Research

[top]

## Recruitment

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. Read here for more details.

[top]