{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T17:28:37Z","timestamp":1777656517776,"version":"3.51.4"},"reference-count":37,"publisher":"MDPI AG","issue":"4","license":[{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"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>Human-like automatic deductive reasoning has always been one of the most challenging open problems in the interdisciplinary field of mathematics and artificial intelligence. This paper is the third in a series of our works. We built a neural-symbolic system, named FGeo-DRL, to automatically perform human-like geometric deductive reasoning. The neural part is an AI agent based on deep reinforcement learning, capable of autonomously learning problem-solving methods from the feedback of a formalized environment, without the need for human supervision. It leverages a pre-trained natural language model to establish a policy network for theorem selection and employ Monte Carlo Tree Search for heuristic exploration. The symbolic part is a reinforcement learning environment based on geometry formalization theory and FormalGeo, which models geometric problem solving (GPS) as a Markov Decision Process (MDP). In the formal symbolic system, the symmetry of plane geometric transformations ensures the uniqueness of geometric problems when converted into states. Finally, the known conditions and objectives of the problem form the state space, while the set of theorems forms the action space. Leveraging FGeo-DRL, we have achieved readable and verifiable automated solutions to geometric problems. Experiments conducted on the formalgeo7k dataset have achieved a problem-solving success rate of 86.40%.<\/jats:p>","DOI":"10.3390\/sym16040437","type":"journal-article","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T08:27:52Z","timestamp":1712305672000},"page":"437","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["FGeo-DRL: Deductive Reasoning for Geometric Problems through Deep Reinforcement Learning"],"prefix":"10.3390","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-3657-4909","authenticated-orcid":false,"given":"Jia","family":"Zou","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\/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\/0000-0001-9958-5173","authenticated-orcid":false,"given":"Yiming","family":"He","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\/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,5]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"1199350","DOI":"10.3389\/frai.2023.1199350","article-title":"Human-like problem-solving abilities in large language models using ChatGPT","volume":"6","author":"Piarulli","year":"2023","journal-title":"Front. Artif. Intell."},{"key":"ref_2","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_3","unstructured":"Gao, J., Pi, R., Zhang, J., Ye, J., Zhong, W., Wang, Y., Hong, L., Han, J., Xu, H., and Li, Z. (2023). G-llava: Solving geometric problem with multi-modal large language model. arXiv."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"1526","DOI":"10.1038\/s41562-023-01659-w","article-title":"Emergent analogical reasoning in large language models","volume":"7","author":"Webb","year":"2023","journal-title":"Nat. Hum. Behav."},{"key":"ref_5","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_6","unstructured":"Nam, H., Kim, S., and Jung, K. (February, January 27). Number sequence prediction problems for evaluating computational powers of neural networks. Proceedings of the AAAI Conference on Artificial Intelligence, Honolulu, HI, USA."},{"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","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_9","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_10","unstructured":"Li, K., Gupta, A., Reddy, A., Pong, V.H., Zhou, A., Yu, J., and Levine, S. (2021, January 18\u201324). Mural: Meta-learning uncertainty-aware rewards for outcome-driven reinforcement learning. Proceedings of the International Conference on Machine Learning (PMLR), Virtual."},{"key":"ref_11","first-page":"13566","article-title":"Rudder: Return decomposition for delayed rewards","volume":"32","author":"Gillhofer","year":"2019","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1038\/nature16961","article-title":"Mastering the game of Go with deep neural networks and tree search","volume":"529","author":"Silver","year":"2016","journal-title":"Nature"},{"key":"ref_13","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. arXiv.","DOI":"10.3390\/sym16040437"},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Gelernter, H., Hansen, J.R., and Loveland, D.W. (1960, January 3\u20135). Empirical explorations of the geometry theorem machine. Proceedings of the Western Joint IRE-AIEE-ACM Computer Conference, San Francisco, CA, USA.","DOI":"10.1145\/1460361.1460381"},{"key":"ref_15","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_16","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00283133","article-title":"Automated generation of readable proofs with geometric invariants: I. Multiple and shortest proof generation","volume":"17","author":"Chou","year":"1996","journal-title":"J. Autom. Reason."},{"key":"ref_17","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_18","first-page":"8822","article-title":"Reinforcement learning of theorem proving","volume":"31","author":"Kaliszyk","year":"2018","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"ref_19","first-page":"9330","article-title":"Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning","volume":"34","author":"Wu","year":"2021","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"1061","DOI":"10.1109\/TASLP.2022.3155284","article-title":"Automatic math word problem generation with topic-expression co-attention mechanism and reinforcement learning","volume":"30","author":"Wu","year":"2022","journal-title":"IEEE\/ACM Trans. Audio Speech Lang. Process."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Wang, L., Zhang, D., Gao, L., Song, J., Guo, L., and Shen, H.T. (2018, January 2\u20137). Mathdqn: Solving arithmetic word problems via deep reinforcement learning. Proceedings of the AAAI Conference on Artificial Intelligence, New Orleans, LA, USA.","DOI":"10.1609\/aaai.v32i1.11981"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Peng, S., Fu, D., Liang, Y., Gao, L., and Tang, Z. (2023, January 30). 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_23","doi-asserted-by":"crossref","unstructured":"Kocsis, L., and Szepesv\u00e1ri, C. (2006, January 18\u201322). Bandit based Monte-Carlo planning. Proceedings of the European Conference on Machine Learning, Berlin, Germany.","DOI":"10.1007\/11871842_29"},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Puterman, M.L. (1994). Markov Decision Processes: Discrete Stochastic Dynamic Programming, John Wiley & Sons.","DOI":"10.1002\/9780470316887"},{"key":"ref_25","unstructured":"Sanh, V., Debut, L., Chaumond, J., and Wolf, T. (2019). DistilBERT, a distilled version of BERT: Smaller, faster, cheaper and lighter. arXiv."},{"key":"ref_26","unstructured":"Devlin, J., Chang, M.W., Lee, K., and Toutanova, K. (2018). Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv."},{"key":"ref_27","first-page":"1057","article-title":"Policy gradient methods for reinforcement learning with function approximation","volume":"12","author":"Sutton","year":"1999","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Van Hasselt, H., Guez, A., and Silver, D. (2016, January 12\u201317). Deep reinforcement learning with double q-learning. Proceedings of the AAAI Conference on Artificial Intelligence, Phoenix, AR, USA.","DOI":"10.1609\/aaai.v30i1.10295"},{"key":"ref_29","unstructured":"Schulman, J., Moritz, P., Levine, S., Jordan, M., and Abbeel, P. (2015). High-dimensional continuous control using generalized advantage estimation. arXiv."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1023\/A:1013689704352","article-title":"Finite-time analysis of the multiarmed bandit problem","volume":"47","author":"Auer","year":"2002","journal-title":"Mach. Learn."},{"key":"ref_31","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_32","unstructured":"Gelernter, H. (1995). Computers & Thought, MIT Press."},{"key":"ref_33","unstructured":"Russell, S.J., and Norvig, P. (2016). Artificial Intelligence: A Modern Approach, Pearson."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"J\u00e4ntschi, L. (2020). Detecting extreme values with order statistics in samples from continuous distributions. Mathematics, 8.","DOI":"10.3390\/math8020216"},{"key":"ref_35","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_36","doi-asserted-by":"crossref","unstructured":"Sachan, M., Dubey, K., and Xing, E. (2017, January 7\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_37","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, Canada.","DOI":"10.18653\/v1\/S17-1029"}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/16\/4\/437\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T14:23:46Z","timestamp":1760106226000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/16\/4\/437"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,5]]},"references-count":37,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2024,4]]}},"alternative-id":["sym16040437"],"URL":"https:\/\/doi.org\/10.3390\/sym16040437","relation":{},"ISSN":["2073-8994"],"issn-type":[{"value":"2073-8994","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,5]]}}}