Abstract
We describe a purely image-based method for finding geometric constructions with a ruler and compass in the Euclidea geometric game. The method is based on adapting the Mask R-CNN state-of-the-art visual recognition neural architecture and adding a tree-based search procedure to it. In a supervised setting, the method learns to solve all 68 kinds of geometric construction problems from the first six level packs of Euclidea with an average 92% accuracy. When evaluated on new kinds of problems, the method can solve 31 of the 68 kinds of Euclidea problems. We believe that this is the first time that purely image-based learning has been trained to solve geometric construction problems of this difficulty.
This work was partly supported by the European Regional Development Fund under the projects IMPACT and AI&Reasoning (reg. no. CZ.02.1.01/0.0/0.0/15_003/0000468 and CZ.02.1.01/0.0/0.0/15_003/0000466) and the ERC Consolidator grant SMART no. 714034.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Project webpage. https://data.ciirc.cvut.cz/public/projects/2021GeometryReasoning
Euclidea. https://www.euclidea.xyz
He K., Gkioxari G., Dollár P., Girshick, R.: Mask R-CNN. In: 2017 IEEE International Conference on Computer Vision (ICCV) (2017)
Seo, M.J., Hajishirzi, H., Farhadi, A., Etzioni, O.: Diagram understanding in geometry questions. In: American Association for Artificial Intelligence (2014)
Seo, M., Hajishirzi, H., Farhadi, A., Etzioni, O., Malcolm, C.: Solving geometry problems: combining text and diagram interpretation. Association for Computational Linguistics (2015)
Quaresma, P.: Thousands of Geometric Problems for Geometric Theorem Provers (TGTP). Springer, Heidelberg (2011)
Vesna, M.: ArgoTriCS – automated triangle construction solver. J. Exper. Theor. Artif. Intell. 29(2), 247–271 (2017)
Balbiani, P., Cerro, L.F.: Affine Geometry of Collinearity and Conditional Term Rewriting. Springer, Heidelberg (1995)
Chou, S.C., Gao, X.S., Zhang, J.Z.: A deductive database approach to automated geometry theorem proving and discovering. J. Autom. Reasoning 25, 219–246 (2000)
Gao, X.: Transcendental functions and mechanical theorem proving in elementary geometries. J. Autom. Reasoning 6, 403–417 (1990)
Deepak, K.: Using Gröbner bases to reason about geometry problems. J. Symbolic Comput. 2(4), 399–408 (1986)
Chou, S.C., Gao, X.S., Zhang, J.: Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems (1994)
McCune, W., Wos, L.: Otter: the CADE-13 competition incarnations. J. Autom. Reasoning 18(2), 211–220 (1997)
McCune, W.: Prover9 and Mace4. http://www.cs.unm.edu/~mccune/prover9/
Beeson, M., Wos, L.: Finding proofs in Tarskian geometry. J. Autom. Reasoning 58(1), 201–207 (2017)
Durdevic, S.S., Narboux, J., Janicic, P.: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry. Ann. Math. Artif. Intell. 74(3–4), 249–269 (2015)
Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers, Dordrecht (1992)
Beeson, M., Narboux, J., Wiedijk, F.: Proof-checking Euclid. Ann. Math. Artif. Intell. 85, 213–257 (2019). https://doi.org/10.1007/s10472-018-9606-x
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.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 448–463. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_29
Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., Norrish, M.: TacticToe: learning to prove with tactics. J. Autom. Reasoning 65(2), 257–286 (2021)
Hosang, J., Benenson, R., Schiele, B.: Learning non-maximum suppression. In: Conference on Computer Vision and Pattern Recognition (CVPR) (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Macke, J., Sedlar, J., Olsak, M., Urban, J., Sivic, J. (2021). Learning to Solve Geometric Construction Problems from Images. In: Kamareddine, F., Sacerdoti Coen, C. (eds) Intelligent Computer Mathematics. CICM 2021. Lecture Notes in Computer Science(), vol 12833. Springer, Cham. https://doi.org/10.1007/978-3-030-81097-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-81097-9_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-81096-2
Online ISBN: 978-3-030-81097-9
eBook Packages: Computer ScienceComputer Science (R0)