AI帮你理解科学

AI 生成解读视频

AI抽取解析论文重点内容自动生成视频


pub
生成解读视频

AI 溯源

AI解析本论文相关学术脉络


Master Reading Tree
生成 溯源树

AI 精读

AI抽取本论文的概要总结


微博一下
We introduce a new technique that can handle all rational weights, i.e. all weights of the form

Taming Discrete Integration via the Boon of Dimensionality

NIPS 2020, (2020)

被引用3|浏览40
EI
下载 PDF 全文
引用
微博一下

摘要

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...更多
0
简介
  • 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.
    Google ScholarLocate open access versionFindings
  • Megasthenis Asteris and Alexandros G Dimakis. LDPC codes for discrete integration. Technical report, Technical report, UT Austin, 2016.
    Google ScholarFindings
  • Arthur Asuncion and David Newman. UCI machine learning repository, 2007.
    Google ScholarFindings
  • Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, and Peter Stuckey. #∃SAT: Projected model counting. In Proc. of SAT, pages 121–137.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • 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.
    Findings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Proc. of CP, pages 200–216, 2013.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6):772–799, 2008.
    Google ScholarLocate open access versionFindings
  • Adnan Darwiche. New advances in compiling CNF to decomposable negation normal form. In Proc. of ECAI, pages 318–322, 2004.
    Google ScholarLocate open access versionFindings
  • Adnan Darwiche and Pierre Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research, 17:229–264, 2002.
    Google ScholarLocate open access versionFindings
  • Jessica Davies. Solving MaxSAT by decoupling optimization and satisfaction. PhD thesis, University of Toronto, 2013.
    Google ScholarFindings
  • Alexis de Colnet and Kuldeep S. Meel. Dual hashing-based algorithms for discrete integration. In Proc. of CP, pages 161–176.
    Google ScholarLocate open access versionFindings
  • Fan Ding, Hanjing Wang, Ashish Sabharwal, and Yexiang Xue. Towards efficient discrete integration via adaptive quantile queries. arXiv preprint arXiv:1910.05811, 2019.
    Findings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Frederik Eaton and Zoubin Ghahramani. Choosing a variable to clamp. In Proc. of AISTATS, 2009.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Randy Hickey and Fahiem Bacchus. Speeding up assumption-based SAT. In Proc. of SAT, pages 164–182.
    Google ScholarLocate open access versionFindings
  • Daphne Koller and Nir Friedman. Probabilistic graphical models: principles and techniques. MIT press, 2009.
    Google ScholarFindings
  • Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In Proc. of IJCAI, volume 2017, 2017.
    Google ScholarLocate open access versionFindings
  • Jean-Marie Lagniez and Pierre Marquis. A recursive algorithm for projected model counting. In Proc. of AAAI, volume 33, pages 1536–1543, 2019.
    Google ScholarLocate open access versionFindings
  • Yann LeCun, Corinna Cortes, and CJ Burges. Mnist handwritten digit database, 2010.
    Google ScholarFindings
  • Qiang Liu and Alexander Ihler. Bounding the partition function using Holder’s inequality. In Proc. of ICML, 2011.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Thomas Minka and Yuan Qi. Tree-structured approximations by expectation propagation. In Proc. of NeurIPS, 2004.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Nina Narodytska, Hongce Zhang, Aarti Gupta, and Toby Walsh. In search for a SAT-friendly binarized neural network architecture. In Proc. of ICLR, 2020.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Yash Pote, Saurabh Joshi, and Kuldeep S. Meel. Phase transition behavior of cardinality and XOR constraints. In Proc. of IJCAI, pages 1162–1168, 2019.
    Google ScholarLocate open access versionFindings
  • Matthew Richardson and Pedro Domingos. Markov logic networks. Machine learning, 62(12):107–136, 2006.
    Google ScholarLocate open access versionFindings
  • Norman Routledge. Computing Farey series. The Mathematical Gazette, 92(523):55–62, 2008.
    Google ScholarLocate open access versionFindings
  • Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Proc. of IJCAI, 2019.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT Solvers to Cryptographic Problems. In Proc. of SAT. Springer-Verlag, 2009.
    Google ScholarLocate open access versionFindings
  • Larry Stockmeyer. The complexity of approximate counting. In Proc. of STOC, pages 118–126, 1983.
    Google ScholarLocate open access versionFindings
  • Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM Journal on Computing, 8(3):410–421, 1979.
    Google ScholarLocate open access versionFindings
  • Wim Wiegerinck and Tom Heskes. Fractional belief propagation. In Proc. of NeurIPS, 2003.
    Google ScholarLocate open access versionFindings
  • Jonathan S. Yedidia, William T. Freeman, and Yair Weiss. Generalized belief propagation. Proc. of NeurIPS, 2000.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Michael Zhu and Stefano Ermon. A hybrid approach for probabilistic inference using random projections. In Proc. of ICML, pages 2039–2047, 2015.
    Google ScholarLocate open access versionFindings
您的评分 :
0

 

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