{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:22:13Z","timestamp":1760059333064,"version":"build-2065373602"},"reference-count":51,"publisher":"MDPI AG","issue":"6","license":[{"start":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T00:00:00Z","timestamp":1749254400000},"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>Plane geometry problem solving has been a long-term challenge in mathematical reasoning and symbolic artificial intelligence. With the continued advancement of automated methods, the need for large-scale datasets and rigorous evaluation frameworks has become increasingly critical for benchmarking and guiding system development. However, existing resources often lack sufficient scale, systematic difficulty modeling, and quantifiable, process-based evaluation metrics. To address these limitations, we propose FGeo-Eval, a comprehensive evaluation system for plane geometry problem solving, and introduce the FormalGeo30K dataset, an extended dataset derived from FormalGeo7K. The evaluation system includes a problem completion rate metric PCR to assess partial progress, theorem weight computation to quantify knowledge importance, and a difficulty coefficient based on reasoning complexity. By analyzing problem structures and solution dependencies, this system enables fine-grained difficulty stratification and objective performance measurement. Concurrently, FormalGeo30K expands the dataset to 30,540 formally annotated problems, supporting more robust model training and evaluation. Experimental results demonstrate that the proposed metrics effectively evaluate problem difficulty and assess solver capabilities. With the augmented dataset, the average success rate across all difficulty levels for the FGeo-HyperGNet model increases from 77.43% to 85.01%, while the average PCR increases from 88.57% to 91.79%. These contributions provide essential infrastructure for advancing plane geometry reasoning systems, offering standardized benchmarks for model development and guiding optimization of geometry-solving models.<\/jats:p>","DOI":"10.3390\/sym17060902","type":"journal-article","created":{"date-parts":[[2025,6,9]],"date-time":"2025-06-09T09:13:01Z","timestamp":1749460381000},"page":"902","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["FGeo-Eval: Evaluation System for Plane Geometry Problem Solving"],"prefix":"10.3390","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-6016-7741","authenticated-orcid":false,"given":"Qike","family":"Huang","sequence":"first","affiliation":[{"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":"Institute of Artificial Intelligence, Shanghai University, Shanghai 200444, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fangzhen","family":"Zhu","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, 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":"Institute of Artificial Intelligence, Shanghai University, Shanghai 200444, China"},{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai 200444, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2025,6,7]]},"reference":[{"key":"ref_1","unstructured":"Littman, M.L., Ajunwa, I., Berger, G., Boutilier, C., Currie, M., Doshi-Velez, F., Hadfield, G., Horowitz, M.C., Isbell, C., and Kitano, H. (2022). Gathering strength, gathering storms: The one hundred year study on artificial intelligence (AI100) 2021 study panel report. arXiv."},{"key":"ref_2","unstructured":"Gelernter, H. (1995). Realization of a geometry-theorem proving machine. Computers & Thought, MIT Press."},{"key":"ref_3","first-page":"721","article-title":"The geometry information search system by forward reasoning","volume":"19","author":"Zhang","year":"1996","journal-title":"Chin. J.-Comput.-Chin. Ed."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/BF02328447","article-title":"Basic principles of mechanical theorem proving in elementary geometries","volume":"2","year":"1986","journal-title":"J. Autom. Reason."},{"key":"ref_5","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_6","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_7","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_8","doi-asserted-by":"crossref","first-page":"476","DOI":"10.1038\/s41586-023-06747-5","article-title":"Solving olympiad geometry without human demonstrations","volume":"625","author":"Trinh","year":"2024","journal-title":"Nature"},{"key":"ref_9","unstructured":"Zhang, X., Zhu, N., He, Y., Zou, J., Huang, Q., Jin, X., Guo, Y., Mao, C., Li, Y., and Zhu, Z. (2023). FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving. arXiv."},{"key":"ref_10","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_11","doi-asserted-by":"crossref","unstructured":"Lin, D., and Liu, Z. (1993, January 6\u20138). Some results on theorem proving in geometry over finite fields. Proceedings of the 1993 International Symposium on Symbolic and Algebraic Computation, Kiev, Ukraine.","DOI":"10.1145\/164081.164143"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF00881835","article-title":"Automated reasoning in differential geometry and mechanics using the characteristic set method: Part II. Mechanical theorem proving","volume":"10","author":"Chou","year":"1993","journal-title":"J. Autom. Reason."},{"key":"ref_13","first-page":"193","article-title":"On a finiteness theorem about problems involving inequalities","volume":"7","author":"Wu","year":"1994","journal-title":"J. Syst. Sci. Math. Sci."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Buchberger, B. (1988). Applications of Gr\u00f6bner bases in non-linear computational geometry. Mathematical Aspects of Scientific Software, Springer.","DOI":"10.1007\/978-1-4684-7074-1_3"},{"key":"ref_15","unstructured":"Yang, L., Zhang, J., and Li, C. (1992, January 17\u201319). A prover for parallel numerical verification of a class of constructive geometry theorems. Proceedings of the International Workshop on Memory Management, St. Malo, France."},{"key":"ref_16","unstructured":"Yang, L., and Zhang, J. (1990). Searching dependency between algebraic equations: An algorithm applied to automated reasoning. Technical Report, International Centre for Theoretical Physics."},{"key":"ref_17","unstructured":"Lu, Y. (1998, January 24\u201328). Practical automated reasoning on inequalities: Generic programs for inequality proving and discovering. Proceedings of the Third Asian Technology Conference in Mathematics, Tsukuba, Japan."},{"key":"ref_18","unstructured":"Chou, S.C., Gao, X.S., and Zhang, J.Z. (1993, January 19\u201323). Automated production of traditional proofs for constructive geometry theorems. Proceedings of the [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, QC, Canada."},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., and Zhang, J.Z. (1993, January 6\u20138). Automated geometry theorem proving by vector calculation. Proceedings of the 1993 International Symposium on Symbolic and Algebraic Computation, Kiev, Ukraine.","DOI":"10.1145\/164081.164142"},{"key":"ref_20","unstructured":"Chou, S.C., Gao, X.S., and Zhang, J.Z. (1994). A Collection of 110 Geometry Theorems and Their Machine Produced Proofs Using Full-Angles, Washington State University."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/BF00881858","article-title":"Automated production of traditional proofs in solid geometry","volume":"14","author":"Chou","year":"1995","journal-title":"J. Autom. Reason."},{"key":"ref_22","unstructured":"Chou, S., Gao, X., and Zhang, J. (1994). A Collection of 90 Mechanically Solved Geometry Problems from Non-Euclidean Geometries, Washington State University."},{"key":"ref_23","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_24","doi-asserted-by":"crossref","unstructured":"Sachan, M., Dubey, K., and Xing, E. (2017, January 9\u201311). From textbooks to knowledge: A case study in harvesting axiomatic knowledge from textbooks to solve geometry problems. Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing, Copenhagen, Denmark.","DOI":"10.18653\/v1\/D17-1081"},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Sachan, M., and Xing, E. (2017, January 3\u20134). Learning to solve geometry problems from natural language demonstrations in textbooks. Proceedings of the 6th Joint Conference on Lexical and Computational Semantics (* SEM 2017), Vancouver, BC, Canada.","DOI":"10.18653\/v1\/S17-1029"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Alvin, C., Gulwani, S., Majumdar, R., and Mukhopadhyay, S. (2017, January 22\u201324). Synthesis of Solutions for Shaded Area Geometry Problems. Proceedings of the Thirtieth International Florida Artificial Intelligence Research Society Conference, Marco Island, FL, USA.","DOI":"10.1007\/978-3-319-61425-0_39"},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"1940005","DOI":"10.1142\/S0218001419400056","article-title":"A framework for solving explicit arithmetic word problems and proving plane geometry theorems","volume":"33","author":"Yu","year":"2019","journal-title":"Int. J. Pattern Recognit. Artif. Intell."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"1940003","DOI":"10.1142\/S0218001419400032","article-title":"Automatically proving plane geometry theorems stated by text and diagram","volume":"33","author":"Gan","year":"2019","journal-title":"Int. J. Pattern Recognit. Artif. Intell."},{"key":"ref_29","first-page":"83","article-title":"Automatic understanding and formalization of natural language geometry problems using syntax-semantics models","volume":"14","author":"Gan","year":"2018","journal-title":"Int. J. Innov. Comput. Inf. Control"},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"1940003","DOI":"10.1142\/S0218213019400037","article-title":"Automatic understanding and formalization of plane geometry proving problems in natural language: A supervised approach","volume":"28","author":"Gan","year":"2019","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"627","DOI":"10.1162\/coli_a_00360","article-title":"Discourse in multimedia: A case study in extracting geometry knowledge from textbooks","volume":"45","author":"Sachan","year":"2020","journal-title":"Comput. Linguist."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"He, Y., Zou, J., Zhang, X., Zhu, N., and Leng, T. (2024). Fgeo-tp: A language model-enhanced solver for euclidean geometry problems. Symmetry, 16.","DOI":"10.3390\/sym16040421"},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Tsai, S.h., Liang, C.C., Wang, H.M., and Su, K.Y. (2021). Sequence to general tree: Knowledge-guided geometry word problem solving. arXiv.","DOI":"10.18653\/v1\/2021.acl-short.121"},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Peng, S., Fu, D., Liang, Y., Gao, L., and Tang, Z. (2023, January 9\u201314). Geodrl: A self-learning framework for geometry problem solving using reinforcement learning in deductive reasoning. Proceedings of the Findings of the Association for Computational Linguistics: ACL 2023, Toronto, ON, Canada.","DOI":"10.18653\/v1\/2023.findings-acl.850"},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"Wu, W., Zhang, L., Liu, J., Tang, X., Wang, Y., Wang, S., and Wang, Q. (2024, January 18\u201322). E-gps: Explainable geometry problem solving via top-down solver and bottom-up generator. Proceedings of the IEEE\/CVF Conference on Computer Vision and Pattern Recognition, Vancouver, BC, Canada.","DOI":"10.1109\/CVPR52733.2024.01312"},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Zou, J., Zhang, X., He, Y., Zhu, N., and Leng, T. (2024). Fgeo-drl: Deductive reasoning for geometric problems through deep reinforcement learning. Symmetry, 16.","DOI":"10.3390\/sym16040437"},{"key":"ref_37","unstructured":"Zhang, C., Song, J., Li, S., Liang, Y., Ma, Y., Wang, W., Zhu, Y., and Zhu, S.C. (2024). Proposing and solving olympiad geometry with guided tree search. arXiv."},{"key":"ref_38","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_39","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, Busan, Republic of Korea."},{"key":"ref_40","unstructured":"Ning, M., Wang, Q.F., Huang, K., and Huang, X. (November, January 29). A symbolic characters aware model for solving geometry problems. Proceedings of the 31st ACM International Conference on Multimedia, Ottawa, ON, Canada."},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Liang, Z., Yang, T., Zhang, J., and Zhang, X. (2023, January 6\u201310). Unimath: A foundational and multimodal mathematical reasoner. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, Singapore.","DOI":"10.18653\/v1\/2023.emnlp-main.440"},{"key":"ref_42","doi-asserted-by":"crossref","unstructured":"Xiao, T., Liu, J., Huang, Z., Wu, J., Sha, J., Wang, S., and Chen, E. (2024). Learning to solve geometry problems via simulating human dual-reasoning process. arXiv.","DOI":"10.24963\/ijcai.2024\/725"},{"key":"ref_43","doi-asserted-by":"crossref","unstructured":"Zhang, J., and Moshfeghi, Y. (2024). GOLD: Geometry problem solver with natural language description. arXiv.","DOI":"10.2139\/ssrn.4875118"},{"key":"ref_44","doi-asserted-by":"crossref","unstructured":"Li, Z.Z., Zhang, M.L., Yin, F., and Liu, C.L. (2023). LANS: A layout-aware neural solver for plane geometry problem. arXiv.","DOI":"10.18653\/v1\/2024.findings-acl.153"},{"key":"ref_45","doi-asserted-by":"crossref","unstructured":"Zhang, M.L., Yin, F., Hao, Y.H., and Liu, C.L. (2022). Plane geometry diagram parsing. arXiv.","DOI":"10.24963\/ijcai.2022\/228"},{"key":"ref_46","doi-asserted-by":"crossref","unstructured":"Zhu, N., Zhang, X., Huang, Q., Zhu, F., Zeng, Z., and Leng, T. (2024). FGeo-Parser: Autoformalization and Solution of Plane Geometric Problems. Symmetry, 17.","DOI":"10.3390\/sym17010008"},{"key":"ref_47","unstructured":"Murphy, L., Yang, K., Sun, J., Li, Z., Anandkumar, A., and Si, X. (2024). Autoformalizing euclidean geometry. arXiv."},{"key":"ref_48","doi-asserted-by":"crossref","unstructured":"Zhang, X., Zhu, N., He, Y., Zou, J., Qin, C., Li, Y., and Leng, T. (2024). FGeo-SSS: A Search-Based Symbolic Solver for Human-like Automated Geometric Reasoning. Symmetry, 16.","DOI":"10.3390\/sym16040404"},{"key":"ref_49","unstructured":"Zhang, X., Zhu, N., Qin, C., Li, Y., Zeng, Z., and Leng, T. (2024). FGeo-HyperGNet: Geometric Problem Solving Integrating Formal Symbolic System and Hypergraph Neural Network. arXiv."},{"key":"ref_50","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), Montreal, QC, Canada.","DOI":"10.1109\/ICPR56361.2022.9956397"},{"key":"ref_51","doi-asserted-by":"crossref","unstructured":"Zhang, M.L., Yin, F., and Liu, C.L. (2023). A multi-modal neural geometric solver with textual clauses parsed from diagram. arXiv.","DOI":"10.24963\/ijcai.2023\/376"}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/17\/6\/902\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:48:12Z","timestamp":1760032092000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/17\/6\/902"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,7]]},"references-count":51,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2025,6]]}},"alternative-id":["sym17060902"],"URL":"https:\/\/doi.org\/10.3390\/sym17060902","relation":{},"ISSN":["2073-8994"],"issn-type":[{"type":"electronic","value":"2073-8994"}],"subject":[],"published":{"date-parts":[[2025,6,7]]}}}