Document Open Access Logo

Towards Learning Quantifier Instantiation in SMT

Authors Mikoláš Janota , Jelle Piepenbrock , Bartosz Piotrowski

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.7.pdf
  • Filesize: 1.13 MB
  • 18 pages

Document Identifiers

Author Details

Mikoláš Janota
  • Czech Technical University in Prague, Czech Republic
Jelle Piepenbrock
  • Czech Technical University in Prague, Czech Republic
  • Radboud University Nijmegen, Netherlands
Bartosz Piotrowski
  • Czech Technical University in Prague, Czech Republic
  • University of Warsaw, Poland

Funding

The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902, the European Regional Development Fund under the Czech project AI&Reasoning no. CZ.02.1.01/0.0/0.0/15_003/0000466, the grant of National Science Center, Poland, no. 2018/29/N/ST6/02903, and Amazon Research Awards. This article is part of the RICAIP project that has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 857306.

Cite AsGet BibTex

Mikoláš Janota, Jelle Piepenbrock, and Bartosz Piotrowski. Towards Learning Quantifier Instantiation in SMT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.7

Abstract

This paper applies machine learning (ML) to solve quantified satisfiability modulo theories (SMT) problems more efficiently. The motivating idea is that the solver should learn from already solved formulas to solve new ones. This is especially relevant in classes of similar formulas. We focus on the enumerative instantiation - a well-established approach to solving quantified formulas anchored in the Herbrand’s theorem. The task is to select the right ground terms to be instantiated. In ML parlance, this means learning to rank ground terms. We devise a series of features of the considered terms and train on them using boosted decision trees. In particular, we integrate the LightGBM library into the SMT solver cvc5. The experimental results demonstrate that the ML-guided solver enables us to solve more formulas than the base solver and reduce the number of quantifier instantiations. We also do an ablation study on the features used in the machine learning component, showing the contributions of the various additions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • satisfiability modulo theories
  • quantifier instantiation
  • machine learning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Mislav Balunovic, Pavol Bielik, and Martin T. Vechev. Learning to solve SMT formulas. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pages 10338-10349, 2018. URL: https://proceedings.neurips.cc/paper/2018/hash/68331ff0427b551b68e911eebe35233b-Abstract.html.
  2. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  3. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects, 4th International Symposium, FMCO, volume 4111, pages 364-387. Springer, 2005. URL: https://doi.org/10.1007/11804192_17.
  4. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Computer Aided Verification - 23rd International Conference, CAV, volume 6806, pages 171-177. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_14.
  5. Clark W. Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, and Cesare Tinelli. The SMT-LIB initiative and the rise of SMT - (HVC 2010 award talk). In Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC, volume 6504, page 3. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-19583-9_2.
  6. Clark W. Barrett and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Model Checking, pages 305-343. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_11.
  7. Nikolaj Bjørner and Mikoláš Janota. Playing with quantified satisfaction. In 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR, volume 35, pages 15-27. EasyChair, 2015. URL: https://easychair.org/publications/paper/jmM, URL: https://doi.org/10.29007/vv21.
  8. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending sledgehammer with SMT solvers. J. Autom. Reason., 51(1):109-128, 2013. URL: https://doi.org/10.1007/s10817-013-9278-5.
  9. Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, and Pascal Fontaine. veriT: An open, trustable and efficient SMT-solver. In Automated Deduction - CADE-22, 22nd International Conference on Automated, volume 5663, pages 151-156. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02959-2_12.
  10. Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, and Wolfram Schulte. Vcc: Contract-based modular verification of concurrent c. In 2009 31st International Conference on Software Engineering-Companion Volume, pages 429-430. IEEE, 2009. Google Scholar
  11. David Detlefs, Greg Nelson, and James B. Saxe. Simplify: A theorem prover for program checking. J. ACM, 52(3):365-473, 2005. URL: https://doi.org/10.1145/1066100.1066102.
  12. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: Pre-training of deep bidirectional transformers for language understanding. In Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT, 2019. URL: https://doi.org/10.18653/v1/n19-1423.
  13. Azadeh Farzan and Zachary Kincaid. Strategy synthesis for linear arithmetic games. Proc. ACM Program. Lang., 2(POPL):61:1-61:30, 2018. URL: https://doi.org/10.1145/3158149.
  14. Tom Fawcett. An introduction to ROC analysis. Pattern Recognit. Lett., 27(8):861-874, 2006. URL: https://doi.org/10.1016/j.patrec.2005.10.010.
  15. Michael J. Fischer and Michael O. Rabin. Super-exponential complexity of presburger arithmetic. In Texts and Monographs in Symbolic Computation, pages 122-135. Springer Vienna, 1998. URL: https://doi.org/10.1007/978-3-7091-9459-1_5.
  16. Yeting Ge and Leonardo Mendonça de Moura. Complete instantiation for quantified formulas in satisfiability modulo theories. In Computer Aided Verification, 21st International Conference, CAV, pages 306-320, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_25.
  17. Jacques Herbrand. Recherches sur la théorie de la démonstration. Doctorat d'état, La Faculté des Sciences de Paris, 1930. Google Scholar
  18. Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, and Josef Urban. ENIGMA Anonymous: Symbol-independent inference guiding machine (system description). In Automated Reasoning - 10th International Joint Conference, IJCAR, volume 12167, pages 448-463. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_29.
  19. Mikoláš Janota, Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. Fair and adventurous enumeration of quantifier instantiations. In Formal Methods in Computer-Aided Design, 2021. Google Scholar
  20. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems, NeurIPS, 2018. URL: https://proceedings.neurips.cc/paper/2018/hash/55acf8539596d25624059980986aaa78-Abstract.html.
  21. Guolin Ke, Qi Meng, Thomas Finley, Taifeng Wang, Wei Chen, Weidong Ma, Qiwei Ye, and Tie-Yan Liu. LightGBM: A highly efficient gradient boosting decision tree. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems, pages 3146-3154, 2017. URL: https://proceedings.neurips.cc/paper/2017/hash/6449f44a102fde848669bdd9eb6b76fa-Abstract.html.
  22. Alex Krizhevsky, Ilya Sutskever, and Geoffrey E. Hinton. ImageNet classification with deep convolutional neural networks. In Advances in Neural Information Processing Systems 25: 26th Annual Conference on Neural Information Processing Systems, pages 1106-1114, 2012. URL: https://proceedings.neurips.cc/paper/2012/hash/c399862d3b9d6b76c8436e924a68c45b-Abstract.html.
  23. James Donald Monk. Mathematical logic, volume 37. Springer Science & Business Media, 2012. Google Scholar
  24. Yannick Moy and Angela Wallenburg. Tokeneer: Beyond formal program verification. Embedded Real Time Software and Systems, 24, 2010. Google Scholar
  25. Saeed Nejati, Ludovic Le Frioux, and Vijay Ganesh. A machine learning based splitting heuristic for divide-and-conquer solvers. In Principles and Practice of Constraint Programming - 26th International Conference, CP, volume 12333, pages 899-916. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_52.
  26. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. Solving quantified bit-vectors using invertibility conditions. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, volume 10982, pages 236-255. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96142-2_16.
  27. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. Syntax-guided quantifier instantiation. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, volume 12652, pages 145-163. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_8.
  28. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli. Towards bit-width-independent proofs in SMT solvers. In International Conference on Automated Deduction, pages 366-384. Springer, 2019. Google Scholar
  29. Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM, 53(6):937-977, 2006. URL: https://doi.org/10.1145/1217856.1217859.
  30. Eniola Olaleye. How to win any ML contest, 2021. Published as URL: https://medium.com/machine-learning-insights/how-to-win-any-ml-contest-244a12c62f30.
  31. Danieli El Ouraou, Pascal Fontaine, and Cezary Kaliszyk. Machine learning for instance selection in SMT solving, 2019. URL: https://members.loria.fr/delouraoui/links/instanceselection_paper.pdf.
  32. Nikhil Pimpalkhare, Federico Mora, Elizabeth Polgreen, and Sanjit A. Seshia. Medleysolver: Online SMT algorithm selection, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_31.
  33. Bartosz Piotrowski and Josef Urban. ATPboost: learning premise selection in binary setting with ATP feedback. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC, volume 10900, pages 566-574. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_37.
  34. Bartosz Piotrowski and Josef Urban. Stateful premise selection by recurrent neural networks. In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73, pages 409-422. EasyChair, 2020. URL: https://easychair.org/publications/paper/g38n, URL: https://doi.org/10.29007/j5hd.
  35. Ruzica Piskac, Thomas Wies, and Damien Zufferey. GRASShopper. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2014. Google Scholar
  36. Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Revisiting enumerative instantiation. In Tools and Algorithms for the Construction and Analysis of Systems, volume 10806, pages 112-131, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_7.
  37. Andrew Reynolds, Tim King, and Viktor Kuncak. Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des., 51(3):500-532, 2017. URL: https://doi.org/10.1007/s10703-017-0290-y.
  38. Andrew Reynolds, Cesare Tinelli, and Leonardo Mendonça de Moura. Finding conflicting instances of quantified formulas in SMT. In Formal Methods in Computer-Aided Design, FMCAD, pages 195-202. IEEE, 2014. URL: https://doi.org/10.1109/FMCAD.2014.6987613.
  39. Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, and Vijay Ganesh. MachSMT: A machine learning-based algorithm selector for SMT solvers. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, volume 12652, pages 303-325. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_16.
  40. Daniel Selsam and Nikolaj Bjørner. Guiding high-performance SAT solvers with unsat-core predictions. In Mikoláš Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, volume 11628, pages 336-353. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_24.
  41. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil. MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, volume 5195, pages 441-456. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71070-7_37.
  42. Julien Vanegue and Shuvendu Lahiri. Towards practical reactive security audit using extended static checkers. In IEEE Symposium on Security and Privacy (Oakland'13), May 2013. URL: https://www.microsoft.com/en-us/research/publication/towards-practical-reactive-security-audit-using-extended-static-checkers/.
  43. Soner Yildirim. How to tune the hyperparameters for better performance, 2020. Published as URL: https://towardsdatascience.com/how-to-tune-the-hyperparameters-for-better-performance-cfe223d398b3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact