“Kuldeep

Kuldeep S. Meel

NUS Presidential Young Professor
Assistant Professor
School of Computing
National University of Singapore

CV: [pdf] | Research Statement: [pdf]
Teaching: [pdf] | Publications: [html] [pdf]

Research Group
Office: COM2-03-41
Email: meel@comp.nus.edu.sg
Twitter: @ksmeel
Tools: Github
SAT-22 Call for Papers is out!
External: [Scholar] [DBLP]

Recent Talks Nov 5: Northeastern U. |Oct 21: MPI-SP |Oct 19: MSR Summit |Sep 15: MIAO,U. of Cophengan |Apr 19: Oxford | Apr 15: USC | Mar 29: MPI-SWS | Mar 24: University of Wisconsin | Mar 1: UC Berkeley

Kuldeep Meel holds NUS Presidential Young Professorship in the School of Computing at the National University of Singapore. He is a receipient of 2019 NRF Fellowship for AI (accompanied with SGD 2.6 million funding) and was named AI's 10 to Watch by IEEE Intelligent Systems in 2020.

His research interests are at the intersection of formal methods and artificial intelligence. His research program's long-term vision is to advance automated reasoning techniques to enable computing to deal with increasingly uncertain real-world environments. Check out Research Statement for more details.

Our research group is still growing. Check out Open Positions.

External Funding: National Research Foundation, AI Singapore, Grab NUS AI Lab, Microsoft Research Asia, Ministry of Education, Defense Service Organization

Awards and Honors

Research Paper Recognition

Software Recognition

  • Model Counting Competition
    • 2020: 1st place in Model Counting Track and Projected Model Counting Track
    • 2021: 2nd place in Model Counting Track
  • 2nd place in EDA Challenge 2021
  • 3rd place in SAT competition 2020

Students & Postdocs

Learn more at Group Website

Selected Recent Publications

See Google Scholar and All Publications for details.
1
Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice
Kuldeep S. Meel ⓡ S. Akshay
Proceedings of Logic in Computer science (LICS), 2020.
Given a CNF formula F on n variables, the problem of model counting, also referred to as #SAT, is to compute the number of models or satisfying assignments of F. Model counting is a fundamental but hard problem in computer science with varied applications. Recent years have witnessed a surge of effort towards developing efficient algorithmic techniques that combine the classical 2-universal hashing (from [Stockmeyer 1983]) with the remarkable progress in SAT solving over the past decade. These techniques augment the CNF formula F with random XOR constraints and invoke an NP oracle repeatedly on the resultant CNF-XOR formulas. In practice, the NP oracle calls are replaced by calls to a SAT solver and it is observed that runtime performance of modern SAT solvers (based on conflict-driven clause learning) on CNF-XOR formulas is adversely affected by the size of XOR constraints. However, the standard construction of 2-universal hash functions chooses every variable with probability p =1/2 leading to XOR constraints of size n/2 in expectation. Consequently, the main challenge is to design sparse hash functions, where variables can be chosen with smaller probability and lead to smaller sized XOR constraints, which can then replace 2-universal hash functions. In this paper, our goal is to address this challenge both from a theoretical and a practical perspective. First, we formalize a relaxation of universal hashing, called concentrated hashing, a notion implicit in prior works to design sparse hash functions. We then establish a novel and beautiful connection between concentration measures of these hash functions and isoperimetric inequalities on boolean hypercubes. This allows us to obtain tight bounds on variance as well as the dispersion index and show that p = O(log m /m ) suffices for the design of sparse hash functions from 2^n to 2^m belonging to concentrated hash family. Finally, we use sparse hash functions belonging to this concentrated hash family to develop new approximate counting algorithms. A comprehensive experimental evaluation of our algorithm on 1896 benchmarks with computational effort of over 20,000 computational hours demonstrates significant speedup compared to existing approaches. To the best of our knowledge, this work is the first study to demonstrate runtime improvement of approximate model counting algorithms through the usage of sparse hash functions, while still retaining strong theoretical guarantees (a la 2-universal hash functions).
2
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.
3
Manthan: A Data-Driven Approach for Boolean Function Synthesis
Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel
Proceedings of International Conference on Computer-Aided Verification (CAV), 2020.
Boolean functional synthesis is a fundamental problem in computer science with wide-ranging applications and has witnessed a surge of interest resulting in progressively improved techniques over the past decade. Despite intense algorithmic development, a large number of problems remain beyond the reach of the current state of the art techniques. Motivated by the progress in machine learning, we propose Manthan, a novel data-driven approach to Boolean functional synthesis. Manthan views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. Furthermore, Manthan solves 60 benchmarks that none of the current state of the art techniques could solve. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.
4
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.
5
Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls
Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi
Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2016.
Probabilistic inference via model counting has emerged as a scalable technique with strong formal guarantees, thanks to recent advances in hashing-based approximate counting. State-of-the-art hashing-based counting algorithms use an {\NP} oracle, such that the number of oracle invocations grows linearly in the number of variables n in the input constraint. We present a new approach to hashing-based approximate model counting in which the number of oracle invocations grows logarithmically in $n$, while still providing strong theoretical guarantees. Our experiments show that the new approach outperforms state-of-the-art techniques for approximate counting by 1-2 orders of magnitude in running time.

Full list of publications is available here. Please visit Software and Github Repository for the accompanied softwares.

Teaching

  • CS3243: Introduction to Artificial Intelligence (Fall 2020; Fall 2021)
  • CS 4244: Knowledge Representation and Reasoning (Spring 2021; Spring 2020; Spring 2019; Spring 2018)
  • CS 4269/5469: Fundamentals of Logic in Computer Science (Fall 2019)
  • CS 6283: Advanced Topics in Computer Science: Logic in AI (Fall 2018)

Service

Selected Recorded Talks

  • Functional Synthesis: An Ideal Meeting Ground for Formal Methods and Machine Learning [slides] [video](@Wisconsin)
  • Approximate Counting and Sampling [slides] [video] (@Simons Institute)
  • The Rise of Approximate Model Counting: Beyond Classical Theory and Practice of SAT [slides] [video](@Simons Institute)

News

  • 21 December 2021

    Our paper “Efficient Learning of Interpretable Classification Rules” is accepted to JAIR journal. Joint work with Bishwamittra Ghosh and Dmitry Malioutov.

  • 03 December 2021

    Our paper “A Scalable t-wise Coverage Estimator” is accepted to ICSE 2022. Joint work with Eduard Baranov, Sourav Chakraborty, Axel Legay, and N. V. Vinodchandran.

  • 02 December 2021

    Three papers from our group were accepted to AAAI 2022.

    1. Algorithmic Fairness Verification with Graphical Models (Joint work with Bishwamittra Ghosh and Debabrota Basu)

    2. ApproxASP - A Scalable Approximate Answer Set Counter (Joint work with Mohimenul Kabir, Flavio Everardo, Ankit K Shukla, Markus Hecher, and Johannes Fichte)

    3. Constraint-Driven Explanations for Black Box ML Models (Joint work with Aditya Shrotri, Nina Narodytska, Alexey Ignatiev, Joao Marques-Silva, and Moshe Y. Vardi)

  • 30 October 2021

    Our ICCAD-21 paper received Best Paper Award Nomination at ICCAD-21.

All news…

Recent: MeelGroup Wins Model Counting Competition
Profile: Kuldeep Meel: The New CS Professor
Old Profile: Kuldeep Meel: High-Risk, High-Reward Research