Source-linked AI summary
UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression
Jiaqi Chen, Tong Li, Jinghui Qin, Pan Lu, Liang Lin, Chongyu Chen, Xiaodan Liang
TL;DR
Geometry calculation and proving are commonly treated as separate tasks despite shared representations and mathematical knowledge. The paper unifies them through the UniGeo benchmark, sequence-based proof reformulation, Geoformer, and Mathematical Expression Pretraining. Geoformer achieves state-of-the-art performance, with reported accuracy improvements of 5.6% on calculation and 3.2% on proving over task-specific NGS models.
Problem
Calculation and proving are usually treated as separate geometry tasks despite overlapping representations and mathematical knowledge, limiting unified evaluation of neural reasoning.
Method
The paper constructs UniGeo with compatible calculation and proving sequences, then trains Geoformer jointly after Mathematical Expression Pretraining on solution expressions.
Results
5.6% and 3.2% accuracy improvements over task-specific NGS models are reported for calculation and proving problems, respectively.
Takeaways & Limitations
Unified formulation improves geometry reasoning performance on both calculation and proving tasks in the UniGeo benchmark.
Takeaways & Limitations
Answer accuracy remains far from real-world application, while manual data construction limits the type and difficulty of geometry problems.
Abstract
from arXiv · showhide
Geometry problem solving is a well-recognized testbed for evaluating the high-level multi-modal reasoning capability of deep models. In most existing works, two main geometry problems: calculation and proving, are usually treated as two specific tasks, hindering a deep model to unify its reasoning capability on multiple math tasks. However, in essence, these two tasks have similar problem representations and overlapped math knowledge which can improve the understanding and reasoning ability of a deep model on both two tasks. Therefore, we construct a large-scale Unified Geometry problem benchmark, UniGeo, which contains 4,998 calculation problems and 9,543 proving problems. Each proving problem is annotated with a multi-step proof with reasons and mathematical expressions. The proof can be easily reformulated as a proving sequence that shares the same formats with the annotated program sequence for calculation problems. Naturally, we also present a unified multi-task Geometric Transformer framework, Geoformer, to tackle calculation and proving problems simultaneously in the form of sequence generation, which finally shows the reasoning ability can be improved on both two tasks by unifying formulation. Furthermore, we propose a Mathematical Expression Pretraining (MEP) method that aims to predict the mathematical expressions in the problem solution, thus improving the Geoformer model. Experiments on the UniGeo demonstrate that our proposed Geoformer obtains state-of-the-art performance by outperforming task-specific model NGS with over 5.6% and 3.2% accuracies on calculation and proving problems, respectively.
1 Introduction
The paper argues that geometry calculation and proving should be unified because they share reasoning skills and can use compatible sequence representations. It introduces UniGeo, Geoformer, and Mathematical Expression Pretraining to support this unified setting.
- Motivation: Unified geometry reasoning is motivated by shared skills and knowledge across calculation and proving tasks.A unified model can avoid auxiliary task identification and model selection, which may introduce cumulative errors.
- Problem: Existing proving data is small-scale and uses an incompatible format, motivating a unified benchmark and representation.The proposed reformulation turns proof steps into causal proving sequences compatible with calculation program sequences.
- UniGeo: UniGeo contains 4,998 calculation problems and 9,543 proving problems.The benchmark is designed to evaluate high-level geometry logical reasoning in neural models.
- Geoformer: Geoformer handles geometry calculation and proof reasoning simultaneously through a unified geometric transformer framework.It is fine-tuned to predict program and proving sequences for both problem types.
- Pretraining: Mathematical Expression Pretraining predicts mathematical expressions extracted from problem solutions before unified task training.The expressions are treated as solution-sequence targets containing implicit mathematical knowledge.
2 Related Work
Prior geometry datasets and theorem-proving systems leave gaps in scale, task coverage, and neural-based geometry proving. UniGeo addresses these gaps by combining calculation and proving in a unified benchmark and model.
- Geometry Problem Solving: Earlier geometry datasets were often unavailable or small, limiting development of geometry problem-solving research.Later datasets focused mainly on arithmetic calculation rather than comprehensive geometry reasoning.
- Geometry Theorem Proving: Existing geometry theorem-proving work largely relies on designed rules, deductive databases, or forward-chaining systems.These approaches differ from neural-based generation of proofs from diagrams and statements.
- Geometry Theorem Proving: Automatic neural-based proving in the geometry domain remains less studied.The paper proposes Geoformer to generate proofs from geometry diagrams and statements from scratch.
3 Unifying Geometry Reasoning
UniGeo unifies geometry calculation and proving by collecting a large proving benchmark and reformulating proofs into target sequences compatible with calculation programs. This representation supports a shared multimodal reasoning task across both problem types.
- UniGeo combines 4,998 calculation problems with 9,543 proving problems in one benchmark.
- Each proving example includes a diagram, description, and proof with reasons and mathematical expressions.The proving data contains 37 reason categories, with each expression representing a proof step using operators and geometry elements.
- Proofs are converted into proving sequences containing reason, operator, and geometry-element tokens.Reasons precede proof expressions, while geometry elements are converted to tokens based on a randomly shuffled element list.
- The shuffled geometry-element list increases target diversity and discourages models from memorizing typical proof patterns.The shuffled list is appended to the problem text and supplied to the model during training.
- Expression reformulation gives proving a clear sequence-prediction representation and unifies it with calculation programs in UniGeo.The resulting task still requires correspondence between the diagram, text, selected elements, and target tokens.
4 Unified Geometric Transformer
Geoformer uses a multimodal encoder-decoder and unified sequence-generation objectives to train on geometry calculation and proving together. Mathematical Expression Pretraining further adapts the model to geometry-specific solution representations.
- Geoformer jointly handles calculation and proving with a bidirectional multimodal encoder and autoregressive text decoder.Its fine-tuning stage uses calculation and proving problems simultaneously rather than optimizing separate task-specific models.
- Mathematical Expression Pretraining trains Geoformer on mathematical corpora because geometry problems differ substantially from natural-language data.
- Solution expressions are reformulated into sequences containing geometry entities, operation symbols, and numbers for prediction.Numbers are replaced with ordered NS_i tokens, and geometry elements use character-level tokenization.
- The pretraining tasks include masked language modeling and mathematical-expression prediction before unified fine-tuning.The model masks 30% of input text tokens for the masked-language-modeling task and combines the pretraining tasks.
- All pretraining and fine-tuning tasks share a text-generation objective based on negative log-likelihood.The target sequence is generated token by token from problem text and extracted diagram features.
5 Experiments
Experiments evaluate UniGeo across calculation and proving settings, showing that unified training and mathematical expression pretraining improve performance across both tasks while revealing task-specific difficulty and remaining proof failures.
- Experimental Settings: UniGeo experiments cover calculation problems, proving problems, and their unified benchmark, with accuracy and top-K proof metrics.The proving benchmark includes five sub-tasks, while proof evaluation reports top-1 and top-10 accuracy.
- Performance Comparison: 55.7% top-10 accuracy is achieved by Geoformer on proving problems, compared with 53.2% total performance for NGS.Proving performance varies substantially across sub-tasks, from 19.4% for parallel problems to 72.5% for similarity problems.
- Unified Training: 60.9% and 55.8% accuracy are obtained by unified Geoformer on calculation and proving problems, respectively, while avoiding the performance decline seen in unified NGS training.Unified NGS loses 5.0% and 5.8% on calculation and proving, whereas unified Geoformer outperforms task-specific Geoformer models on both tasks.
- Pretraining: 62.5% and 56.4% accuracy are reached after pretraining on calculation and proving problems, respectively, exceeding task-specialized NGS by 5.6% and 3.2%.The pretraining target consists of mathematical expressions extracted from calculation-problem solutions.
- Ablation Study: Combining masked language modeling and mathematical expression pretraining produces the highest 62.5% and 56.4% accuracies across the two tasks.Using masked language modeling alone does not significantly change Geoformer performance, while the combined setting improves both task types.
- Case Study: The case study shows unified Geoformer correctly solving a similar-triangle calculation where task-specialized Geoformer predicts an incorrect program, but failing on parts of a proving example.The failure includes two wrong geometry elements and omission of the final two critical proof steps.
6 Conclusion
The paper unifies geometry calculation and proving through the UniGeo benchmark, Geoformer, and mathematical expression pretraining. Experiments report strong performance across both tasks with one set of model weights.
- Method: Geoformer addresses calculation and proving simultaneously with a unified model, while mathematical expression pretraining further promotes its performance.The model handles both tasks with a single set of model weights.
- Results: Experiments report state-of-the-art performance, with Geoformer outperforming task-specialized models on both geometry tasks.The conclusion attributes this result to the unified benchmark, unified model, and mathematical expression pretraining contributions.
Limitations
The unified Geoformer still has limited accuracy on complex geometry tasks requiring high-level reasoning, while manual data construction constrains the scope and sophistication of available problems.
- Neural-network approaches remain far from real-world application accuracy on complex geometry tasks requiring high-level reasoning.
- Manual collection and annotation make mathematical logical reasoning datasets costly to construct.
- This construction burden limits the types and difficulty levels of geometry problems represented in the data.
- Restricted problem coverage can lead neural models to fail on more sophisticated geometry cases.