×

Portfolio theorem proving and prover runtime prediction for geometry. (English) Zbl 1431.68123

Summary: In recent years, portfolio problem solving found many applications in automated reasoning, primarily in SAT solving and in automated and interactive theorem proving. Portfolio problem solving is an approach in which for an individual instance of a specific problem, one particular, hopefully most appropriate, solving technique is automatically selected among several available ones and used. The selection usually employs machine learning methods. To our knowledge, this approach has not been used in automated theorem proving in geometry so far and it poses a number of new challenges. In this paper we propose a set of features which characterize a specific geometric theorem, so that machine learning techniques can be used in geometry. Relying on these features and using different machine learning techniques, we constructed several portfolios for theorem proving in geometry and also runtime prediction models for provers involved. The evaluation was performed on two corpora of geometric theorems: one coming from geometric construction problems and one from a benchmark set of the GeoGebra tool. The obtained results show that machine learning techniques can be useful in automated theorem proving in geometry, while there is still room for further progress.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
51M04 Elementary problems in Euclidean geometries
68T05 Learning and adaptive systems in artificial intelligence
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Aigner, M., Biere, A., Kirsch, C.M., Niemetz, A., Preiner, M.: Analysis of portfolio-style parallel SAT solving on current multi-core architectures. In: Fourth Pragmatics of SAT workshop, a workshop of the SAT 2013 conference. POS-13, pp. 28-40 (2013)
[2] Alama, J.; Heskes, T.; Kühlwein, D.; Tsivtsivadze, E.; Urban, J., Premise selection for mathematics by corpus analysis and kernel methods, J. Autom. Reason., 52, 191-213, (2014) · Zbl 1315.68217
[3] Aloul, F., Sierawski, B., Sakallah, K.: A tool for measuring progress of backtrack-search solvers. In: Theory and Applications of Satisfiability Testing - SAT 2002 (2002)
[4] Amadini, R.; Gabbrielli, M.; Mauro, J., Sunny: a lazy portfolio approach for constraint solving, Theory Pract. Logic Program., 14, 509-524, (2014) · Zbl 1307.68077
[5] Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel SAT solving. In: Theory and Applications of Satisfiability Testing - SAT 2012, pp. 200-213. Springer, Berlin (2012)
[6] Bartz-Beielstein, T., Lasarczyk, C.W.G., Preuss, M.: Sequential parameter optimization. In: 2005 IEEE Congress on Evolutionary Computation, vol. 1, pp. 773-780 (2005) · Zbl 1208.90166
[7] Beeson, M.; Wos, L., Finding proofs in Tarskian geometry, J. Autom. Reason., 58, 181-207, (2017) · Zbl 1414.68100
[8] Botana, F.; Hohenwarter, M.; Janičić, P.; Kovács, Z.; Petrović, I.; Recio, T.; Weitzhofer, S., Automated theorem proving in GeoGebra: current achievements, J. Autom. Reason., 55, 39-59, (2015) · Zbl 1356.68181
[9] Botana, F.; Kovács, Z., A singular web service for geometric computations, Ann. Math. Artif. Intell., 74, 359-370, (2015) · Zbl 1330.68336
[10] Chou, S.-C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Dordrecht (1987) · Zbl 0661.14037
[11] Chou, S.-C., Gao, X.-S.: Automated reasoning in geometry. In: Handbook of Automated Reasoning. Elsevier and MIT Press (2001) · Zbl 1011.68128
[12] Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994) · Zbl 0941.68503
[13] Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: An introduction to geometry expert. In: CADE 13, Volume 1104 of Lecture Notes in Artificial Intelligence. Springer, Berlin (1996) · Zbl 1412.68214
[14] Czajka, Ł; Kaliszyk, C., Hammer for Coq automation for dependent type theory, J. Autom. Reason., 61, 423-453, (2018) · Zbl 1448.68458
[15] Duda, R., Hart, P., Stork, D.: Pattern Classification. Wiley-Interscience, New York (2000) · Zbl 0968.68140
[16] Duncan, H., Bundy, A., Levine, J., Storkey, A., Pollet, M.: The use of data-mining for the automatic formation of tactics. In: Proceedings of the Workshop on Computer-Supported Mathematical Theory Development, IJCAR 2004 (2004)
[17] Färber, M., Brown, C.: Internal guidance for Satallax. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning, pp. 349-361. Springer International Publishing (2016) · Zbl 1475.68435
[18] Färber, M., Kaliszyk, C.: Random forests for premise selection. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems, pp. 325-340. Springer International Publishing (2015) · Zbl 1471.68307
[19] Fink, E.: How to solve it automatically: selection among problem-solving methods. In: Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems, pp. 128-136. AAAI Press (1998)
[20] Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T., Schneider, M.T., Ziller, S.: A portfolio solver for answer set programming: preliminary report. In: Logic Programming and Nonmonotonic Reasoning, LPNMR 2011, pp. 352-357. Springer, Berlin (2011)
[21] Gelernter, H.: Realisation of a geometry-proving machine. In: Automation of Reasoning. Springer, Berlin (1983)
[22] Gross, J.: Linear Regression. Springer, Berlin (2003) · Zbl 1039.62061
[23] Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: Principles and Practice of Constraint Programming - CP 2010, pp. 252-265. Springer, Berlin (2010)
[24] Haim, S., Walsh, T.: Online estimation of SAT solving runtime. In: Theory and Applications of Satisfiability Testing - SAT 2008, pp. 133-138. Springer, Berlin (2008) · Zbl 1138.68540
[25] Hastie, T., Tibshirani, R., Friedman, J.: The Elements of Statistical Learning. Springer, New York (2001) · Zbl 0973.62007
[26] Helmert, M., Röger, G., Karpas, E.: Fast downward stone soup: a baseline for building planner portfolios. In: Proceedings of the ICAPS 2011 Workshop of AI Planning and Learning (2011)
[27] Ho, T.K.: Random decision forests. In: Proceedings of the Third International Conference on Document Analysis and Recognition (Volume 1), ICDAR ’95, pp. 278-282. IEEE Computer Society, Los Alamitos (1995)
[28] Hohenwarter, M.: GeoGebra: ein softwaresystem für dynamische geometrie und algebra der ebene. Master’s Thesis, Paris Lodron University. Salzburg, Austria (2002)
[29] Hurley, B., Kotthoff, L., Malitsky, L., O’Sullivan, B.: Proteus: a hierarchical portfolio of solvers and transformations. In: Integration of AI and OR Techniques in Constraint Programming, CPAIOR 2014, pp. 301-317. Springer International Publishing (2014) · Zbl 06298800
[30] Hurley, B., O’Sullivan, B.: Statistical regimes and runtime prediction. In: Proceedings of the 24th International Conference on Artificial Intelligence, pp. 318-324. AAAI Press (2015)
[31] Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Learning and Intelligent Optimization, LION 5, pp. 507-523. Springer, Berlin (2011)
[32] Hutter, F., Hoos, H.H., Leyton-Brown, K.: Parallel algorithm configuration. In: Learning and Intelligent Optimization, LION 6, pp. 55-70. Springer, Berlin (2012)
[33] Hutter, F., Hoos, H.H., Leyton-Brown, K., Murphy, K.: Time-bounded sequential parameter optimization. In: Learning and Intelligent Optimization, LION 4, pp. 281-298. Springer, Berlin (2010)
[34] Hutter, F.; Lin, X.; Hoos, HH; Leyton-Brown, K., Algorithm runtime prediction: methods & evaluation, Artif. Intell., 206, 79-111, (2014) · Zbl 1334.68185
[35] Jakubuv, J., Urban, J.: Blistrtune: hierarchical invention of theorem proving strategies. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Cpp. 2017, pp. 43-52 (2017)
[36] Janičić, P.: GCLC - a tool for constructive euclidean geometry and more than that. In: Proceedings of International Congress of Mathematical Software (ICMS 2006), Volume 4151 of Lecture Notes in Computer Science, pp. 58-73. Springer, Berlin (2006) · Zbl 1230.51024
[37] Janičić, P., Quaresma, P.: System description: GCLCprover + GeoThms. In: International Joint Conference on Automated Reasoning (IJCAR-2006), Volume 4130 of Lecture Notes in Artificial Intelligence, pp. 145-150. Springer, Berlin (2006)
[38] Janičić, P.; Narboux, J.; Quaresma, P., The area method: a recapitulation, J. Autom. Reason., 48, 489-532, (2012) · Zbl 1242.68281
[39] Janičić, P., Geometry constructions language, J. Autom. Reason., 44, 3-24, (2010) · Zbl 1185.68626
[40] Janičić, P., Quaresma, P.: Automatic verification of regular constructions in dynamic geometry systems. In: Automated Deduction in Geometry, Volume 4869 of Lecture Notes in Artificial Intelligence, pp. 39-51. Springer, Berlin (2007) · Zbl 1195.68092
[41] Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming, CP’11, pp. 454-469. Springer, Berlin (2011)
[42] Kaliszyk, C., Urban, J.: Femalecop: fairly efficient machine learning connection prover. In: Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings, pp. 88-96 (2015) · Zbl 1471.68312
[43] Kaliszyk, C., Urban, J., Vyskocil, J.: Efficient semantic features for automated reasoning over large theories. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 3084-3090 (2015)
[44] Komendantskaya, E., Heras, J., Grov, G.: Machine learning in proof general: interfacing interfaces. In: Proceedings 10th International Workshop on User Interfaces for Theorem Provers, UITP 2012, pp. 15-41 (2012)
[45] Kotthoff, L.; Gent, IP; Miguel, I., An evaluation of machine learning in algorithm selection for search problems, AI Commun., 25, 257-270, (2012)
[46] Kovács, Z.: Computer Based Conjectures and Proofs in Teaching Euclidean Geometry. PhD Thesis Computer Based Johannes Kepler University. Linz, Austria (2015)
[47] Kovács, Z., Parisse, B.: Giac and GeoGebra - improved Gröbner basis computations. In: Computer Algebra and Polynomials, Lecture Notes in Computer Science, pp. 126-138. Springer, Berlin (2015) · Zbl 1434.68708
[48] Kovács, Z., Recio, T., Weitzhofer, S.: Implementing theorem proving in GeoGebra by using exact check of a statement in a bounded number of test cases. In: Proceedings EACA 2012 Libro de resúmenes del XIII Encuentro de Álgebra Computacional y Aplicaciones, pp. 123-126. Universidad de Alcalá (2012)
[49] Krstajić, D.; Buturović, LJ; Leahy, DE; Thomas, S., Cross-validation pitfalls when selecting and assessing regression and classification models, J. Cheminf., 6, 1-15, (2014)
[50] Kühlwein, D.; Urban, J., Males: A framework for automatic tuning of automated theorem provers, J. Autom. Reason., 55, 91-116, (2015) · Zbl 1356.68193
[51] Kullback, S.; Leibler, R., On information and sufficiency, Ann. Math. Stat., 22, 79-86, (1951) · Zbl 0042.38403
[52] Lindauer, M., Hoos, H., Hutter, F.: From sequential algorithm selection to parallel portfolio selection. In: Learning and Intelligent Optimization, LION 9, pp. 1-16. Springer International Publishing (2015)
[53] Lobjois, L., Lemaître, M.: Branch and bound algorithm selection by performance prediction. In: Proceedings of the Fifteenth National/Tenth Conference on Artificial Intelligence/Innovative Applications of Artificial Intelligence, AAAI’98/IAAI’98, pp. 353-358. American Association for Artificial Intelligence (1998)
[54] Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Non-model-based algorithm portfolios for SAT. In: Theory and Applications of Satisfiability Testing, SAT 2011 (2011)
[55] Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Parallel SAT solver selection and scheduling. In: Principles and Practice of Constraint Programming, CP 2012, pp. 512-526. Springer, Berlin (2012)
[56] Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Boosting sequential solver portfolios: knowledge sharing and accuracy prediction. In: Learning and Intelligent Optimization, LION 7, pp. 153-167. Springer, Berlin (2013)
[57] Marić, F., Petrović, I., Petrović, D., Janičić, P.: Formalization and implementation of algebraic methods in geometry. In: Proceedings First Workshop on CTP Components for Educational Software, Volume 79 of Electronic Proceedings in Theoretical Computer Science, pp. 63-81. Open Publishing Association (2012)
[58] Marinković, V., On-line compendium of triangle construction problems with automatically generated solutions, The Teaching of Mathematics, XVIII, 29-44, (2015)
[59] Marinković, V., ArgoTriCS - automated triangle construction solver, J. Exp. Theor. Artif. Intell., 29, 247-271, (2017)
[60] Marinković, V., Janičić, P.: Towards understanding triangle construction problems. In: Intelligent Computer Mathematics - CICM 2012, Volume 7362 of Lecture Notes in Computer Science. Springer, Berlin (2012) · Zbl 1359.68265
[61] Marinković, V., Janičić, P., Schreck, P.: Solving geometric construction problems supported by theorem proving. In: Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), pp. 121-146. CISUC Technical report TR 2014/01, University of Coimbra (2014)
[62] Menouer, T., Baarir, S.: Parallel learning portfolio-based solvers. In: International Conference on Computational Science, ICCS 2017, volume 108 (2017)
[63] Murphy, K.P.: Machine learning: a probabilistic perspective. MIT Press, Cambridge (2012) · Zbl 1295.68003
[64] Nikolić, M., Marić, F., Janičić, P.: Instance-based selection of policies for SAT solvers. In: Theory and Applications of Satisfiability Testing - SAT 2009, Volume 5584 of Lecture Notes in Computer Science, pp. 326-340. Springer, Berlin (2009)
[65] Nikolić, M., Marić, F., Janičić, P.: Simple algorithm portfolio for SAT. Artif. Intell. Rev., pp. 1-9 (2012)
[66] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Volume 2283 of Lecture Notes in Computer Science. Springer (2002) · Zbl 0994.68131
[67] Nudelman, E., Leyton-Brown, K., Hoos, H.H., Devkar, A., Shoham, Y.: Understanding random SAT: beyond the clauses-to-variables ratio. In: Principles and Practice of Constraint Programming - CP 2004, pp. 438-452. Springer, Berlin (2004) · Zbl 1152.68569
[68] O’Mahony, E., Hebrard, E., Holland, A., Nugent, C.: Using case-based reasoning in an algorithm portfolio for constraint solving. In: Irish Conference on Artificial Intelligence and Cognitive Science (2008)
[69] Paulson, L.C.: The Isabelle reference manual (2006)
[70] Preiner, J.: Introducing Dynamic Mathematics Software to Mathematics Teachers: The Case of GeoGebra. PhD Thesis, Paris Lodron University. Salzburg, Austria (2008)
[71] Pulina, L., Tacchella, A.: A multi-engine solver for quantified boolean formulas. In: Principles and Practice of Constraint Programming - CP 2007, pp. 574-589. Springer, Berlin (2007)
[72] Pulina, L.; Tacchella, A., A self-adaptive multi-engine solver for quantified boolean formulas, Constraints, 14, 80-116, (2009) · Zbl 1183.68589
[73] Radhakrishna Rao, C.: Linear Statistical Inference and its Applications. Wiley, New York (1973) · Zbl 0256.62002
[74] Riazanov, A.; Voronkov, A., The design and implementation of Vampire, AI Commun., 15, 91-110, (2002) · Zbl 1021.68082
[75] Rizzini, M., Fawcett, C., Vallati, M., Gerevini, A.E., Hoos, H.H.: Static and dynamic portfolio methods for optimal planning: an empirical analysis. Int. J. Artif. Intell. Tools 26(01) (2017)
[76] Roberts, M.; Howe, A., Learning from planner performance, Artif. Intell., 173, 536-561, (2009) · Zbl 1191.68640
[77] Samulowitz, H., Memisevic, R.: Learning to solve QBF. In: Proceedings of the 22Nd National Conference on Artificial Intelligence, AAAI ’07, pp. 255-260. AAAI Press (2007)
[78] Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2,3) (2002) · Zbl 1020.68084
[79] Seipp, J., Sievers, S., Helmert, M., Hutter, F.: Automatic configuration of sequential planning portfolios. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence AAAI’15, pp. 3364-3370 AAAI Press (2015)
[80] Sonobe, T., Kondoh, S., Inaba, M.: Community branching for parallel portfolio SAT solvers. In: Theory and Applications of Satisfiability Testing - SAT 2014, pp. 188-196, Cham. Springer International Publishing (2014) · Zbl 1423.68472
[81] Stojadinović, M.; Marić, F., meSAT: multiple encodings of CSP to SAT, Constraints, 19, 380-403, (2014) · Zbl 1316.90049
[82] Ðuđević, SS; Narboux, J.; Janičić, P., Automated generation of machine verifiable and readable proofs: A case study of Tarski’s geometry, Ann. Math. Artif. Intell., 74, 249-269, (2015) · Zbl 1327.68206
[83] Stojanović, S., Pavlović, V., Janičić, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, Volume 6877 of Lecture Notes in Computer Science, Springer (2011) · Zbl 1252.68264
[84] The Coq development team. The Coq proof assistant reference manual, Version 8.7.2. \(r\)2 Project (2018)
[85] Trgalova, J., Kortenkamp, U., Jahn, A.P., Libbrecht, P., Mercat, C., Recio, T.: Sophie Soury-Lavergne I2GEO.NET. Seventh Congress of the European Society for Research in Mathematics Education, Rzeszow, Poland, pp. 2986-2987. https://hal.archives-ouvertes.fr/hal-01045138 (2011)
[86] Urban, J.: Blistr: the blind strategymaker. In: Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, pp. 312-319 (2015)
[87] Urban, J., Vyskočil, J., Štěpánek, P.: Malecop machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods, pp. 263-277. Springer (2011) · Zbl 1332.68206
[88] Wagner, M.; Lindauer, M.; Mısır, M.; Nallaperuma, S.; Hutter, F., A case study of algorithm selection for the traveling thief problem, J. Heuristics, 24, 295-320, (2017)
[89] Wang, D.: Geother 1.1: handling and proving geometric theorems automatically. In: Automated Deduction in Geometry, Volume 2930 of Lecture Notes in Artificial Intelligence, pp. 194-215. Springer (2004) · Zbl 1202.68390
[90] Wenzel, M., READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking, Electronic Proceedings in Theoretical Computer Science, 118, 57-71, (2013)
[91] Wernick, W., Triangle constructions with three located points, Math. Mag., 55, 227-230, (1982) · Zbl 0497.51016
[92] Lin, X.; Hutter, F.; Hoss, HH; Leyton-Brown, K., SATzilla: Portfolio-based algorithm selection for SAT, J. Artif. Intell. Res., 32, 565-606, (2008) · Zbl 1182.68272
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.