{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T21:49:56Z","timestamp":1775771396087,"version":"3.50.1"},"reference-count":27,"publisher":"MDPI AG","issue":"4","license":[{"start":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T00:00:00Z","timestamp":1712102400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["12071282"],"award-info":[{"award-number":["12071282"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"<jats:p>The application of contemporary artificial intelligence techniques to address geometric problems and automated deductive proofs has always been a grand challenge to the interdisciplinary field of mathematics and artificial intelligence. This is the fourth article in a series of our works, in our previous work, we established a geometric formalized system known as FormalGeo. Moreover, we annotated approximately 7000 geometric problems, forming the FormalGeo7k dataset. Despite the fact that FGPS (Formal Geometry Problem Solver) can achieve interpretable algebraic equation solving and human-like deductive reasoning, it often experiences timeouts due to the complexity of the search strategy. In this paper, we introduced FGeo-TP (theorem predictor), which utilizes the language model to predict the theorem sequences for solving geometry problems. The encoder and decoder components in the transformer architecture naturally establish a mapping between the sequences and embedding vectors, exhibiting inherent symmetry. We compare the effectiveness of various transformer architectures, such as BART or T5, in theorem prediction, and implement pruning in the search process of FGPS, thereby improving its performance when solving geometry problems. Our results demonstrate a significant increase in the problem-solving rate of the language model-enhanced FGeo-TP on the FormalGeo7k dataset, rising from 39.7% to 80.86%. Furthermore, FGeo-TP exhibits notable reductions in solution times and search steps across problems of varying difficulty levels.<\/jats:p>","DOI":"10.3390\/sym16040421","type":"journal-article","created":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T08:42:34Z","timestamp":1712133754000},"page":"421","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["FGeo-TP: A Language Model-Enhanced Solver for Euclidean Geometry Problems"],"prefix":"10.3390","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9958-5173","authenticated-orcid":false,"given":"Yiming","family":"He","sequence":"first","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai 200444, China"},{"name":"Institute of Artificial Intelligence, Shanghai University, Shanghai 200444, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-3657-4909","authenticated-orcid":false,"given":"Jia","family":"Zou","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai 200444, China"},{"name":"Institute of Artificial Intelligence, Shanghai University, Shanghai 200444, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5678-7485","authenticated-orcid":false,"given":"Xiaokai","family":"Zhang","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai 200444, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2513-7060","authenticated-orcid":false,"given":"Na","family":"Zhu","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai 200444, China"},{"name":"Institute of Artificial Intelligence, Shanghai University, Shanghai 200444, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2921-3291","authenticated-orcid":false,"given":"Tuo","family":"Leng","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai 200444, China"},{"name":"Institute of Artificial Intelligence, Shanghai University, Shanghai 200444, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2024,4,3]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1038\/s41586-022-05172-4","article-title":"Discovering faster matrix multiplication algorithms with reinforcement learning","volume":"610","author":"Fawzi","year":"2022","journal-title":"Nature"},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"e2123433119","DOI":"10.1073\/pnas.2123433119","article-title":"A neural network solves, explains, and generates university math problems by program synthesis and few-shot learning at human level","volume":"119","author":"Drori","year":"2022","journal-title":"Proc. Natl. Acad. Sci. USA"},{"key":"ref_3","unstructured":"Mundhenk, T.N., Landajuela, M., Glatt, R., Santiago, C.P., Faissol, D.M., and Petersen, B.K. (2021). Symbolic regression via neural-guided genetic programming population seeding. arXiv."},{"key":"ref_4","unstructured":"Polu, S., Han, J.M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. (2022). Formal mathematics statement curriculum learning. arXiv."},{"key":"ref_5","unstructured":"Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R.J., and Anandkumar, A. (2023). Leandojo: Theorem proving with retrieval-augmented language models. arXiv."},{"key":"ref_6","unstructured":"Polu, S., and Sutskever, I. (2020). Generative language modeling for automated theorem proving. arXiv."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Lu, P., Gong, R., Jiang, S., Qiu, L., Huang, S., Liang, X., and Zhu, S.C. (2021). Inter-GPS: Interpretable geometry problem solving with formal language and symbolic reasoning. arXiv.","DOI":"10.18653\/v1\/2021.acl-long.528"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Chen, J., Tang, J., Qin, J., Liang, X., Liu, L., Xing, E.P., and Lin, L. (2021). GeoQA: A geometric question answering benchmark towards multimodal numerical reasoning. arXiv.","DOI":"10.18653\/v1\/2021.findings-acl.46"},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Chen, J., Li, T., Qin, J., Lu, P., Lin, L., Chen, C., and Liang, X. (2022). Unigeo: Unifying geometry logical reasoning via reformulating mathematical expression. arXiv.","DOI":"10.18653\/v1\/2022.emnlp-main.218"},{"key":"ref_10","unstructured":"Zhang, X., Zhu, N., He, Y., Zou, J., Huang, Q., Jin, X., Guo, Y., Mao, C., Zhu, Z., and Yue, D. (2023). FormalGeo: The First Step Toward Human-like IMO-level Geometric Automated Reasoning. arXiv."},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Hao, Y., Zhang, M., Yin, F., and Huang, L.L. (2022, January 21\u201325). PGDP5K: A diagram parsing dataset for plane geometry problems. Proceedings of the 2022 26th International Conference on Pattern Recognition (ICPR), IEEE, Montreal, QC, Canada.","DOI":"10.1109\/ICPR56361.2022.9956397"},{"key":"ref_12","unstructured":"Gelernter, H. (1995). Computers & Thought, MIT Press."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","article-title":"Plane geometry theorem proving using forward chaining","volume":"6","author":"Nevins","year":"1975","journal-title":"Artif. Intell."},{"key":"ref_14","first-page":"159","article-title":"On the decision problem and the mechanization of theorem proving in elementary geometry","volume":"21","year":"1978","journal-title":"Sci. Sin."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BF01531326","article-title":"Automated production of traditional proofs for theorems in Euclidean geometry I. The Hilbert intersection point theorems","volume":"13","author":"Zhang","year":"1995","journal-title":"Ann. Math. Artif. Intell."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Seo, M., Hajishirzi, H., Farhadi, A., Etzioni, O., and Malcolm, C. (2015, January 17\u201321). Solving geometry problems: Combining text and diagram interpretation. Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, Lisbon, Portugal.","DOI":"10.18653\/v1\/D15-1171"},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Wu, Q., Zhang, Q., Fu, J., and Huang, X.J. (2020, January 16\u201320). A knowledge-aware sequence-to-tree network for math word problem solving. Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), ELECTR NETWORK.","DOI":"10.18653\/v1\/2020.emnlp-main.579"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Sun, T., Shao, Y., Qiu, X., Guo, Q., Hu, Y., Huang, X., and Zhang, Z. (2020). Colake: Contextualized language and knowledge embedding. arXiv.","DOI":"10.18653\/v1\/2020.coling-main.327"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Liang, Z., Zhang, J., Wang, L., Qin, W., Lan, Y., Shao, J., and Zhang, X. (2021). Mwp-bert: Numeracy-augmented pre-training for math word problem solving. arXiv.","DOI":"10.18653\/v1\/2022.findings-naacl.74"},{"key":"ref_20","unstructured":"Cao, J., and Xiao, J. (2022, January 12\u201317). An augmented benchmark dataset for geometric question answering through dual parallel text encoding. Proceedings of the 29th International Conference on Computational Linguistics, Gyeongju, Republic of Korea."},{"key":"ref_21","first-page":"6000","article-title":"Attention is all you need","volume":"30","author":"Vaswani","year":"2017","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"ref_22","first-page":"3104","article-title":"Sequence to sequence learning with neural networks","volume":"27","author":"Sutskever","year":"2014","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Lewis, M., Liu, Y., Goyal, N., Ghazvininejad, M., Mohamed, A., Levy, O., Stoyanov, V., and Zettlemoyer, L. (2019). Bart: Denoising sequence-to-sequence pre-training for natural language generation, translation, and comprehension. arXiv.","DOI":"10.18653\/v1\/2020.acl-main.703"},{"key":"ref_24","first-page":"1","article-title":"Exploring the limits of transfer learning with a unified text-to-text transformer","volume":"21","author":"Raffel","year":"2020","journal-title":"J. Mach. Learn. Res."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Xue, L., Constant, N., Roberts, A., Kale, M., Al-Rfou, R., Siddhant, A., Barua, A., and Raffel, C. (2020). mT5: A massively multilingual pre-trained text-to-text transformer. arXiv.","DOI":"10.18653\/v1\/2021.naacl-main.41"},{"key":"ref_26","unstructured":"Chung, H.W., Hou, L., Longpre, S., Zoph, B., Tay, Y., Fedus, W., Li, Y., Wang, X., Dehghani, M., and Brahma, S. (2022). Scaling instruction-finetuned language models. arXiv."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"528","DOI":"10.3390\/info2030528","article-title":"Pearson-Fisher chi-square statistic revisited","volume":"2","author":"Pamfil","year":"2011","journal-title":"Information"}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/16\/4\/421\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T14:22:53Z","timestamp":1760106173000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/16\/4\/421"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,3]]},"references-count":27,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2024,4]]}},"alternative-id":["sym16040421"],"URL":"https:\/\/doi.org\/10.3390\/sym16040421","relation":{},"ISSN":["2073-8994"],"issn-type":[{"value":"2073-8994","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,3]]}}}