News

2021

Our paper on Program Synthesis as Dependency Quantified Formula Modulo Theory has been accepted to IJCAI 2021.
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

2020

Our paper on scalable quantitative verification for deep neural networks has been accepted to ICSE 2021.
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
We will be presenting three papers at NeurIPS-20.
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
All the five papers from our group were accepted to AAAI 2021.
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
Three Papers accepted to NeurIPS 2020.
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
Our Paper on Model Counting meets F0 Estimation (public version forthcoming!) is accepted to PODS 2021.
Authors: Arnab Bhattacharyya, Kuldeep Meel, A. Pavan and N.V. Vinodchandran
We presented our work on Phase Transition Behaviour in Knowledge Compilation at CP 2020.
We presented three papers at CAV 2020.
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.
We have released the source code of Manthan.
Our Paper on Phase Transition Behaviour in Knowledge Compilation is accepted to CP 2020.
Authors: Rahul Gupta, Subhajit Roy and Kuldeep S. Meel
We have released ApproxMC 4.
Two Papers accepted to SAT 2020.
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
Paper on Sparse Hashing for Approximate Model counting accepted to LICS 2020. Authors: S. Akshay 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.”
Paper accepted to LPAR-23.
The paper formalizes Induction Models on N extending the classical work of Henkin. Authors: A Dileep, Kuldeep S. Meel and Ammar F. Sabili
Three Papers accepted at Computer Aided Verification (CAV) 2020 conference.
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
Sampling-based approach for quantittive quantitative verification of Deep Neural Nets.
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.
Alexey Ignatiev, Joao Marques-Silva, Kuldeep S. Meel and Nina Narodytska give a tutorial at the Tutorial Forum in AAAI'20: Rigorous Verification and Explanation of ML Models.
Our paper on classification rules in relaxed logical form is accepted in ECAI-2020. Authors: Bishwamittra Ghosh, Dmitry Malioutov, and Kuldeep S. Meel

2019

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 <a href="https://bishwamittra.github.io/publication/irr-ghosh.pdf" 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.
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 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.