FGeo-HyperGNet: Geometric Problem Solving Integrating FormalGeo Symbolic System and Hypergraph Neural Network

1 Introduction

Geometry problem solving (GPS) has always been a longstanding challenge [Littman et al., 2022; Gowers et al., 2023] in the fields of mathematical reasoning and artificial intelligence, due to the cross-modal forms of knowledge and the symbolic-numerical hybrid reasoning process. GPS can be described as: Given a geometric problem description (original images and texts or formalized), the solver needs to implement stepwise reasoning leading to the final answer.

Traditional GPS methods can generally be divided into three categories. The first category is the synthesis methods, such as backward search method [Gelernter, 1959], forward chaining method [Nevins, 1975] and deductive database method [Chou et al., 2000]; the second category is the algebraic methods, such as Wu's method [Wu, 1978] and Gr¨obner bases method [Buchberger, 1988]; the third category is the point elimination methods based on geometric invariants [Zhang et al., 1995; Chou et al., 1995].

∗Corresponding author.

Artificial intelligence technology has provided new perspectives for GPS [Seo et al., 2015; Sachan and Xing, 2017; Gan et al., 2019]. In particular, with the rapid development of deep learning and the application of large language models, a series of neural-symbolic methods have been proposed. These methods can generally be divided into two categories: Deductive Database methods (DD methods) [Lu et al., 2021; Peng et al., 2023; Trinh et al., 2024; Wu et al., 2024] and Program Sequence Generation methods (PSG methods) [Chen et al., 2021; Zhang et al., 2023b; Xiao et al., 2024]. DD methods parse the problem images and texts into a unified formal language description, and then apply a predefined set of theorems to solve the problems. These approaches require the establishment of a formal system and the problem-solving process has mathematical rigor and good readability. PSG methods view GPS as a sequence generation task with multimodal input. These methods learn from annotated examples to map geometric problem descriptions into executable programs. After program sequences are generated, the executor computes them step by step and obtain the problem answer.

However, existing research has notable limitations. Most recent advances in GPS focus on exploring new methods and models [Xiao and Zhang, 2023], yet they overlook the investigation of geometric formal systems. The theorems and predicates of these formal systems are implemented using programming languages, and the definition of new predicates and theorems necessitates modifications to the solver's code. This characteristic significantly hampers the scalability of formal systems. Most Existing DD methods are non-traceable, and the redundant theorems applied during heuristic searches cannot be eliminated. Most Existing PSG methods, on the other hand, fail to yield a human-like problem-solving process, suffer from low readability, and cannot guarantee the correctness of results. The process of solving geometric problems encompasses both numerical computation and relational reasoning, with existing research predominantly focused on numerical problem-solving objectives, struggling to integrate computation and reasoning within a unified framework [Chen et al., 2022]. This imperfection in the existing formal systems severely restricts the types and complexity of GPS.

In addition, existing work predominantly focuses on the unified cross-modal integration of geometric text and image [Zhang et al., 2023b; Zhang et al., 2023a] with limited attention to the embedding of geometric formal languages. AlphaGeometry [Trinh et al., 2024] can solve IMO-level geometry problems, but it treats the solving process as a text sequence and models GPS as a text generation task, ignoring structural relationships between conditions. Neglecting of graph structure information in formal language results in poor theorem prediction [Guo and Jian, 2022]. S2G [Tsai et al., 2021] maps the problem-solving process onto an expression tree, implicitly incorporating process information, yet it does not reflect a human-like problem-solving approach. GeoDRL [Peng et al., 2023] organizes geometric conditions into a Geometric Logic Graph (GLG), but the GLG lacks information about the problem-solving process thus fails to model the interrelations among theorems. Formal language, distinct from natural language, adheres to stringent syntactic forms. Its symbols bear specific meanings and inappropriate tokenization can obliterate the inherent meaning of statements [Ning et al., 2023]. Moreover, due to the unique structure of formal languages, they are represented as three-dimensional real number matrices, which cannot be processed using common network architectures. There is an urgent need for research into the embedding and encoding of formal languages.

We propose a neural-symbolic architecture, named FGeoHyperGNet, to address these issues, as illustrated in Figure 1. The neural component is a hypergraph neural network based on the attention mechanism, consisting of a hypernode encoder and a theorem predictor. The hypernode encoder embeds the semantic information of hypernodes and the neighboring edge information into fixed-length real-number vectors, serving as the feature representations of the nodes. The theorem predictor adopts an encoder-decoder architecture. It first extracts and fuses the node features obtained by the hypernode encoder to generate a hypergraph encoding. Subsequently, it uses a task-specific decoder that receives the hypergraph encoding and the goal encoding to predict the theorems required for solving geometric problems. We first use a self-supervised method to pretrain the hypernode encoder, making it to retain as much semantic information of formalized statements as possible during the encoding stage. Then the encoder is build as part of the theorem predictor for endto-end training. The symbolic component is a symbolic formal system built on FormalGeo [Zhang et al., 2024c], which can construct the process of GPS as a directed hypergraph with conditions as hypernodes and theorems as hyperedges. This symbolic system can validate and apply the theorems predicted by the neural component, perform geometric relational reasoning and algebraic equation solving, and update the state of the hypergraph.

The neural component predicts theorems according to the hypergraph, and the symbolic component applies theorems and updates the hypergraph, thus forming a predict-apply cycle (PAC) to ultimately achieve readable, traceable and verifiable automatic solving of geometric problems. Additionally, we utilize FGeo-Parser [Zhu et al., 2025] to convert geometric problem images and text into formalized language. Benefiting from the structured representation of the problemsolving process, we define a rule-based Solution Generator to derive a human-like solution. To the best of our knowledge, we are the first to construct a geometric problem-solving system that takes raw geometric problem images and text as input, produces a human-like solution as output, and ensures the complete correctness of the solution. Our work presents a neuro-symbolic framework for GPS, while demonstrating that hypergraph-structured data can enhance the capabilities of such methods.

Our contributions are summarized as follows:

1. We introduce HyperGNet, an attention-based hypergraph feature embedding and extraction network. Unlike message-passing models, HyperGNet prioritizes the global relationships and representations of hypernodes, which are crucial for addressing the GPS task.
2. We present FGeo-HyperGNet, a neural-symbolic architecture designed for GPS. The neural component predicts theorems required to solve geometric problems based on the hypergraph, while the symbolic component conducts rigorous geometric relational reasoning and algebraic equation solving to ensure the correctness of the solution process and update the hypergraph. Additionally, we propose PAC to clarify the interaction between the neural and symbolic components.
3. By combining FGeo-Parser, the rule-based solution generator, and FGeo-HyperGNet, we develop a geometric problem solving system that takes raw geometric problem images and text as input, generates a human-like solution as output, and ensures the complete correctness of the solution.
4. We conducted extensive experiments on the FormalGeo7K [Zhang et al., 2024c] dataset, achieving a theorem prediction accuracy (TPA) of 93.50% and a problem-solving success rate (PSSR) of 88.36%. Furthermore, we performed ablation studies on the training methods and model architecture of HyperGNet.

2 Preliminaries

This section outlines the definition of the problem and models the problem-solving process.

2.1 ProblemDefinition andModeling

We formulate geometric problems as a collection of conditions and a problem goal and formulate the problem solving process as the sequential application of theorems. Consequently, the process of solving geometric problems can be represented as a hypergraph, where conditions are modeled as hypernodes and theorems as hyperedges. The fundamental terms and examples are defined below.

Definition 1 Condition (C): Conditions represent a set of geometric entities, attributes, and relationships. These conditions encompass geometric and quantitative relationships, such as "RightTriangle(ABC)" and "Equal(LengthOfLine(AB),10)".

Definition 2 Theorem (T ): Theorems constitute pre-defined prior knowledge. A theorem comprises a set of premise conditions and a set of conclusion conditions, both of which are collections of conditions. For instance, the parallel's transitivity can be expressed as "Parallel(AB,CD) & Parallel(CD,EF) → Parallel(AB,EF)". The collection of all such theorem definitions forms the Prior Knowledge Base TKB. Definition 3 Goal (G): Goal represents the objective of geometric problem solving, which can be considered a special form of condition, such as "Value(MeasureOfAngle(ABC))" or "Relation(Parallel(AB,CD))".

Definition 4 Hypergraph (H): The solution hypergraph, defined as H = (C, T,G), is a directed hypergraph with known conditions as hypernodes and applied theorems as hyperedges. It describes the structured process of geometric problem solving. A successful application of a theorem can add several new hypernodes to the hypergraph and construct a new hyperedge from a set of premise to a set of new conclusion.

The key for GPS lies in the system's ability to accurately predict the theorem to be applied in the current problem state. Most existing methods [Lu et al., 2021; Chen et al., 2021] formulate the theorem prediction task as a generative task, where the parameter optimization objective is to maximize the conditional probability of the next theorem ti given the previously used theorems {t1, t2, . . . , ti-1} and the initial hypergraph h0, as shown in Formula 1. These methods fail to capture the intermediate states hi of the problem, thus cannot fully utilize the intermediate results.

Benefiting from the FormalGeo formal system, we can obtain and update the problem state in real time. We formulate the theorem prediction task as a multi-class classification task, where the parameter optimization objective is to maximize the conditional probability of the next theorem ti given the current problem state hi-1, as shown in Formula 2.

The geometric problem-solving process can be modeled as a Markov Decision Process [Peng et al., 2023], where the problem solution hypergraph constitutes the state space H = {hi|i = 0, 1, 2, . . . }, and the geometry theorem set constitutes the action space T = {ti|i = 1, 2, . . . }. Given a formal representation of a geometric problem, FormalGeo constructs it into a hypergraph h. The hypergraph h0 contains only several unconnected initial condition nodes. Our task is to provide a sequence of theorem t, where each application of ti adds new hyperedges and hypernodes to hi-1, thus extends hi-1 to hi, ultimately constructing a reachable path from the initial conditions to the problem-solving goal.

2.2 Predict-Apply Cycle

We have constructed a system comprising a formal environment and a neural agent to accomplish the aforementioned task. This system involves an interaction of two parts, which we refer to as the Predict-Apply Cycle (PAC), as illustrated in Figure 1. The algorithm is described in Algorithm 1. The AI agent acquires the current solution hypergraph hi-1 of the geometric problem and predicts the theorem ti required for solving the problem. The formalized environment then applies the theorem ti, adds new hyperedges and hypernodes, and updates hi-1 to hi. This interactive process is repeated continuously until the problem is solved or the hypergraph ceases to update.

3 Neural-Symbolic Solver

This section introduces our proposed neural-symbolic architecture, which includes a symbolic formal system built on

Algorithm 1 Predict-Apply cycle

Input: probem: geometric problems described using formalized language.

Output: theorem seqs: theorem sequence for problem solving.

• 1: Initialize env and agent.
• 2: Initialize theorem seqs as None.
• 3: Initialize applied as True.
• 4: env.init hypergraph(problem)
• 5: while applied do
• 6: hypergraph ← env.get hypergraph()
• 7: theorem ← agent.predict(hypergraph)
• 8: applied ← env.apply(theorem)
• 9: if env.solved is True then
• 10: theorem seqs ← env.get theorem seqs()
• 11: break
• 12: end if
• 13: end while

FormalGeo and a hypergraph neural network based on attention mechanisms.

3.1 Symbolic System

Most Existing work has failed to establish a consistent, traceable, and extensible formal system. We have developed a geometric symbolic formal system based on FormalGeo [Zhang et al., 2024c]. FormalGeo employs Geometry Definition Language to define the formal system and uses Condition Declaration Language to declare the topological structure of geometric problems, conditions, and problem-solving goals. It first transforms the problem-solving process into the application of geometric theorems, and subsequently further transforms the application process of these theorems into the execution of Geometric Predicate Logic, thereby enabling traceable relational reasoning and algebraic equation solving.

The conditions of geometric problems are stored as quintuples comprising condition ID, condition type, condition body, premises, and theorem. Based on the premises and theorems, we group and structure these conditions, organizing them into a hypergraph with the condition body as hypernodes and the theorem as hyperedges. A set of premise hypernodes and a set of conclusion hypernodes are connected by a theorem hyperedge, thus forming a hypergraph.

This formal system bridges the gap between humans and computers, ensuring that GPS is both human-readable and mathematically rigorous. A more detail discussion of FormalGeo can be found in [Zhang et al., 2024a].

3.2 Hypernode Encoding

Our task is to create a neural solver that can predict the theorems needed for GPS based on the hypergraph hi given by the current formal environment. This requires encoding the hypernode and its neighboring hyperedge into a real-valued vector that can be processed by neural networks, which can be viewed as a sentence embedding problem [Li et al., 2020]. The Transformer [Vaswani et al., 2017] and its derivative network structures are considered powerful architectures for modeling sequential data but are not capable of directly processing graph-structured data. Inspired by Graphormer [Ying et al., 2021], We first decompose the semantic and structural information in graph-structured data into a serialized form, and then input and embed it at the appropriate positions in the network.

For a directed hypergraph h containing n hypernodes, we can uniquely represent the hypergraph using the hypernode vector c = (c1, c2, . . . , cn) and the hyperedge theorem adjacency matrix Tn×n. ci represents a condition declaration sentence, composed of a predicate and some individual words, such as "RightTriangle(ABC)". Formal languages and mathematical symbols have domain-specific meanings [Ning et al., 2023] and cannot be simply tokenized using natural language tokenization methods. We have designed the FormalGeo tokenizer for neural networks, where ci is ultimately represented as a token list, such as [RightTriangle, A, B, C]. The adjacency matrix Tn×n is an extremely sparse matrix, where the element tij indicates whether there is a hyperedge connecting hypernode ci and cj. When embedding the row vectors ti of the adjacency matrix T, due to its extremely sparse nature, traditional methods would result in the idleness and waste of a large number of neurons. Inspired by the segment encoding of BERT [Devlin et al., 2019], we remove the empty nodes in ti and use position encoding and structure encoding to preserve its structural information. For example, a hyperedge ti = [a, 0, 0, 0, b, 0, 0, 0, c, 0, 0] is transformed into ti = [a, b, c], pei = [1, 2, 3], and sei = [1, 5, 9].

For a hypernode ci and its incident hyperedge ti, we input them into the hypernode encoder, which transforms them into an m-dimensional vector Hi, as shown in Formula 3, where HE represents the hypernode encoder and ⊕ represents vector concatenation. We construct the hypernode encoder based on the Transformer architecture, as illustrated in Figure 2. The hypernode encoder adopts an encoder-decoder architecture and uses a self-supervised approach to reconstruct the input at decoder, thereby forcing the model to learn how to embed semantic and structural information into a fixedlength vector. At the output stage of the encoder, the average of the word sequence embeddings is taken to represent the overall sentence encoding [Yan et al., 2021]. After passing through the hypernode encoder, the solution hypergraph h is ultimately encoded into the hypergraph matrix Hn×m and the goal g ∈ Rm.

3.3 HyperGNet Architecture

As shown in Figure 3, HyperGNet adopts an encoder-decoder architecture. We use the transformer encoder modules to construct the HyperGNet encoder, and task-specific attention to construct HyperGNet decoder. The solving process of problems can be described with a hypergraph H = (C, T,G), where C and T are processed through hypernode encoder and HyperGNet encoder to obtain the hypergraph encoding H(N) n×m. The goal G can be considered as a special hypernode and embedded into an m-dimensional vector g.

A task-specific attention layer is used to extract key information relevant to solving current problem, as shown in Formula 4, where Q = gW (Q) , K = H(N) n×mW (K) and V = H(N) n×mW (V ) . The other modules of HyperGNet decoder align with Transformer [Vaswani et al., 2017]. In summary, hypergraph H is encoded by the hypernode encoder into hypernode embedding Hn×m and goal embedding g, which are fed into HyperGNet to predict the theorem probability ˆ ⃗y.

For the solution hypergraph H, the application process of theorems can be represented as a directed acyclic graph. Multiple alternative theorems may exist at intermediate stages of GPS. We formulate theorem prediction as multi-class classification, decomposing it into binary classification tasks with cross-entropy loss. The loss function is shown in Formula 5, where ˆ y is the predicted theorem selection probability, y is the ground truth, σ is the sigmoid activation function, and M is the number of defined theorems in TKB.

4 Experiments

This section presents the performance of our neural-symbolic architecture on FormalGeo7K [Zhang et al., 2024c], Geometry3K [Lu et al., 2021] and GeoQA [Chen et al., 2021]. We compare and analyze the differences in PSSR and TPA between existing methods and the approach proposed in this paper. Additionally, we conduct ablation experiments on the training method and model architecture of HyperGNet.

4.1 Dataset

We conducted experiments on FormalGeo7K [Zhang et al., 2024c], Geometry3K [Lu et al., 2021] and GeoQA [Chen et al., 2021], partitioning it into a training set, validation set, and test set at a ratio of 3:1:1. We removed the hypernodes from the solution hypergraph, leaving only the hyperedges, which form a directed acyclic graph (DAG) of theorems. Any theorem sequence t obtained by topological sorting of the theorem DAG can solve the problem. We randomly topological sort the theorem DAG and obtained each step's problem state hi-1 and the set of applicable theorems ti, yielding data pairs (hypergraph, applicable theorems). This process ultimately generated 20,571 training data pairs (from 4,079 problems), 7,072 validation data pairs (from 1,370 problems), and 7,046 test data pairs (from 1,372 problems).

4.2 EvaluationMetrics

We use Theorem Prediction Accuracy (TPA) and ProblemSolving Success Rate (PSSR) as the evaluation metrics to assess different methods. Their definitions are as follows:

TPA: Given the current problem state hi-1, the model is tasked with predicting the theorem ti required for solving the problem. This metric captures the theorem prediction accuracy of the model at each step of the problem-solving process. PSSR: PSSR is the proportion of successfully solved problems to the total number of problems. Solving a geometric problem requires several theorems, which the model must predict correctly and in the correct order. The predictions are then verified by the formalized system to determine whether the problem is successfully solved. This metric evaluates the model's overall problem-solving capability.

4.3 BenchmarkMethods

We evaluated a variety of methods on the FormalGeo7K dataset, which include: 1. traditional pure symbolic methods, such as Forward Search and Backward Search; 2. neuralsymbolic methods (neural language models integrated with the FormalGeo symbolic system), such as T5-small with FGeo and BART-base with FGeo; 3. pure-neural methods (large language models), including DeepSeek-v3; 4. neural-symbolic systems specifically designed for GPS, such as Inter-GPS, NGS, DualGeoSolver, FGeo-TP, and FGeoDRL; and 5. our proposed neural-symbolic system, FGeoHyperGNet.

We also compare the performance of 2 state-of-the-art problem-solving methods on the Geometry3K dataset, GeoDRL [Peng et al., 2023] and E-GPS [Wu et al., 2024]; 2 stateof-the-art methods on the GeoQA dataset, SCA-GPS [Ning et al., 2023] and DualGeoSolver [Xiao et al., 2024]; 2 state-ofthe-art methods on the FormalGeo7K dataset, FGeo-TP [He et al., 2024] and DFE-GPS [Zhang et al., 2024d]; as well as the performance of FGeo-HyperGNet on the three aforementioned datasets.

The other methods in the comparison use their original parameter settings. For HyperGNet, we first employ a selfsupervised approach to pre-train the hypernode encoder. This encoder is then integrated into HyperGNet, allowing for endto-end training. We set the hidden dimension dmodel of HyperGNet to 256, the number of layers N to 4, and the number of attention heads h to 4. Under this configuration, HyperGNet has 20.38 million parameters, significantly fewer than the other methods. During training, we optimize the model parameters using the Adam optimizer, with a learning rate of 10-5 , a batch size of 16, and training for 20 epochs. A single training epoch on a GeForce RTX 4090 takes approximately 30 minutes.

4.4 Experimental Results

According to the length of the annotated theorem l, we roughly categorize the difficulty of the problems into 6 levels, denoted as L1(l ≤ 2), L2(3 ≤ l ≤ 4), L3(5 ≤ l ≤ 6), L4(7 ≤ l ≤ 8), L5(9 ≤ l ≤ 10), L6(l ≥ 11). In Table 1, we compare various methods across multiple levels of difficulty on the FormalGeo7K dataset.

Among all evaluated methods, FGeo-HyperGNet achieves the highest overall PSSR of 88.36% and consistently excels across all difficulty levels. While most methods experience a significant drop in performance as the problem difficulty increases (particularly for L5 and L6), FGeo-HyperGNet maintains robust results, achieving 56.67% on L6, compared to 36.59% by second-best NGS. This highlights its ability to handle challenging geometric problems more effectively than existing approaches.

Traditional search methods achieve limited performance. (Large) Language models perform better but their inability to model geometric structures and relationships limits their ability. FGeo-HyperGNet's key advantage lies in its integration of neural and symbolic components. AI-driven heuristic search ensures efficient theorem selection, significantly contributing to the method's superior performance, especially on challenging problems. This design enables it to model long-range dependencies between geometric conditions and theorems effectively. Compared to other neural-symbolic systems, FGeo-HyperGNet significantly outperforming the second-best method, FGeo-TP, by 7.5%.

We also evaluate the performance of FGeo-HyperGNet against several existing state-of-the-art methods on three datasets: Geometry3K, GeoQA, and FormalGeo7K, as shown in Table 2. FGeo-HyperGNet consistently outperforms all competing methods, achieving the highest PSSR across all three datasets. Notably, FGeo-HyperGNet achieves a PSSR of 85.64%, significantly outperforming the current state-ofthe-art (DualGeoSolver with 65.20%) by 20.44%, which largely benefits from our proposed formalization approach and neural-symbolic system. FGeo-HyperGNet captures the intermediate states of problems, thereby more accurately modeling the mapping from problems to theorems.

4.5 Ablation study

We conduct ablation experiments on the training method and model architecture of HyperGNet, as shown in Table 3. The term -w/o Pretrain indicates the removal of the pretraining step, directly proceeding to end-to-end training. -w/o SE denotes the exclusion of the structural encoding in Formula 3. - w/o Hypergraph refers to the removal of the hypergraph structural information, where the node sequence is used to represent the problem state. This is implemented by, without altering the network architecture, omitting the hyperedge information and inputting only the node data as sequential information into the network.

We observe that as the beam size increases, both TPA and PSSR improve. To assess the effectiveness of pretraining, we removed the pretraining stage and found that TPA and PSSR decreased across all beam size settings. This demonstrates that pretraining is crucial for enabling the hypernode encoder to retain the semantic information of geometric conditions. To evaluate the importance of graph-structured data in the context of GPS, we removed the graph structure information and conducted experiments. As shown in Table 3, we found that both TPA and PSSR decreased, regardless of whether the graph structure was removed alone or if both the graph structure and semantic information were entirely removed (i.e., treating the data as sequential). This indicates that graphstructured data is important for the current task. The information of theorem applications and the relationships between conditions contribute to the improvement of TPA and PSSR.

4.6 Case Analysis

We select some representative cases in Figure 4 for further analysis. Taking Case 1 as an example, FGeo-HyperGNet not only provides the solution to the problem but also generates a detailed solution hypergraph. Notably, FGeo-HyperGNet produces a more concise solution process than the human annotations. However, there are some limitations. We found that during the geometric problem-solving process, the time required for solving systems of equations is much longer than that for relational reasoning. The majority of problemsolving failures are due to equation-solving timeouts, especially for theorems involving trigonometric functions, as illustrated in Case 2. Other failures occur because these types of problems are too rare, and the model is unable to adequately learn the solution methods for the minority class from the training data, as shown in Case 3.

5 Conclusions

This paper proposes a neural-symbolic architecture for solving formalized plane geometry problems. We are the first to construct a GPS system that takes problem images and text as input, produces a human-like solution, and ensures the complete correctness of the solution. We also achieve state-of-the-art results with a TPA of 93.50% and a PSSR of 88.36% on the FormalGeo7K dataset. In the future, we plan to integrate reinforcement learning into the neural component and auxiliary construction into the symbolic component to achieve an automatic IMO-level GPS without human supervision.

Acknowledgments

This research was supported by National Natural Science Foundation of China (NSFC) grant 12071282.