Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems 1

Abstract

This paper introduces a benchmark problem library for mechanized mathematics including computer algebra and automated theorem proving. The library consists of pre-university mathematical problems taken from exercise problem books, university entrance examinations, and the International Mathematical Olympiads. The subject areas include real algebra, geometry, number theory, pre-calculus, calculus, and combinatorics. It thus includes problems in various areas of pre-university mathematics and with a variety of difficulty. Unlike other existing benchmark libraries, this one contains problems that are formalized so that they are obtainable as the result of mechanical translation of the original problems expressed in natural language. In other words, the library is designed to support the integration of the technologies of mechanized mathematics and natural language processing towards the goal of end-to-end automatic mathematical problem solving. The paper also presents preliminary experimental results of our prototype reasoning component of an end-to-end system on the library. The library is publicly available through the Internet.

Keywords

Mechanized mathematics benchmark library

Get full access to this article

View all access options for this article.

References

Akbarpour and

L.C.

Paulson, MetiTarski: An automatic theorem prover for real-valued special functions, Journal of Automated Reasoning44(3) (2010), 175–205. doi:10.1007/s10817-009-9149-2.

N.H.

Arai, Tractability of cut-free Gentzen type propositional calculus with permutation inference, Theoretical Computer Science170(1) (1996), 129–144. doi:10.1016/S0304-3975(96)80704-3.

N.H.

Arai and

Masukawa, How to find symmetries hidden in combinatorial problems, in: Proceedings of the Eighth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 2000.

Atkey,

Johann and

Kennedy, Abstraction and invariance for algebraically indexed types, in: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’13, ACM, New York, NY, USA, 2013, pp. 87–100, http://doi.acm.org/10.1145/2429069.2429082.

Avigad,

R.Y.

Lewis and

Roux, A heuristic prover for real inequalities, Journal of Automated Reasoning56(3) (2016), 367–386. doi:10.1007/s10817-015-9356-y.

Barrett,

Stump and

Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), 2010, www.SMT-LIB.org.

D.G.

Bobrow, Natural language input for a computer problem solving system, PhD thesis, Massachusetts Institute of Technology, 1964.

Bos, Wide-coverage semantic analysis with boxer, in: Semantics in Text Processing. STEP 2008 Conference Proceedings. Research in Computational Semantics,

Bos and

Delmonte, eds, College Publications, 2008, pp. 277–286. doi:10.3115/1626481.1626503.

Bradford,

J.H.

Davenport,

England,

McCallum and

Wilson, Truth table invariant cylindrical algebraic decomposition, Journal of Symbolic Computation76 (2016), 1–35. doi:10.1016/j.jsc.2015.11.002.

10.

C.W.

Brown, Open non-uniform cylindrical algebraic decompositions, in: Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation. ISSAC ’15, ACM, New York, NY, USA, 2015, pp. 85–92. doi:10.1145/2755996.2756654.

11.

Chen and

Moreno Maza, Quantifier elimination by cylindrical algebraic decomposition based on regular chains, Journal of Symbolic Computation75(C) (2016), 74–93. doi:10.1016/j.jsc.2015.11.008.

12.

Clark and

J.R.

Curran, Wide-coverage efficient statistical parsing with CCG and log-linear models, Computational Linguistics33 (2007). doi:10.1162/coli.2007.33.4.493.

13.

J.H.

Davenport and

Heintz, Real quantifier elimination is doubly exponential, Journal of Symbolic Computation5(1–2) (1988), 29–35, http://www.sciencedirect.com/science/article/pii/S074771718880004X. doi:10.1016/S0747-7171(88)80004-X.

14.

L.A.

Dennis,

Gow and

Schürmann, Challenge Problems for Inductive Theorem Provers v1.0, Technical report ULCS-07-004, University of Liverpool, Department of Computer Science, 2007.

15.

England and

J.H.

Davenport, Experience with heuristics, benchmarks & standards for cylindrical algebraic decomposition, in: Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation Co-Located with 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016), Timisoara, Romania, September 24, 2016,

Ábrahám,

J.H.

Davenport and

Fontaine, eds, CEUR Workshop Proceedings, Vol. 1804, CEUR-WS.org, 2016, pp. 24–31, http://ceur-ws.org/Vol-1804/paper-06.pdf.

16.

Fukasaku,

Iwane and

Sato, Improving a CGS-QE algorithm, in: Revised Selected Papers of the 6th International Conference on Mathematical Aspects of Computer and Information Sciences – Volume 9582. MACIS 2015, Springer-Verlag Inc., New York, NY, USA, 2016, pp. 231–235.

17.

J.P.

Gelb, Experiments with a natural language problem-solving system, in: Proceedings of the 2nd International Joint Conference on Artificial Intelligence. IJCAI’71, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1971, pp. 455–462.

18.

Grabowski,

Korniłowicz and

Naumowicz, Mizar in a nutshell, Journal of Formalized Reasoning3(2) (2010), 153–245.

19.

Harrison, Without loss of generality, in: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Proceedings, Munich, Germany, August 17–20, 2009, 2009, pp. 43–59. doi:10.1007/978-3-642-03359-9_3.

20.

H.H.

Hoos and

Stützle, SATLIB: An Online Resource for Research on SAT, IOS Press, 2000, pp. 283–292.

21.

M.J.

Hosseini,

Hajishirzi,

Etzioni and

Kushman, Learning to solve arithmetic word problems with verb categorization, in: Proceedings of the 2014 Conference on Empirical Methods in Natural Language Processing, EMNLP, Doha, Qatar, October 25–29, 2014, A meeting of SIGDAT, a Special Interest Group of the ACL, 2014, pp. 523–533, http://aclweb.org/anthology/D/D14/D14-1058.pdf. doi:10.3115/v1/D14-1058.

22.

Iwane and

Anai, Formula simplification for real quantifier elimination using geometric invariance, in: Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC-2017), 2017, to appear.

23.

Iwane,

Matsuzaki,

Arai and

Anai, Automated natural language geometry math problem solving by real quantier elimination, in: Proceedings of the 10th International Workshop on Automated Deduction (ADG2014), 2014, pp. 75–84.

24.

Iwane,

Yanami,

Anai and

Yokoyama, An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination, Theor. Comput. Sci.479 (2013), 43–69. doi:10.1016/j.tcs.2012.10.020.

25.

Kaliszyk,

Sutcliffe and

Rabe, TH1: The TPTP typed higher-order form with rank-1 polymorphism, in: Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), 2016, pp. 41–55.

26.

Kerber and

Pollet, A tough nut for mathematical knowledge management, in: Mathematical Knowledge Management, Springer, 2006, pp. 81–95. doi:10.1007/11618027_6.

27.

Kobayashi,

Iwane,

Matsuzaki and

Anai, Efficient subformula orders for real quantifier elimination of non-prenex formulas, in: Mathematical Aspects of Computer and Information Sciences – 6th International Conference, MACIS 2015, Revised Selected Papers, Berlin, Germany, November 11–13, 2015, pp. 236–251. doi:10.1007/978-3-319-32859-1_21.

28.

Koncel-Kedziorski,

Hajishirzi,

Sabharwal,

Etzioni and

Ang, Parsing algebraic word problems into equations, Transactions of the Association for Computational Linguistics3 (2015), 585–597, https://transacl.org/ojs/index.php/tacl/article/view/692.

29.

Kushman,

Artzi,

Zettlemoyer and

Barzilay, Learning to automatically solve algebra word problems, in: Proceedings of the 52nd Annual Meeting of the Association for Computational Linguistics, Volume 1: Long Papers, Association for Computational Linguistics, Baltimore, Maryland, 2014, pp. 271–281, http://www.aclweb.org/anthology/P14-1026. doi:10.3115/v1/P14-1026.

30.

Kwiatkowksi,

Zettlemoyer,

Goldwater and

Steedman, Inducing probabilistic CCG grammars from logical form with higher-order unification, in: Proceedings of the 2010 Conference on Empirical Methods in Natural Language Processing, Association for Computational Linguistics, 2010, pp. 1223–1233.

31.

Matsuzaki,

Ito,

Iwane,

Anai and

N.H.

Arai, Semantic parsing of pre-university math problems, in: Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics. Association for Computational Linguistics, 2017, to appear.

32.

Matsuzaki,

Iwane,

Anai and

N.H.

Arai, The most uncreative examinee: A first step toward wide coverage natural language math problem solving, in: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014, pp. 1098–1104.

33.

Matsuzaki,

Iwane,

Kobayashi,

Zhan,

Fukasaku,

Kudo,

Anai and

N.H.

Arai, Race against the teens – benchmarking mechanized math on pre-university problems, in: Automated Reasoning – 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27,

Olivetti and

Tiwari, eds, Proceedings. Lecture Notes in Computer Science, Vol. 9706, Springer, 2016, pp. 213–227, July 2, 2016.

34.

Matsuzaki,

Kobayashi and

N.H.

Arai, An information-processing account of representation change: International mathematical olympiad problems are hard not only for humans, in: Proceedings of the 38th Annual Conference of the Cognitive Science Society, Cognitive Science Society, 2016, pp. 2297–2302.

35.

McCarthy, A tough nut for proof procedures, Technical report Stanford Artificial Intelligence Project Memo 16, Stanford University, 1964.

36.

Mitra and

Baral, Learning to use formulas to solve simple arithmetic problems, in: Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, 2016, pp. 2144–2153.

37.

Quaresma, Thousands of geometric problems for geometric theorem provers (TGTP), in: Automated Deduction in Geometry,

Schreck,

Narboux and

Richter-Gebert, eds, Lecture Notes in Computer Science, Vol. 6877, Springer, Berlin Heidelberg, 2011, pp. 169–181. doi:10.1007/978-3-642-25070-5_10.

38.

Raggi,

Bundy,

Grov and

Pease, Automating change of representation for proofs in, Discrete Mathematics (Extended Version). Mathematics in Computer Science10(4) (2016), 429–457.

39.

Roy and

Roth, Solving general arithmetic word problems, in: Conference Proceedings – EMNLP 2015: Conference on Empirical Methods in Natural Language Processing, Association for Computational Linguistics (ACL), 2015, pp. 1743–1752. doi:10.18653/v1/D15-1202.

40.

Shi,

Wang,

C.-Y.

Lin,

Liu and

Rui, Automatically solving number word problems by semantic parsing and reasoning, in: EMNLP,

Màrquez,

Callison-Burch,

Su,

Pighin and

Marton, eds, The Association for Computational Linguistics, 2015, pp. 1132–1142, http://dblp.uni-trier.de/db/conf/emnlp/emnlp2015.html#ShiWLLR15.

41.

Shuppan, 2014, Studyaid D.B. Chart-Shiki database (in Japanese).

42.

Steedman, The Syntactic Process. Bradford Books, MIT Press, Cambridge, 2001.

43.

Strzeboński, A., Cylindrical algebraic decomposition using local projections, Journal of Symbolic Computation76(C) (2016), 36–64. doi:10.1016/j.jsc.2015.11.018.

44.

Sutcliffe, The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0, Journal of Automated Reasoning43(4) (2009), 337–362. doi:10.1007/s10817-009-9143-8.

45.

Sutcliffe,

Stickel,

Schulz, Urban and

Answer, Extraction for TPTP, http://www.cs.miami.edu/~tptp/TPTP/Proposals/AnswerExtraction.html.

46.

Tarski, A Decision Method for Elementary Algebra and Geometry, University of California Press, Berkeley, 1951.

47.

Zhou,

Dai and

Chen, Learn to solve algebra word problems using quadratic programming, in: EMNLP,

Màrquez,

Callison-Burch,

Su,

Pighin and

Marton, eds, The Association for Computational Linguistics, 2015, pp. 817–822, http://dblp.uni-trier.de/db/conf/emnlp/emnlp2015.html#ZhouDC15.