Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions (2026.acl-long)
Copied to clipboard
Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, Yeyun Gong
| Challenge: | Existing methods for geometry theorem proving in Euclidean geometry are challenging and require a neural network to perform. |
| Approach: | They propose a method for adding auxiliary points in geometry that runs on CPUs without relying on neural network-based inference. |
| Outcome: | The proposed method achieves silver-medal-level human performance on IMO-30 benchmark. |
Similar Papers
Towards Robust Mathematical Reasoning (2025.emnlp-main)
Copied to clipboard
Thang Luong, Dawsen Hwang, Hoang H Nguyen, Golnaz Ghiasi, Yuri Chervonyi, Insuk Seo, Junsu Kim, Garrett Bingham, Jonathan Lee, Swaroop Mishra, Alex Zhai, Huiyi Hu, Henryk Michalewski, Jimin Kim, Jeonghyun Ahn, Junhwi Bae, Xingyou Song, Trieu Hoang Trinh, Quoc V Le, Junehyuk Jung
| Challenge: | IMO-Bench is a suite of advanced reasoning benchmarks that targets the international mathematical Olympiad level. |
| Approach: | They propose IMO-Bench, a suite of advanced reasoning benchmarks that targets the level of the international mathematical Olympiad. |
| Outcome: | IMO-Bench is a suite of advanced reasoning benchmarks that targets the level of the international mathematical Olympiad. |
GeometryZero: Advancing Geometry Solving via Group Contrastive Policy Optimization (2026.findings-acl)
Copied to clipboard
| Challenge: | Existing methods for auxiliary construction training are expensive and underperform . Existing Corresponding Author training methods lack self-correction capabilities in reasoning chains. |
| Approach: | They propose a reinforcement learning framework that rewards auxiliary construction with geometric reasoning by grouping construction rewards with a Length Reward. |
| Outcome: | Experiments on Geometry3K and MathVista show that GeometryZero outperforms baselines on auxiliary constructions. |
RLMEval: Evaluating Research-Level Neural Theorem Proving (2025.findings-emnlp)
Copied to clipboard
| Challenge: | RLMEval evaluates large language models for research-level neural theorem proving and proof autoformalization . the best model achieves only a 10.3% pass rate on existing benchmarks . |
| Approach: | They propose a new evaluation suite for large language models . it evaluates research-level theorems from real-world Lean formalization projects . |
| Outcome: | RLMEval evaluates research-level theorems from real-world Lean formalization projects. |
UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression (2022.emnlp-main)
Copied to clipboard
| Challenge: | Existing work on geometry problem solving treats calculation and proving as two specific tasks hindering a deep model to unify reasoning ability on multiple math tasks. |
| Approach: | They propose a large-scale Unified Geometry problem benchmark to unify geometry on multiple math tasks. |
| Outcome: | The proposed framework outperforms the existing model with 5.6% and 3.2% accuracies on calculation and proving problems. |
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models (2023.emnlp-main)
Copied to clipboard
Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, Qun Liu
| Challenge: | Automated theorem proving (ATP) benchmarks focus on symbolic inference but rarely involve understanding complex number combination reasoning. |
| Approach: | They propose a benchmark that requires a model to reduce a trigonometric expression with step-by-step proof and evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
| Outcome: | The proposed benchmark evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models (2026.acl-long)
Copied to clipboard
| Challenge: | Existing evaluation frameworks for large reasoning models are saturated by a lack of reliable and verifiable benchmarks. |
| Approach: | They propose a rigorously curated, Olympiad-level math benchmark comprising 350 problems, each with parallel English and Chinese versions. |
| Outcome: | The proposed benchmark unifies two evaluation paradigms and offers 150 problems formalized in Lean 4 for rigorous process-level evaluation. |
GOLD: Geometry Problem Solver with Natural Language Description (2024.findings-naacl)
Copied to clipboard
| Challenge: | Existing methods for solving geometry math problems struggle with accurately interpreting geometry diagrams, posing a challenge for problem-solving. |
| Approach: | They propose a model that extracts geometric relations from diagrams and converts them into natural language descriptions. |
| Outcome: | The proposed model outperforms the previous best method on the UniGeo dataset by 12.7% and 42.1% in calculation and proving subsets. |
An Augmented Benchmark Dataset for Geometric Question Answering through Dual Parallel Text Encoding (2022.coling-1)
Copied to clipboard
| Challenge: | Existing methods for solving geometric problems are limited due to lack of high-quality datasets and efficient neural solvers. |
| Approach: | They propose to annotate 2,518 geometric problems with richer types and greater difficulty using a benchmark dataset. |
| Outcome: | The proposed method improves the accuracy of automatic geometric problem solving to 66.09%. |
Neural Unification for Logic Reasoning over Natural Language (2021.findings-emnlp)
Copied to clipboard
| Challenge: | Automated Theorem Proving (ATP) is a computer program that can show that conjectures are logical consequences of a set of axioms. |
| Approach: | They propose a transformer-based architecture for deriving conjectures given axioms . they propose 'neural unifier' and relative training procedure to train the model . |
| Outcome: | The proposed architectures are able to answer queries with deep queries with a relatively low training time. |
Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning (2021.acl-long)
Copied to clipboard
| Challenge: | Existing methods for solving geometric problems are either small in scale or not publicly available. |
| Approach: | They propose a large-scale benchmark for geometric problem solving using formal language and symbolic reasoning. |
| Outcome: | The proposed approach parses geometry problems into formal language and performs symbolic reasoning step by step. |