## AI帮你理解科学

## AI 精读

AI抽取本论文的概要总结

微博一下：

# Taming Discrete Integration via the Boon of Dimensionality

NIPS 2020, (2020)

EI

关键词

摘要

Discrete integration is a fundamental problem in computer science that concerns the computation of discrete sums over exponentially large sets. Despite intense interest from researchers for over three decades, the design of scalable techniques for computing estimates with rigorous guarantees for discrete integration remains the holy gra...更多

简介

- Given a large set of items S and a weight function W that assigns weight to each of the items, the problem of discrete integration, known as weighted counting, is to compute the weight of S, defined as the weighted sum of items of S.
- It is commonplace to implicitly represent S as the set of assignments that satisfy a Boolean formula F by using standard transformations from discrete domains to Boolean variables [6]
- This allows one to leverage powerful combinatorial solvers within the process of answering the discrete integration query [23, 24, 8].
- Since discrete integration is #P-complete even when the weight function is constant [46], this has motivated theoreticians and practitioners alike to focus on approximation techniques

重点内容

- Given a large set of items S and a weight function W that assigns weight to each of the items, the problem of discrete integration, known as weighted counting, is to compute the weight of S, defined as the weighted sum of items of S
- Discrete integration is a fundamental problem in computer science with a wide variety of applications covering partition function computations [22, 1], probabilistic inference [32, 50], network reliability estimation [19], and the verification of neural networks [5, 35, 36], which is the topic of this work
- We introduce in Section 3 the primary contribution of this paper: an efficient reduction from discrete integration to model counting that allows for non-dyadic weights
- We build on the paradigm of reducing discrete integration to model counting and propose a reduction that relaxes the restriction to dyadic weights from prior work
- The resulting tool, DeWeight, is able to handle instances arising from neural network verification domains, a critical area of concern

方法

- All experiments are performed on 2.5 GHz CPUs with 24 cores and 96GB RAM. Each discrete integration query ran on one core with a 4GB memory cap and 8 hour timeout.

结果

- Of the unweighted 1056 formulas, 126 are detected as unsatisfiable by ApproxMC within 8 hours and so the authors discard these.
- The authors consider two different weight settings on the remaining satisfiable benchmarks.
- Times recorded for DeWeight and Dyadic include both the time for the reduction stage and time spent in ApproxMC; the time for the reduction stage was never more than 4 seconds.
- Number of benchmarks solved (a) Experiment 1 (b) Experiment 2.
- Probability of satisfiability DeWeight Dyadic 10−43 Benchmark Number 10−34.
- 100 200 300 Benchmark Number

结论

- Discrete integration is a fundamental problem in computer science with a wide variety of applications.
- The resulting tool, DeWeight, is able to handle instances arising from neural network verification domains, a critical area of concern
- These instances were shown to be beyond the ability of prior work.
- One limitation of the framework is that due to the performance of the underlying approximate model counter, the method is currently limited to work well only for problems where the problem can be projected on 100 or fewer variables
- Even with this limitation, DeWeight is the only technique that is able to handle such benchmarks with large tilt.
- The authors trust that improvements in the underlying approximate model counter, which is itself a highly active research area, will allow for larger sampling sets in the future

相关工作

- Recently, hashing-based techniques have emerged as a dominant paradigm in the context of model counting [45, 25, 10, 24, 49, 11, 2, 43, 42]. The key idea is to reduce the problem of counting the solutions of a formula F to that of polynomially many satisfiability (SAT) queries wherein each query is described as the formula F conjuncted with random XOR constraints. The concurrent development of CryptoMiniSat [44, 43, 42], a state of the art SAT solver with native support for XORs, has led to impressive scalability of hashing-based model counting techniques.

In a significant conceptual breakthrough, Ermon et al [24] showed how hashing-based techniques can be lifted to discrete integration. Their framework, WISH, reduces the computation of discrete integration to linearly many optimization queries (specifically, MaxSAT queries) wherein each query is invoked over F conjuncted with random XOR constraints. The unavailability of MaxSAT solvers with native support for XORs has hindered the scalability of WISH style techniques. A dual approach proposed by Chakraborty et al [8, 16] reduces discrete integration to linearly many counting queries over formulas wherein each of counting query is constructed by conjunction of F with Pseudo-Boolean constraints, which is shown to scale poorly [38]. In summary, there exists a wide gap in the theory and practice of hashing-based approaches for discrete integration.

基金

- This work was supported in part by National Research Foundation Singapore under its NRF Fellowship Programme [NRF-NRFFAI1-2019-0004] and AI Singapore Programme [AISG-RP-2018-005], by NUS ODPRT Grant [R-252-000-685-13], and by NSF grants [IIS-1527668, CCF-1704883, IIS-1830549, and DMS-1547433]

引用论文

- Dimitris Achlioptas and Pei Jiang. Stochastic integration via error-correcting codes. In Proc. of UAI, pages 22–31, 2015.
- Megasthenis Asteris and Alexandros G Dimakis. LDPC codes for discrete integration. Technical report, Technical report, UT Austin, 2016.
- Arthur Asuncion and David Newman. UCI machine learning repository, 2007.
- Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, and Peter Stuckey. #∃SAT: Projected model counting. In Proc. of SAT, pages 121–137.
- Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, and Prateek Saxena. Quantitative verification of neural networks and its security applications. In Proc. of CCS, pages 1249–1264. ACM, 2019.
- Armin Biere, Marijn. Heule, Hans van Maaren, and Toby Walsh. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, The Netherlands, 2009.
- Thomas Caridroit, Fabien Delorme, Jean-Marie Lagniez, and Emmanuel Lonca. The d-DNNF reasoner. http://www.cril.univ-artois.fr/kc/d-DNNF-reasoner.html. Accessed:2020-05-01.
- Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. Distribution-aware sampling and weighted model counting for SAT. In Proc. of AAAI, pages 1722–1730, 2014.
- Supratik Chakraborty, Dror Fried, Kuldeep S Meel, and Moshe Y Vardi. From weighted to unweighted model counting. In Proc. of AAAI, pages 689–695, 2015.
- Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Proc. of CP, pages 200–216, 2013.
- Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In Proc. of IJCAI, 2016.
- Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6):772–799, 2008.
- Adnan Darwiche. New advances in compiling CNF to decomposable negation normal form. In Proc. of ECAI, pages 318–322, 2004.
- Adnan Darwiche and Pierre Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research, 17:229–264, 2002.
- Jessica Davies. Solving MaxSAT by decoupling optimization and satisfaction. PhD thesis, University of Toronto, 2013.
- Alexis de Colnet and Kuldeep S. Meel. Dual hashing-based algorithms for discrete integration. In Proc. of CP, pages 161–176.
- Fan Ding, Hanjing Wang, Ashish Sabharwal, and Yexiang Xue. Towards efficient discrete integration via adaptive quantile queries. arXiv preprint arXiv:1910.05811, 2019.
- Jeffrey M Dudek, Kuldeep S Meel, and Moshe Y Vardi. The hard problems are almost everywhere for random CNF-XOR formulas. In Proc. of IJCAI, pages 600–606, 2017.
- Leonardo Dueñas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Countingbased reliability estimation for power-transmission grids. In Proc. of AAAI, pages 4488–4494. AAAI Press, 2017.
- Arnaud Durand, Miki Hermann, and Phokion G Kolaitis. Subtractive reductions and complete problems for counting complexity classes. Theoretical Computer Science, 340(3):496–513, 2005.
- Frederik Eaton and Zoubin Ghahramani. Choosing a variable to clamp. In Proc. of AISTATS, 2009.
- Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Embed and project: Discrete sampling with universal hashing. In Proc. of NeurIPS, pages 2085–2093, 2013.
- Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Optimization with parity constraints: From binary codes to discrete integration. In Proc. of UAI, 2013.
- Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Taming the curse of dimensionality: Discrete integration by hashing and optimization. In Proc. of ICML, pages 334–342, 2013.
- Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting: A new strategy for obtaining good bounds. In Proc. of AAAI, volume 21, pages 54–61, 2006.
- Randy Hickey and Fahiem Bacchus. Speeding up assumption-based SAT. In Proc. of SAT, pages 164–182.
- Daphne Koller and Nir Friedman. Probabilistic graphical models: principles and techniques. MIT press, 2009.
- Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In Proc. of IJCAI, volume 2017, 2017.
- Jean-Marie Lagniez and Pierre Marquis. A recursive algorithm for projected model counting. In Proc. of AAAI, volume 33, pages 1536–1543, 2019.
- Yann LeCun, Corinna Cortes, and CJ Burges. Mnist handwritten digit database, 2010.
- Qiang Liu and Alexander Ihler. Bounding the partition function using Holder’s inequality. In Proc. of ICML, 2011.
- Qi Lou, Rina Dechter, and Alexander Ihler. Dynamic importance sampling for anytime bounds of the partition function. In Proc. of NeurIPS, pages 3196–3204, 2017.
- Thomas Minka and Yuan Qi. Tree-structured approximations by expectation propagation. In Proc. of NeurIPS, 2004.
- Christian Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric I. Hsu. DSHARP: fast dDNNF compilation with sharpSAT. In Proc. of Canadian AI, pages 356–361.
- Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, and João MarquesSilva. Assessing heuristic machine learning explanations with model counting. In Proc. of SAT, volume 11628 of Lecture Notes in Computer Science, pages 267–278.
- Nina Narodytska, Hongce Zhang, Aarti Gupta, and Toby Walsh. In search for a SAT-friendly binarized neural network architecture. In Proc. of ICLR, 2020.
- Judea Pearl. Reverend bayes on inference engines: A distributed hierarchical approach. In David L. Waltz, editor, Proc. of AAAI, pages 133–136. AAAI Press, 1982.
- Yash Pote, Saurabh Joshi, and Kuldeep S. Meel. Phase transition behavior of cardinality and XOR constraints. In Proc. of IJCAI, pages 1162–1168, 2019.
- Matthew Richardson and Pedro Domingos. Markov logic networks. Machine learning, 62(12):107–136, 2006.
- Norman Routledge. Computing Farey series. The Mathematical Gazette, 92(523):55–62, 2008.
- Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Proc. of IJCAI, 2019.
- Mate Soos, Stephan Gocht, and Kuldeep S. Meel. Accelerating approximate techniques for counting and sampling models through refined CNF-XOR solving. In Proc. of CAV, 7 2020.
- Mate Soos and Kuldeep S Meel. BIRD: Engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In Proc. of AAAI, 2019.
- Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT Solvers to Cryptographic Problems. In Proc. of SAT. Springer-Verlag, 2009.
- Larry Stockmeyer. The complexity of approximate counting. In Proc. of STOC, pages 118–126, 1983.
- Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM Journal on Computing, 8(3):410–421, 1979.
- Wim Wiegerinck and Tom Heskes. Fractional belief propagation. In Proc. of NeurIPS, 2003.
- Jonathan S. Yedidia, William T. Freeman, and Yair Weiss. Generalized belief propagation. Proc. of NeurIPS, 2000.
- Shengjia Zhao, Sorathan Chaturapruek, Ashish Sabharwal, and Stefano Ermon. Closing the gap between short and long XORs for model counting. In Proc. of AAAI, 2016.
- Michael Zhu and Stefano Ermon. A hybrid approach for probabilistic inference using random projections. In Proc. of ICML, pages 2039–2047, 2015.

标签

评论

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn