Towards finding longer proofs. (English) Zbl 07532515
Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 167-186 (2021).
Summary: We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). Unlike most learning based approaches, we focus on generalising from very little training data and achieving near complete confidence. We use several simple, structured datasets with very long proofs to show that FLoP can successfully generalise a single training proof to a large class of related problems. On these benchmarks, FLoP is competitive with strong theorem provers despite using very limited search, due to its ability to solve problems that are prohibitively long for other systems.
For the entire collection see [Zbl 1486.68013].
For the entire collection see [Zbl 1486.68013].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
Software:
E Theorem Prover; Coq; MaLARea; Isabelle/HOL; VAMPIRE; HOL Light; TPTP; ENIGMA; HOList; OpenAI Gym; FEMaLeCoP; lazyCoP; Stable Baselines; GitHubReferences:
| [1] | Anthony, T., Tian, Z., Barber, D.: Thinking fast and slow with deep learning and tree search. CoRR abs/1705.08439 (2017). http://arxiv.org/abs/1705.08439 |
| [2] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge: Cambridge University Press, Cambridge · Zbl 0948.68098 · doi:10.1017/CBO9781139172752 |
| [3] | Bansal, K., Loos, S.M., Rabe, M.N., Szegedy, C., Wilcox, S.: HOList: an environment for machine learning of higher-order theorem proving (extended version). CoRR abs/1904.03241 (2019). http://arxiv.org/abs/1904.03241 |
| [4] | Barrett, C.; Tinelli, C.; Clarke, E.; Henzinger, T.; Veith, H.; Bloem, R., Satisfiability modulo theories, Handbook of Model Checking, 305-343 (2018), Cham: Springer, Cham · Zbl 1392.68379 · doi:10.1007/978-3-319-10575-8_11 |
| [5] | Bertot, Y.; Castran, P., Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions (2010), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-662-07964-5 |
| [6] | Bibel, W., Eder, E., Fronhöfer, B.: Towards an advanced implementation of the connection method. In: Bundy, A. (ed.) Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, FRG, August 1983, pp. 920-922. William Kaufmann (1983). http://ijcai.org/Proceedings/83-2/Papers/072.pdf |
| [7] | Bledsoe, W.W.: Some thoughts on proof discovery. In: Proceedings of the 1986 Symposium on Logic Programming, Salt Lake City, Utah, USA, 22-25 September 1986, pp. 2-10. IEEE-CS (1986) |
| [8] | Brock, B.; Cooper, S.; Pierce, W.; Lusk, E.; Overbeek, R., Analogical reasoning and proof discovery, 9th International Conference on Automated Deduction, 454-468 (1988), Heidelberg: Springer, Heidelberg · Zbl 0666.68096 · doi:10.1007/BFb0012849 |
| [9] | Brockman, G., et al.: OpenAI gym. CoRR abs/1606.01540 (2016). http://arxiv.org/abs/1606.01540 |
| [10] | Bundy, A.; Lusk, E.; Overbeek, R., The use of explicit plans to guide inductive proofs, 9th International Conference on Automated Deduction, 111-120 (1988), Heidelberg: Springer, Heidelberg · Zbl 0656.68106 · doi:10.1007/BFb0012826 |
| [11] | Chvalovský, K., Jakubuv, J., Suda, M., Urban, J.: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. CoRR abs/1903.03182 (2019). http://arxiv.org/abs/1903.03182 · Zbl 1535.68449 |
| [12] | Crouse, M., et al.: A deep reinforcement learning approach to first-order logic theorem proving. Artificial Intelligence (2019) |
| [13] | Harrison, J.; Srivas, M.; Camilleri, A., HOL light: a tutorial introduction, Formal Methods in Computer-Aided Design, 265-269 (1996), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0031814 |
| [14] | Hill, A., et al.: Stable baselines (2018). https://github.com/hill-a/stable-baselines |
| [15] | Jakubův, J.; Chvalovský, K.; Olšák, M.; Piotrowski, B.; Suda, M.; Urban, J.; Peltier, N.; Sofronie-Stokkermans, V., ENIGMA anonymous: symbol-independent inference guiding machine (system description), Automated Reasoning, 448-463 (2020), Cham: Springer, Cham · Zbl 07614690 · doi:10.1007/978-3-030-51054-1_29 |
| [16] | Jakubův, J.; Urban, J.; Geuvers, H.; England, M.; Hasan, O.; Rabe, F.; Teschke, O., ENIGMA: efficient learning-based inference guiding machine, Intelligent Computer Mathematics, 292-302 (2017), Cham: Springer, Cham · Zbl 1367.68249 · doi:10.1007/978-3-319-62075-6_20 |
| [17] | Jakubuv, J., Urban, J.: Hammering mizar by learning clause guidance. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA. LIPIcs, vol. 141, pp. 34:1-34:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). doi:10.4230/LIPIcs.ITP.2019.34 |
| [18] | Kaliszyk, C.; Urban, J.; Davis, M.; Fehnker, A.; McIver, A.; Voronkov, A., FEMaLeCoP: fairly efficient machine learning connection prover, Logic for Programming, Artificial Intelligence, and Reasoning, 88-96 (2015), Heidelberg: Springer, Heidelberg · Zbl 1471.68312 · doi:10.1007/978-3-662-48899-7_7 |
| [19] | Kaliszyk, C., Urban, J., Michalewski, H., Olsák, M.: Reinforcement learning of theorem proving. In: NeurIPS, pp. 8836-8847 (2018) |
| [20] | Kaliszyk, C., Urban, J., Vyskočil, J.: Certified connection tableaux proofs for HOL Light and TPTP. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP ’15, pp. 59-66. ACM (2015). doi:10.1145/2676724.2693176. doi:10.1145/2676724.2693176 |
| [21] | Kaliszyk, C., Urban, J., Vyskočil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) Proc. of the 24th International Joint Conference on Artificial Intelligence (IJCAI’15), pp. 3084-3090. AAAI Press (2015) |
| [22] | Kalman, JA, A shortest single axiom for the classical equivalential calculus, Notre Dame J. Form. Logic, 19, 1, 141-144 (1978) · Zbl 0368.02009 · doi:10.1305/ndjfl/1093888216 |
| [23] | Kinyon, M.; Veroff, R.; Vojtěchovský, P.; Bonacina, MP; Stickel, ME, Loops with abelian inner mapping groups: an application of automated deduction, Automated Reasoning and Mathematics, 151-164 (2013), Heidelberg: Springer, Heidelberg · Zbl 1383.68077 · doi:10.1007/978-3-642-36675-8_8 |
| [24] | Kocsis, L.; Szepesvári, C.; Fürnkranz, J.; Scheffer, T.; Spiliopoulou, M., Bandit based Monte-Carlo planning, Machine Learning: ECML 2006, 282-293 (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11871842_29 |
| [25] | Kovács, L.; Voronkov, A.; Sharygina, N.; Veith, H., First-order theorem proving and Vampire, Computer Aided Verification, 1-35 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_1 |
| [26] | Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (2017) · Zbl 1403.68197 |
| [27] | McCune, W.; Wos, L.; Kapur, D., Experiments in automated deduction with condensed detachment, Automated Deduction—CADE-11, 209-223 (1992), Heidelberg: Springer, Heidelberg · Zbl 0925.68402 · doi:10.1007/3-540-55602-8_167 |
| [28] | Melis, E.; Pinto-Ferreira, C.; Mamede, NJ, Theorem proving by analogy — A compelling example, Progress in Artificial Intelligence, 261-272 (1995), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-60428-6_22 |
| [29] | Melis, E.; Siekmann, JH, Knowledge-based proof planning, Artif. Intell., 115, 1, 65-105 (1999) · Zbl 0939.68822 · doi:10.1016/S0004-3702(99)00076-4 |
| [30] | Nipkow, T.; Wenzel, M.; Paulson, LC, Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002), Heidelberg: Springer, Heidelberg · Zbl 0994.68131 · doi:10.1007/3-540-45949-9 |
| [31] | Olsák, M., Kaliszyk, C., Urban, J.: Property invariant embedding for automated reasoning. In: Giacomo, G.D., Catalá, A., Dilkina, B., Milano, M., Barro, S., Bugarín, A., Lang, J. (eds.) ECAI 2020-24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020). Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 1395-1402. IOS Press (2020). doi:10.3233/FAIA200244 · Zbl 1464.68317 |
| [32] | Otten, J.; Bibel, W., leanCoP: lean connection-based theorem proving, J. Symb. Comput., 36, 139-161 (2003) · Zbl 1025.68076 · doi:10.1016/S0747-7171(03)00037-3 |
| [33] | Paliwal, A., Loos, S.M., Rabe, M.N., Bansal, K., Szegedy, C.: Graph representations for higher-order logic and theorem proving. CoRR abs/1905.10006 (2019). http://arxiv.org/abs/1905.10006 |
| [34] | Peterson, JG, Shortest single axioms for the classical equivalential calculus, Notre Dame J. Formal Log., 17, 2, 267-271 (1976) · Zbl 0313.02006 · doi:10.1305/ndjfl/1093887534 |
| [35] | Piotrowski, B.; Urban, J.; Benzmüller, C.; Miller, B., Guiding inferences in connection tableau by recurrent neural networks, Intelligent Computer Mathematics, 309-314 (2020), Cham: Springer, Cham · Zbl 1455.68252 · doi:10.1007/978-3-030-53518-6_23 |
| [36] | Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. CoRR abs/2009.03393 (2020). https://arxiv.org/abs/2009.03393 |
| [37] | Polya, G.: Mathematics and Plausible Reasoning. Introduction and Analogy in Mathematics, vol. 1. Princeton University Press, Princeton (1954) · Zbl 0056.24102 |
| [38] | Polya, G.: How to Solve It. Princeton University Press (1971). http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20&path=ASIN/0691023565 · Zbl 0061.00616 |
| [39] | Rawson, M., Reger, G.: lazycop 0.1. EasyChair Preprint no. 3926 (2020, EasyChair) |
| [40] | Resnick, C., Raileanu, R., Kapoor, S., Peysakhovich, A., Cho, K., Bruna, J.: Backplay: “Man muss immer umkehren”. CoRR abs/1807.06919 (2018). http://arxiv.org/abs/1807.06919 |
| [41] | Robinson, A.; Voronkov, A., Handbook of Automated Reasoning (2001), Amsterdam: Elsevier Science Publishers B. V, Amsterdam · Zbl 0964.00020 |
| [42] | Robinson, R.M.: An essentially undecidable axiom system. In: Proceedings of the International Congress of Mathematics, pp. 729-730 (1950) |
| [43] | Ross, S., Gordon, G., Bagnell, D.: A reduction of imitation learning and structured prediction to no-regret online learning. In: Gordon, G., Dunson, D., Dudik, M. (eds.) Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics. Proceedings of Machine Learning Research, vol. 15, pp. 627-635. PMLR, Fort Lauderdale (2011). http://proceedings.mlr.press/v15/ross11a.html |
| [44] | Salimans, T., Chen, R.: Learning Montezuma’s Revenge from a single demonstration. CoRR abs/1812.03381 (2018). http://arxiv.org/abs/1812.03381 |
| [45] | Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms. CoRR abs/1707.06347 (2017) |
| [46] | Schulz, S.; McMillan, K.; Middeldorp, A.; Voronkov, A., System description: E 1.8, Logic for Programming, Artificial Intelligence, and Reasoning, 735-743 (2013), Heidelberg: Springer, Heidelberg · Zbl 1407.68442 · doi:10.1007/978-3-642-45221-5_49 |
| [47] | Silver, D., Mastering the game of go without human knowledge, Nature, 550, 354 (2017) · doi:10.1038/nature24270 |
| [48] | Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483-502 (2017) · Zbl 1425.68381 |
| [49] | Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction, 2nd edn. The MIT Press (2018). http://incompleteideas.net/book/the-book-2nd.html · Zbl 1407.68009 |
| [50] | Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007. CEUR Workshop Proceedings, vol. 257. CEUR-WS.org (2007). http://ceur-ws.org/Vol-257/05_Urban.pdf |
| [51] | Urban, J.; Jakubův, J.; Benzmüller, C.; Miller, B., First neural conjecturing datasets and experiments, Intelligent Computer Mathematics, 315-323 (2020), Cham: Springer, Cham · Zbl 1455.68261 · doi:10.1007/978-3-030-53518-6_24 |
| [52] | Urban, J.; Sutcliffe, G.; Pudlák, P.; Vyskočil, J.; Armando, A.; Baumgartner, P.; Dowek, G., MaLARea SG1 - machine learner for automated reasoning with semantic guidance, Automated Reasoning, 441-456 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68434 · doi:10.1007/978-3-540-71070-7_37 |
| [53] | Veroff, R., Using hints to increase the effectiveness of an automated reasoning program: case studies, J. Autom. Reason., 16, 3, 223-239 (1996) · Zbl 0857.68095 · doi:10.1007/BF00252178 |
| [54] | Wos, L.; Winker, S.; Smith, B.; Veroff, R.; Henschen, L., A new use of an automated reasoning assistant: open questions in equivalential calculus and the study of infinite domains, Artifi. Intell., 22, 3, 303-356 (1984) · Zbl 0553.68051 · doi:10.1016/0004-3702(84)90054-7 |
| [55] | Wos, L., Meeting the challenge of fifty years of logic, J. Autom. Reason., 6, 2, 213-232 (1990) · Zbl 0697.68091 · doi:10.1007/BF00245821 |
| [56] | Zombori, Z.; Urban, J.; Brown, CE; Peltier, N.; Sofronie-Stokkermans, V., Prolog technology reinforcement learning prover, Automated Reasoning, 489-507 (2020), Cham: Springer, Cham · Zbl 07614694 · doi:10.1007/978-3-030-51054-1_33 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
