Elamur Research⌕
☰
home / papers / 2019 / Towards Finding Longer Proofs

Towards Finding Longer Proofs

Paper · 2019 · Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski et al.

Summary

Automated theorem provers usually fail on long proofs, because the number of possible inference sequences grows exponentially with proof length. The authors present FLoP, a guidance system for the connection tableau calculus (via the fCoP prover). It treats proving as a reinforcement learning environment and trains with PPO, a policy-gradient method with Temporal Difference value learning, plus curriculum learning. Rather than improving search, FLoP aims to absorb the pattern of a single training proof and reuse it on related, much longer problems, a basic form of reasoning by analogy. The evaluation uses a synthetic Robinson Arithmetic benchmark with adjustable difficulty and two Logical Calculi (LCL) sets from TPTP enriched with lemmata. Trained on one problem and given only a few attempts without search, FLoP generalises to proofs with hundreds or thousands of steps. It competes with or beats Vampire, E, leanCoP and rlCoP, especially when numbers use binary encoding. The datasets also serve as a scalable, interpretable RL benchmark.

Key points

  • FLoP pairs PPO-based rollout learning with curriculum techniques that were new to theorem proving. It contrasts with the MaLARea/DAgger search-and-retrain loop used by mcts-CoPs such as rlCoP, plCoP and graphCoP.
  • With unary-encoded arithmetic, only a portfolio mode of a single rewriting-based prover beat FLoP. With binary encoding, FLoP came out on top.
  • Under eager evaluation (no MCTS), plCoP collapsed on the LCL problems while FLoP was unaffected. Without a depth limit, FLoP fully solved both arithmetic problem classes.
  • Curriculum learning gave a small but steady gain over exploration alone. On LCL-Imp, 0.51 of proofs were found during training versus 0.45 without it.
  • When training proofs contained distracting extra steps, supervised learning on RA-1 fell from 0.98 to 0.52 success, while curriculum-trained FLoP stayed at about 0.98.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Universität InnsbruckInnsbruck · Austria23 works · 1,475 citations🎓Czech Technical University in PraguePrague · Czechia16 works · 930 citations🎓University of WarsawWarsaw · Poland14 works · 774 citations🔬HUN-REN Alfréd Rényi Institute of MathematicsBudapest · Hungary2 works · 77 citations🎓Eötvös Loránd UniversityBudapest · Hungary6 works · 277 citations

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk and Josef Urban. 2019. Towards Finding Longer Proofs. arXiv:1905.13100.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.1905.13100 · arXiv 1905.13100

@misc{zombori2019finding,
  title = {{Towards Finding Longer Proofs}},
  author = {Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk and Josef Urban},
  year = {2019},
  doi = {10.48550/arxiv.1905.13100},
  eprint = {1905.13100},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1905.13100}
}

References

57 references, 14 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  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. Cambridge University Press (1998) find
  3. Bansal, K., Loos, S.M., Rabe, M.N., Szegedy, C.: Learning to reason in large theories without imitation. CoRR abs/1905.10501 (2019), http://arxiv.org/abs/1905.10501 ↗
  4. 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 ↗
  5. Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305–343. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_11, https://doi.org/10.1007/978-3-319-10575-8_11 — [doi:10.1007/978-3-319-10575-8_11](https://doi.org/10.1007/978-3-319-10575-8_11) ↗
  6. Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions. Springer Publishing Company, Incorporated, 1st edn. (2010) find
  7. 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/… ↗
  8. Bledsoe, W.W.: Some thoughts on proof discovery. In: Proceedings of the 1986 Symposium on Logic Programming, Salt Lake City, Utah, USA, September 22-25, 1986. pp. 2–10. IEEE-CS (1986) find
  9. Brock, B., Cooper, S., Pierce, W.: Analogical reasoning and proof discovery. In: Lusk, E., Overbeek, R. (eds.) 9th International Conference on Automated Deduction. pp. 454–468. Springer Berlin Heidelberg, Berlin, Heidelberg (1988) find
  10. Brockman, G., Cheung, V., Pettersson, L., Schneider, J., Schulman, J., Tang, J., Zaremba, W.: OpenAI gym. CoRR abs/1606.01540 (2016), http://arxiv.org/abs/1606.01540 ↗
  11. Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E.L., Overbeek, R.A. (eds.) 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings. Lecture Notes in Computer Science, vol. 310, pp. 111–120. Springer (1988). https://doi.org/… find
  12. 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 ↗
  13. Crouse, M., Abdelaziz, I., Makni, B., Whitehead, S., Cornelio, C., Kapanipathi, P., Srinivas, K., Thost, V., Witbrock, M., Fokoue, A.: A deep reinforcement learning approach to first-order logic theorem proving. arXiv: Artificial Intelligence (2019) find
  14. Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M.K., Camilleri, A.J. (eds.) Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings. LNCS, vol. 1166, pp. 265–269. Springer (1996). https://doi.org/1… — [doi:10.1007/bfb0031814](https://doi.org/10.1007/bfb0031814) find
  15. Hill, A., Raffin, A., Ernestus, M., Gleave, A., Kanervisto, A., Traore, R., Dhariwal, P., Hesse, C., Klimov, O., Nichol, A., Plappert, M., Radford, A., Schulman, J., Sidor, S., Wu, Y.: Stable baselines. https://github.com/hill-a/stable-baselines (2018) ↗
  16. Jakubův, J., Chvalovský, K., Olšák, M., Piotrowski, B., Suda, M., Urban, J.: Enigma anonymous: Symbol-independent inference guiding machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. pp. 448–463. Springer International Publishing, Cham (2020)
  17. Jakubuv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Lecture Notes in Comput…
  18. 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… — [doi:10.4230/lipics.itp.2019.34](https://doi.org/10.4230/lipics.itp.2019.34) find
  19. Kaliszyk, C., Urban, J.: FEMaLeCoP: Fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, 2015, Proceedings. LNCS, vol. 9450, pp. 88–96. Springer… — [doi:10.1007/978-3-662-48899-7_7](https://doi.org/10.1007/978-3-662-48899-7_7) find
  20. Kaliszyk, C., Urban, J., Michalewski, H., Olsák, M.: Reinforcement learning of theorem proving. In: NeurIPS. pp. 8836–8847 (2018)
  21. 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. pp. 59–66. CPP ’15, ACM (2015). https://doi.org/10.1145/2676724.2693176, http://doi.acm.org/10.1145/2676724.2693176 Towards Fin… — [doi:10.1145/2676724.2693176](https://doi.org/10.1145/2676724.2693176) ↗
  22. 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) find
  23. Kalman, J.A.: A shortest single axiom for the classical equivalential calculus. Notre Dame Journal of Formal Logic 19(1), 141–144 (1978). https://doi.org/10.1305/ndjfl/1093888216 — [doi:10.1305/ndjfl/1093888216](https://doi.org/10.1305/ndjfl/1093888216) ↗
  24. Kinyon, M.K., Veroff, R., Vojtechovský, P.: Loops with abelian inner mapping groups: An application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics - Essays in Memory of William W. McCune. LNCS, vol. 7788, pp. 151–164. Springer (2013). https://doi… — [doi:10.1007/978-3-642-36675-8_8](https://doi.org/10.1007/978-3-642-36675-8_8) find
  25. Kocsis, L., Szepesvári, C.: Bandit based monte-carlo planning. In: Fürnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) Machine Learning: ECML 2006. pp. 282–293. Springer Berlin Heidelberg, Berlin, Heidelberg (2006) find
  26. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: CAV (2013) find
  27. 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)
  28. McCune, W., Wos, L.: Experiments in automated deduction with condensed detachment. In: Kapur, D. (ed.) Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings. Lecture Notes in Computer Science, vol. 607, pp. 209–2… — [doi:10.1007/3-540-55602-8_167](https://doi.org/10.1007/3-540-55602-8_167) find
  29. Melis, E.: Theorem proving by analogy - A compelling example. In: Pinto-Ferreira, C.A., Mamede, N.J. (eds.) Progress in Artificial Intelligence, 7th Portuguese Conference on Artificial Intelligence, EPIA ’95, Funchal, Madeira Island, Portugal, October 3-6, 1995, Proceedings. Lecture Notes in Compute… — [doi:10.1007/3-540-60428-6_22](https://doi.org/10.1007/3-540-60428-6_22) find
  30. Melis, E., Siekmann, J.H.: Knowledge-based proof planning. Artif. Intell. 115(1), 65–105 (1999). https://doi.org/10.1016/S0004-3702(99)00076-4, https://doi.org/10.1016/S0004-3702(99)00076-4 — [doi:10.1016/s0004-3702(99)00076-4](https://doi.org/10.1016/s0004-3702%2899%2900076-4) ↗
  31. Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Berlin, Heidelberg (2002) find
  32. 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 Compostel…
  33. Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36, 139–161 (2003) find
  34. 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 ↗
  35. Peterson, J.G.: Shortest single axioms for the classical equivalential calculus. Notre Dame J. Formal Log. 17(2), 267–271 (1976). https://doi.org/10.1305/ndjfl/1093887534, https://doi.org/10.1305/ndjfl/1093887534 — [doi:10.1305/ndjfl/1093887534](https://doi.org/10.1305/ndjfl/1093887534) ↗
  36. Piotrowski, B., Urban, J.: Guiding inferences in connection tableau by recurrent neural networks. In: Benzmüller, C., Miller, B.R. (eds.) Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings. Lecture Notes in Computer Science, v…
  37. Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. CoRR abs/2009.03393 (2020), https://arxiv.org/abs/2009.03393 ↗
  38. Polya, G.: Mathematics and Plausible Reasoning, Volume 1: Introduction and Analogy in Mathematics. Princeton University Press (1954) find
  39. Polya, G.: How to Solve It. Princeton University Press (November 1971), http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20&path=ASIN/0691023565 ↗
  40. Rawson, M., Reger, G.: lazycop 0.1. EasyChair Preprint no. 3926 (EasyChair, 2020) find
  41. 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 ↗
  42. Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science Publishers B. V., Amsterdam, The Netherlands, The Netherlands (2001) find
  43. Robinson, R.M.: An essentially undecidable axiom system. Proceedings of the International Congress of Mathematics pp. 729–730 (1950) find
  44. 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… find
  45. Salimans, T., Chen, R.: Learning Montezuma’s Revenge from a single demonstration. CoRR abs/1812.03381 (2018), http://arxiv.org/abs/1812.03381 — [arXiv:1812.03381](https://arxiv.org/abs/1812.03381) ↗
  46. Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms. CoRR abs/1707.06347 (2017) find
  47. Schulz, S.: System Description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) Proc. of the 19th LPAR. LNCS, vol. 8312. Springer (2013) find
  48. Silver, D., Schrittwieser, J., Simonyan, K., Antonoglou, I., Huang, A., Guez, A., Hubert, T., Baker, L., Lai, M., Bolton, A., Chen, Y., Lillicrap, T., Hui, F., Sifre, L., van den Driessche, G., Graepel, T., Hassabis, D.: Mastering the game of go without human knowledge. Nature 550, 354– (Oct 2017),… find
  49. Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59(4), 483–502 (2017) find
  50. Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. The MIT Press, second edn. (2018), http://incompleteideas.net/book/the-book-2nd.html ↗
  51. 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-…
  52. Urban, J., Jakubuv, J.: First neural conjecturing datasets and experiments. In: Benzmüller, C., Miller, B.R. (eds.) Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12236, pp. 315–323…
  53. Urban, J., Sutcliffe, G., Pudlák, P., Vyskocil, J.: MaLARea SG1- machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings.… — [doi:10.1007/978-3-540-71070-7_37](https://doi.org/10.1007/978-3-540-71070-7_37) find
  54. Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Autom. Reasoning 16(3), 223–239 (1996). https://doi.org/10.1007/BF00252178, https://doi.org/10.1007/BF00252178 — [doi:10.1007/bf00252178](https://doi.org/10.1007/bf00252178) ↗
  55. 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. Artificial Intelligence 22(3), 303 – 356 (1984). https://doi.org/https://doi.org/10.1016/0004-3702(84)90054-7, http://w… — [doi:10.1016/0004-3702(84)90054-7](https://doi.org/10.1016/0004-3702%2884%2990054-7) find
  56. Wos, L.: Meeting the challenge of fifty years of logic. J. Autom. Reason. 6(2), 213–232 (1990). https://doi.org/10.1007/BF00245821, https://doi.org/10.1007/BF00245821 — [doi:10.1007/bf00245821](https://doi.org/10.1007/bf00245821) ↗
  57. Zombori, Z., Urban, J., Brown, C.E.: Prolog technology reinforcement learning prover. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. pp. 489–507. Springer International Publishing, Cham (2020) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zombori-2019-finding-longer-proofs/