We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates.

Authors: Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel

1. The first paper is Auditable Algorithms for Approximate Model Counting

Authors: S. Akshay, Supratik Chakraborty and Kuldeep S. Meel

2. The second paper is An Approximate Skolem Function Counter

Authors: Arijit Shaw, Brendan Juba and Kuldeep S. Meel

3. The third paper is Exact ASP Counting with Compact Encodings

Authors: Mohimenul Kabir, Supratik Chakraborty and Kuldeep S. Meel

4. The fourth paper is Testing Self-Reducible Samplers

Authors: Rishiraj Bhattacharyya, Sourav Chakraborty, Yash Pote, Uddalok Sarkar and Sayantan Sen

5. The fifth paper is Engineering an Exact Pseudo-Boolean Model Counter

Authors: Suwei Yang and Kuldeep S. Meel

In this tutorial, we address three questions on bias in machine learning: (i) Choosing a compatible fairness metric based on application context, (ii) Formally quantifying fairness with respect to the compatible metric, and (iii) Explaining the sources of unfairness corresponding to the metric.

We show how reducing an NP-hard problem to a problem in the second order of the polynomial hierarchy helps us to exponentially decrease the encoding size. By leveraging modern solvers that solve problems beyond NP, we can solve much larger problem instances than the former state of the art.

If you are attending IJCAI in Macau, please come to our talk on

Authors: Anna L.D. Latour, Arunabha Sen, Kuldeep S. Meel

We round the approximate count of ApproxMC, which allows us to achieve 4$\times$ speedup over the state of the art.

Authors: Jiong Yang and Kuldeep S. Meel

We extend the first-order model counting algorithm ForcLift with new compilation rules, enabling it to discover recursive solutions to previously-unsolved instances.

Authors: Paulius Dilkas, Vaishak Belle

We combine explainability with fairness in machine learning, where we compute the influence of individual features and the intersectional effect of multiple features on the resulting bias of a classifier on a dataset. This allows us to have a higher granular depiction of sources of bias than earlier methods.

We introduce a random model and use it to discover some critical differences among weighted model counting algorithms.

Authors: Paulius Dilkas

We present an approach that combines advances in machine learning with automated reasoning for efficiently synthesizing functions with explicit dependencies.

Authors: Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel

Authors: Yash Pote and Kuldeep S. Meel

We show that we can identify a set of variables, called

Authors: Jiong Yang, Supratik Chakraborty, and Kuldeep S. Meel

We propose the first efficient algorithmic technique to estimate the Shannon entropy of a specification with PAC-style guarantees, i.e., the computed estimate is guaranteed to lie within a (1 ± ε)-factor of the ground truth with confidence at least 1−δ.

Authors: Priyanka Golia, Brendan Juba, Kuldeep S. Meel

We design a computational hardness-based tester, called ScalBarbarik that provides a qunatitative way to analysis the quality of a sampler.

Authors: Mate Soos, Priyanka Golia, Sourav Chakraborty, Kuldeep S. Meel

Authors: Bishwamittra Ghosh, Dmitry Malioutov and Kuldeep S. Meel

Authors: Eduard Baranov, Sourav Chakraborty, Axel Legay, Kuldeep S. Meel, and N.V. Vinodchandran

1. The first paper is on Algorithmic Fairness Verification with Graphical Models.

Authors: Bishwamittra Ghosh, Debabrota Basu and Kuldeep S. Meel

2. The second paper is ApproxASP - A Scalable Approximate Answer Set Counter.

Authors: Mohimenul Kabir , Flavio Everardo, Ankit Shukla, Johannes K. Fichte, Markus Hecher and Kuldeep Meel

3. The third paper is on Constraint-Driven Explanations for Black Box ML Models.

Authors: Aditya Shrotri, Nina Narodytska, Alexey Ignatiev, Joao Marques-Silva, Kuldeep S. Meel and Moshe Vardi

Authors: Yash Pote and Kuldeep S. Meel

Authors: Jiong Yang and Kuldeep S. Meel

The work addresses scalability barriers faced by the current state-of-the-art synthesis techniques. We propose four algorithmic improvements for a data-driven framework for functional synthesis.

Authors: Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, Kuldeep S. Meel

Our Sampler not only passes the tests of Barbarik but also leads to significant performance improvements for real-world instances.

Authors: Priyanka Golia, Mate Soos, Sourav Chakraborty, Kuldeep S. Meel

Authors: Mate Soos and Kuldeep S. Meel

Authors: Nicolas Prevot, Mate Soos, and Kuldeep S. Meel

We show that theory-constrained synthesis can be reduced DQF(T), i.e., to the problem of finding a witness of a dependency quantified formula modulo theory.

Authors: Priyanka Golia, Subhajit Roy, Kuldeep S. Meel

Authors: Jaroslav Bendik and Kuldeep S. Meel

This paper presents a survey of 17 partition function estimation techniques and a rigorous empirical study of their behavior across an extensive set of benchmarks.

Authors: Durgesh Agrawal, Yash Pote, and Kuldeep S. Meel

Authors: Kuldeep S. Meel, N.V.Vinodchandran, and Sourav Chakraborty

Authors: Gilles Pesant, Kuldeep S. Meel, and Mahshid Mohammadalitajrishi

We give a sampling-based approach for quantifying properties for deep neural networks and an attack-agnostic metric called adversarial hardness to capture a model's robustness.

Authors: Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel and Prateek Saxena

1. The first paper focuses on efficient distance approximation in high dimension distributions. We propose an amazingly simple method that can compute L1 distance with rigorous guarantees. Come Poster Session 5 on Thursday.

Joint work with A. Bhattacharya, S. Gayen, and N.V. Vinodchandran

2. The second paper provides the first scalable method to test samplers in practice. Barbarik can now test samplers that sample from log-linear models. If you propose a sampling technique but can't prove its correctness, you can now use Barbarik to check its quality. Just the way we use testing for our software. (Poster)

Joint work with S. Chakraborty and Y. Pote

3. The third paper seeks to tame discrete integration with the boon of dimensionality (Yes, the boon not the curse). We extended our IJCAI-15's work of weighted to unweighted counting (thereby increasing the dimensionality) to handle rational weights. (Poster)

Joint work with J.M. Dudek and D. Fried

1. Justicia: A Stochastic SAT Approach to Formally Verify Fairness

Authors: Bishwamittra Ghosh, Debabrota Basu, and Kuldeep S Meel

2. Predicting Forest Fire Using Remote Sensing Data And Machine Learning

Authors: Suwei Yang, Massimo Lupascu, and Kuldeep S Meel

3. Symmetric Component Caching for Model Counting on Structured Instances

Authors: Timothy van Bremen, Vincent Derkinderen, Shubham Sharma, Subhajit Roy, and Kuldeep S Meel

4. Counting Maximal Satisfiable Subsets

Authors: Jaroslav Bendik and Kuldeep S. Meel

5. The Power of Literal Equivalence in Model Counting

Authors: Yong Lai, Kuldeep S Meel, and Roland Yap

1. The first paper on On Testing of Samplers.

Authors: Kuldeep S Meel, Yash Pralhad Pote and Sourav Chakraborty

2. The second paper on Taming Discrete Integration via the Boon of Dimensionality.

Authors: Jeffrey M. Dudek, Dror Fried and Kuldeep S. Meel

3. The third paper on Efficient Distance Approximation for Structured High-Dimensional Distributions via Learning.

Authors: Arnab Bhattacharyya, Sutanu Gayen, Kuldeep S. Meel and N. V. Vinodchandran

Authors: Arnab Bhattacharyya, Kuldeep Meel, A. Pavan and N.V. Vinodchandran

1. The first paper builds on our CNF-XOR solving paradigm (BIRD) and as a result, the new versions of ApproxMC and UniGen are faster than ever.

2. The second paper proposes the first algorithm for approximate MUS counting.

3. The third one proposes a data-driven approach for Boolean functional synthesis, which works at the intersection of constrained sampling, machine learning and automated reasoning.

Authors: Rahul Gupta, Subhajit Roy and Kuldeep S. Meel

1. The first paper shows that the currently known bounds for sparse hashing are too weak to be used for algorithms such as ApproxMC. Authors: Durgesh Agarwal, Bhavishya and Kuldeep S. Meel

2. The second paper 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. Authors: Arijit Shaw and Kuldeep S. Meel

One of the reviews: “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.”

The paper formalizes Induction Models on N extending the classical work of Henkin. Authors: A Dileep, Kuldeep S. Meel and Ammar F. Sabili

1. The first paper proposes a new approach that combines sampling+machine learning+MaxSAT to achieve a significant progress in solving Boolean Functional Synthesis. Authors: Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel

2. The second paper builds on our CNF-XOR solving paradigm (BIRD) and as a result, the new versions of ApproxMC and UniGen are faster than ever. Stay tuned for our releases. Authors: Mate Soos, Stephan Gocht, and Kuldeep S. Meel

3. The third paper proposes the first algorithm for approximate MUS counting. Authors: Jaroslav Bendik and Kuldeep S. Meel

We propose a new attack agnostic metric adversarial hardness to capture the model's robustness: https://arxiv.org/pdf/2002.06864.pdf Authors: Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel and Prateek Saxena.

Our paper on Symmetry breaking and model counting is accepted to TACAS 2020. Authors: Wenxi Wang, Muhammad Usman, Alyas Almaawi, Kaiyuan Wang, Kuldeep S. Meel, and Sarfraz Khurshid

Two of our group's papers are accepted to accepted as poster presentations with a spotlight talk at StarAI 2020 workshop in AAAI 2020: Our AIES-19 paper on incremental classification rule learning and our CCS-19 paper on quantiatative verification for binarized neural networks.

Our paper on MaxSAT-based formulation for group testing is accepted in AAAI 2020. Authors: Lorenzo Ciampiconi, Bishwamittra Ghosh, Jonathan Scarlett and Kuldeep S. Meel

Alexis will be presenting our work on unifying hashing-based approaches for discrete integration, and Bishwa will present on learning interpretable classifiers at CP2019.

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

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.

We have released the source code of GANAK.

Our NPAQ framework focused on providing PAC guarantees for verification of Neural Networks is accepted to CCS-19 Quoting reviewer: “This work is pioneering a new technique to solve an incredibly challenging problem, and it shows that smaller problem can be solved. I can live with that, future work can improve computational efficiency.” Authors: Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, Prateek Saxena

Our paper on interpretable rules expressed as relaxed-CNF is accepted at IJCAI workshop on XAI (Explainable Artificial Intelligence) and DSO (Data Science meets Optimization), 2019. Authors: Bishwamittra Ghosh, Dmitry Malioutov, Kuldeep S. Meel.

Kuldeep recieved notification of the award of NRF Fellowship for AI for the project: Provably Verified and Explainable Probabilistic Reasoning.

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.

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.

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 Bombay.

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. Vardi.

Our paper on weighted and projected sampling is accepted at TACAS 2019. Authors: Shubham Sharma, Rahul Gupta, Subhajit Roy and Kuldeep S. Meel.

© 2019–2024

Powered by the Academic theme for Hugo.