Cold Expansion Team Unveils New FormalGeo Geometry Automatic Solver at IJCAI 2025

Recently, the International Joint Conference on Artificial Intelligence (IJCAI 2025), one of the most influential and authoritative conferences in the field of artificial intelligence, announced its peer review results. A research team led by Associate Professor Leng Tuo from the School of Computer Engineering and Science at Shanghai University successfully had their paper titled "FGeo-HyperGNet: Geometric Problem Solving Integrating FormalGeo Symbolic System and Hypergraph Neural Network" accepted for presentation. The first author is Zhang Xiaokai, a doctoral student at Shanghai University’s computer engineering program starting in 2024, while Associate Professor Leng Tuo is the sole corresponding author. With an acceptance rate of approximately 19%, IJCAI is a highly competitive conference held annually worldwide. Geometry, a time-honored and continuously evolving discipline, has seen significant advancements since Euclid's Elements introduced its foundational principles. Over the years, the exploration of automatic geometric problem-solving methods has paralleled the development of geometric theories. The advent of computers brought new possibilities, leveraging their powerful computational and reasoning capabilities to design algorithms for automatic problem-solving. This led to the birth of mathematical mechanization, a branch that focuses on converting mathematical knowledge into a form comprehensible by computers—a crucial step in the integration of mathematics and computer science. Associate Professor Leng Tuo's team has systematically researched the formal representation and automatic solving of geometric problems. They have integrated mathematical mechanization techniques with deep learning to create an innovative framework called FormalGeo. This framework is divided into four primary components: geometric formalization theory (represented in red), the geometric symbolic system (in yellow), the geometric problem solver (in blue), and the automated formalization and de-formalization of geometric problems (in green). The latest work accepted by IJCAI 2025, "FGeo-HyperGNet," marks the seventh paper in their series on geometric problem-solving. This system combines a neural network and symbolic reasoning to achieve human-like automated geometric solutions. The symbolic component, built on FormalGeo, automates geometric relationship inference and algebraic operations, organizing the solution process into a hypergraph structure where known conditions are hypernodes and geometric theorems are hyperedges. The neural component, HyperGNet, is an attention-based hypergraph neural network that consists of an encoder for effectively representing hypergraph structure and semantic information, and a theorem predictor that guides the solution process. By predicting the required theorems and applying them iteratively, FGeo-HyperGNet can solve geometric problems with a clear, traceable, and explainable process. The team tested FGeo-HyperGNet on three geometric problem datasets: FormalGeo7K, Geometry3K, and GeoQA. Their method achieved state-of-the-art success rates of 88.36%, 85.64%, and 91.99% respectively, outperforming existing top methods by 5.98%, 20.44%, and 1.59%. Notably, in solving high-difficulty geometric problems, FGeo-HyperGNet demonstrated a significant advantage over current leading methods. Over nearly five years, Leng Tuo's research group has gained substantial recognition in the field of geometric automated reasoning. Their foundational work, including the FormalGeo formalization system, has supported numerous derivative studies. For instance, a team from Peking University developed a new framework called DFE-GPS based on FormalGeo, enhancing multi-modal large language models' ability to understand and reason about geometric figures through a three-stage training process. Another team from the University of Science and Technology of China proposed the GeoGen method, which generates multi-step reasoning paths for geometric problems using FormalGeo, ensuring logical correctness. This method trains specialized large language models to convert natural language reasoning steps into formal representations, making them easier to verify symbolically. These achievements underscore the growing impact and depth of graduate education at Shanghai University's School of Computer Engineering and Science, where students are increasingly contributing to cutting-edge research. This work not only highlights the potential of combining symbolic and neural approaches but also underscores the importance of interdisciplinary collaboration in advancing the field of artificial intelligence. The FormalGeo framework serves as a robust foundation, supporting various applications and driving innovation in geometric problem-solving. For more information on the FormalGeo project, visit the official website at FormalGeo.