Paper deep dive
GeoChallenge: A Multi-Answer Multiple-Choice Benchmark for Geometric Reasoning with Diagrams
Yushun Zhang, Weiping Fu, Zesheng Yang, Bo Zhao, Lingling Zhang, Jian Zhang, Yumeng Fu, Jiaxing Huang, Jun Liu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 7/20/2026, 12:23:30 PM
Summary
The paper introduces GeoChallenge-90K, a large-scale benchmark for evaluating geometric reasoning in Large Language Models (LLMs). It consists of 90,279 automatically generated multiple-choice geometry proof problems with aligned text and diagrams. The study highlights a significant performance gap between state-of-the-art LLMs (besting at ~76% accuracy) and human solvers (~95%), identifying failure patterns such as weak visual reliance and overextended reasoning.
Entities (6)
Relation Signals (5)
GeoChallenge-90K → contains → 90,279 problems
confidence 98% · GeoChallenge-90K, a dataset of 90,279 automatically generated multiple-choice geometry proof problems
GeoChallenge-90K → evaluates → LLMs
confidence 95% · Evaluating the symbolic reasoning of large language models (LLMs) calls for geometry benchmarks... We introduce GeoChallenge
gpt-5-nano → achievesaccuracyon → GeoChallenge-90K
confidence 92% · the best-performing model, GPT-5-nano, achieves 75.89 exact match
Human → outperforms → gpt-5-nano
confidence 90% · the best-performing model, GPT-5-nano, achieves 75.89 exact match vs. 94.74 for humans
AlphaGeometry → usedfor → deduction
confidence 90% · We use AlphaGeometry (Trinh et al., 2024) for deduction with a rule setR
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Evaluating the symbolic reasoning of large language models (LLMs) calls for geometry benchmarks that require multi-step proofs grounded in both text and diagrams. However, existing benchmarks are often limited in scale and rarely provide visually grounded multiple-choice questions, limiting reliable evaluation of complex reasoning. We introduce GeoChallenge, a dataset of 90K automatically generated multiple-choice geometry proof problems, each requiring multi-step reasoning over aligned textual descriptions and diagrams. GeoChallenge provides fine-grained complexity ratings and formal language annotations to enable controlled evaluation. Experiments on multiple advanced LLMs show a clear performance gap between models and humans (the best-performing model, GPT-5-nano, achieves 75.89 exact match vs. 94.74 for humans). Further analysis also reveals three common failure patterns of LLMs: (1) exact match failures under the multiple-choice setting; (2) weak visual reliance; and (3) overextended reasoning without convergence.
Tags
Links
- Source: https://arxiv.org/abs/2603.19252v1
- Canonical: https://arxiv.org/abs/2603.19252v1
Trouble viewing inline? Open PDF directly →
Full Text
66,442 characters extracted from source content.
Expand or collapse full text
GeoChallenge: A Multi-Answer Multiple-Choice Benchmark for Geometric Reasoning with Diagrams Yushun Zhang 1,2 , Weiping Fu 1,2 , Zesheng Yang 1,2 , Bo Zhao 1,2 , Lingling Zhang 1,2 , Jian Zhang 1,2 , Yumeng Fu 1,2 , Jiaxing Huang 1,2 , Jun Liu 1,2 , 1 School of Computer Science and Technology, Xi’an Jiaotong University, Xi’an, China, 2 Shaanxi Province Key Laboratory of Big Data Knowledge Engineering, Xi’an, China Abstract Evaluating the symbolic reasoning of large language models (LLMs) calls for geome- try benchmarks that require multi-step proofs grounded in both text and diagrams. However, existing benchmarks are often limited in scale and rarely provide visually grounded multiple- choice questions, limiting reliable evaluation of complex reasoning. We introduce GeoChal- lenge, a dataset of 90K automatically generated multiple-choice geometry proof problems, each requiring multi-step reasoning over aligned tex- tual descriptions and diagrams. GeoChallenge provides fine-grained complexity ratings and formal language annotations to enable con- trolled evaluation. Experiments on multiple advanced LLMs show a clear performance gap between models and humans (the best-performing model, GPT-5- nano, achieves 75.89 exact match vs. 94.74 for humans). Further analysis also reveals three common failure patterns of LLMs: (1) exact match failures under the multiple-choice set- ting; (2) weak visual reliance; and (3) overex- tended reasoning without convergence. 1 1 Introduction Geometry problem solving is a fundamental task involving spatial reasoning and symbolic deduc- tion (Trinh et al., 2024; Chervonyi et al., 2025; Pan et al., 2025; Dai et al., 2025), and is widely used to evaluate complex reasoning in large language models (LLMs) (Luo et al., 2025; Feng et al., 2025; Zhang et al., 2025c). Yet evaluating such capabili- ties of LLMs in a systematic and scalable manner remains an open challenge (Lei et al., 2024; Har- iharan et al., 2025; Xu et al., 2025; White et al., 2025; Kazemi et al., 2023). Geometry datasets and benchmarks have pro- gressed along two complementary lines. Early ef- forts such as Geometry3K (Lu et al., 2021) and 1 Codes and resources will be available at:https:// github.com/fanhualiushang/GeoChallenge ID: gen_318945 Question_en: Given square ABCD. ...... the midpoints of CB, GB, respectively. A_en: BM:DM ≠ GI:HK B_en: ∠(BD-FM) = ∠FHC C_en: H,I,K are collinear D_en: AM is perpendicular to EI Answer: BD FormalText: a b c d = isquare a b c d; ...... ; j k l m = centroid j k l m g c b Prior_Difficulty: 411.5, _ ProofSteps_A: 001. B,C,J are collinear [14] & JC = JB [15] ⇒ J is midpoint of BC [26], ..... Posterior Difficulty:0.0000, . A B C D E F G H I J K M ・ ・ ・ ・ ・ ・ ・ ・ ・ ・ ・ ・ Figure 1: Examples in GeoChallenge-90K dataset. GeoQA (Chen et al., 2021) translate diagram– text problems into machine-interpretable struc- tures (e.g., symbolic relations or executable pro- grams), enabling systematic evaluation of geomet- ric reasoning. More recent benchmarks, including MathVerse (Zhang et al., 2024b) and Olympiad- Bench (He et al., 2024), target multimodal (Zhang et al., 2025b) and emphasize faithful diagram un- derstanding in harder visual-math settings. How- ever, reliable evaluation remains challenging: many datasets are manually curated from textbooks or contests, which limits coverage and scalability, and high-difficulty benchmarks stay small due to ex- pert verification costs. Moreover, prevailing single- answer multiple-choice (Feng et al., 2025; Wang et al., 2025; Xing et al., 2024) or open-ended for- mats (Zhang et al., 2025a; Fu et al., 2025b) are ei- ther prone to guessing or difficult to grade at scale. Finally, text–diagram misalignment persists, weak- ening visually grounded evaluation, as highlighted by GeoGPT4V (Cai et al., 2024). To address these issues, we propose a scal- able automatic generation pipeline and introduce GeoChallenge-90K, a dataset of 90,279 challeng- ing geometry proof questions. Each instance pro- vides an aligned textual description, a rendered dia- gram, and four candidate options with possibly mul- tiple correct answers, enabling option-level evalu- ation and discouraging elimination-style guessing. 1 arXiv:2603.19252v1 [cs.CL] 25 Feb 2026 GeoChallenge-90K covers a wide range of proof length (avg. 16.72 steps), diagram complexity, and difficulty, with fine-grained complexity ratings to support controlled stress tests. Experiments on GeoChallenge-90K reveal a large gap between current models and human solvers. General-purpose models average 21.48% accuracy, reasoning-oriented models reach 56.07%, and humans achieve 94.74%. Hierarchical evalu- ation shows that general-purpose models degrade steeply with increasing complexity, whereas hu- mans and reasoning-specialized models remain comparatively stable. Diagram ablations expose a grounding gap: removing diagrams substantially re- duces human accuracy but only marginally affects models, suggesting that current LLMs do not reli- ably extract or calibrate diagram evidence. Error analysis further indicates recurring failures-logical fallacies, invalid outputs, and overextended rea- soning with no verifiable conclusion-while human mistakes are mostly genuine reasoning slips rather than format-related failures. In summary, our main contributions are: •We introduce GeoChallenge-90K, a multi- answer multiple-choice benchmark for diagram-groundedgeometricreasoning, with aligned text–diagram pairs, formal annotations, and fine-grained complexity control. •Extensive experiments provide system- atic empirical evidence that a substantial model–human gap persists on challenging, long-step geometric reasoning, even under rigorous, option-level no-guess evaluation. •Diagnostics reveal large gaps between strict exact match and option-level metrics, weak and inconsistent diagram grounding, and fre- quent answer inconsistency or non-convergent long-step reasoning. 2 Related Work 2.1 Geometry Problem Generation Early geometry datasets were built via templates or manual collection andannotation (Prasetyanto et al., 2020; Kazemi et al., 2023; Zhang et al., 2024c; Chen et al., 2021; Lu et al., 2021; Chen et al., 2022), which produced valuable resources but faced scalability and coverage limits. Sym- bolic generation alleviates these issues by mak- ing problems machine-verifiable: Inter-GPS (Lu et al., 2021) provides parsing/representation, Ge- oGen (Bak, 2020) generates symmetric instances, FormalGeo (Zhang et al., 2023b) formalizes verifi- cation, and R-CoT (Deng et al., 2024a) increases QA diversity. More recently, theorem-guided and verified pipelines further scale generation and align- ment, including TR-CoT (Deng et al., 2024b), Gen- esisGeo (Zhu et al., 2025), and TrustGeoGen (Fu et al., 2025a). LLMs/MMs introduce another paradigm. G- LLaVA (Gao et al., 2023) synthesizes Geo170K with text LLMs, while GeoGPT4V (Cai et al., 2024) leverages GPT-4V/Wolfram to improve dif- ficulty and image–text alignment, demonstrating scalable, targeted generation (Chen et al., 2024; Li et al., 2024). 2.2 Existing geometry datasets Geometry benchmarks range from early text– diagram datasets (e.g., GeoS (Seo et al., 2015)) to large-scale, richly annotated corpora such as Geom- etry3K (Lu et al., 2021), GeoQA/GeoQA+ (Chen et al., 2021; Cao and Xiao, 2022), UniGeo (Chen et al., 2022), and PGPS9K (Zhang et al., 2023a), which provide formal languages, programmatic so- lutions, and detailed diagram annotations. Geo- Laux (Fu et al., 2025b) further targets long-step reasoning with auxiliary-line constructions. With LLMs/MMs, benchmarks increasingly stress multimodal understanding, robustness, and perception, including MATH (Hendrycks et al., 2021), GeoEval (Zhang et al., 2024a), M- MATH (Sun et al., 2024), GePBench (Xing et al., 2024), and FrontierMath (Glazer et al., 2024). 3 The GeoChallenge-90K dataset 3.1 Definitions We first introduce the core concepts used in our automatic data generation procedure. Concrete ex- amples are provided in Appendix A. Clause. A clause is a statement that specifies a geometric relation among a set of points and exist- ing objects (e.g., points, lines, circles): f (X 1 ,X 2 ,...,X n ), wherefis a predefined relation andX 1 ,X 2 ,..., X n are already-defined points. All predefined clauses are listed in table 7. 2 Large-scale premises sampling Challenging options generation Symbolic rea- soning engine Evaluator and ranker rule-based translator Graph engine one premise a b c = right_triangle; d = midpoint a b; e = midpoint a c Premises Conclusion set Top-4 challeng- ing conclusions rewrite 4 options decom- position check if used Simplified problem Plain text pro- blem expression Image of the problem ab ⊥ ac a,b,d are collinear ad = bd ...... a b c = right_triangle; d = midpoint a b; e = midpoint a c de // bc de:bc = 1/2 ∠ade = ∠abc ∠aed = ∠acb de // bc de:bc = 1/4 ∠ade = ∠abc ∠aed ≠ ∠acb one premise de // bc de:bc = 1/4 ∠ade = ∠abc ∠aed ≠ ∠acb 4 options a b c = triangle; ab ⊥ ac d = midpoint a b; e = midpoint a c a b c = triangle; d = midpoint a b; e = midpoint a c a b c = right_triangle; d = midpoint a b; e = midpoint a c Initialize a shape a b c = right_triangle = midpoint rename d = midpoint a b depth sufficient ? a b c = right_triangle merge N Y possible premise Symbol refinement predefined constructions Annealing - based sample Figure 2: Pipeline of dataset generation Construction. A construction is a geometric de- scription that uses one or two clauses to uniquely define a new pointx; when two clauses are given, x is taken as their intersection: Construction x = f (),g(), wherefandgare clauses, andg()may be omitted if f () alone uniquely determines x. Premise. A premise is an ordered sequence of constructions that defines all points and relations in a problem: Premise = (Construction 1 ,Construction 2 , ...,Construction n ). Problem.A problem is a structured task or ques- tion, which consists of a premise and four multiple- choice options (possibly with multiple correct an- swers): Problem = (Premise,Option 1 ,Option 2 , Option 3 ,Option 4 ). (1) See Figure 1 for an example. 3.2 Problem Generation 3.2.1 Large-scale premises sampling We generate a large pool of premises by composing predefined clause templates into multi-layer geo- metric constructions. Starting from a minimal seed at depth0, we iteratively add layers until a target depth is reached. At each layer, we sample one or two templates and instantiate them with valid arguments from currently defined entities, ensuring consistency, then append the resulting clauses to the premise. To balance diversity and tractability, we perform breadth-first expansion with a gradually shrink- ing branching factor (annealing-style): early lay- ers explore more template/parameter combinations, while later layers prune candidates to avoid combi- natorial explosion. We set the maximum depth to N = 8, producing 871,828 sampled premises. 3.2.2 Challenging options generation Given a premise, we enumerate provable conclu- sions using a symbolic engine, score their difficulty, and select the top-scoring ones as the four options. We use AlphaGeometry (Trinh et al., 2024) for de- duction with a rule setR(theorem matching and al- gebraic derivation). As summarized in Appendix B, the engine performs conclusion search via forward chaining, repeatedly applying rules inRto newly derived facts until saturation or a preset depth limit. Following GeoEval (Zhang et al., 2024a), we de- fine difficulty as a weighted sum of five indicators: prior_difficulty = P 5 i=1 w i x i , wherex 1 is descrip- tion length,x 2 premise length,x 3 the number of points,x 4 proof-search depth, andx 5 proof length. We choose four conclusions with the highest scores, treat one as the correct option, and generate hard distractors via equivalence-preserving rewrites, re- lation negation (e.g., equality/parallelism), or ratio perturbation, requiring each distractor to be falsi- fiable under the premise. We avoid naive entity substitution (e.g.,AB ⊥ CD → AB ⊥ CE), which often yields degenerate or accidentally true options. 3.2.3 Symbol refinement We then refine the symbolic instances and render aligned diagrams. Text refinement includes (i) sim- 3 DatasetSizeAGIFCRAvg PLAvg DLFALTQT GeoS (Seo et al., 2015)186%T, I%NA23.34%ENSA MATH (Hendrycks et al., 2021)12,500% T only"5.48202.66%ENOE Geometry3K (Lu et al., 2021)3,002%T, I%NA12.19"ENSA GeoQA (Chen et al., 2021)5,010%T, I%2.7752.46%ZHSA UniGeo (Chen et al., 2022)9,543%T, I%2.5716.23"ENSA, OE GPSM8K (Cobbe et al., 2021)8,790% T only%4.5945.27%ENOE PGDP5K (Hao et al., 2022)5,000% I only%–"– PGPS9K (Zhang et al., 2023a)9,022%T, I%2.439.46"ENOE MathVista (Lu et al., 2023)6,141%T, I%–83.83%EN, ZHSA, OE GeomVerse (Kazemi et al., 2023)9,303"T, I"6.3553.09"ENOE Geo170K (Gao et al., 2023)177,457"T, I%6.2149.01%ENSA GeoEval (Zhang et al., 2024a)5,050%T, I"2.5528.34"ENSA, OE M-MATH (Sun et al., 2024)5,929%T, I%8.5048.50%ENOE AutoGeo-100K (Huang et al., 2025)100,000" I only"–22.41"EN– MathVerse (Zhang et al., 2024b)15,672%T, I"–40.67%ENSA GeoMM (Deng et al., 2024a)33,595"T, I"1.5132.47%ENOE Average----3.9244.98--- GeoChallenge-90K90,279"T, I"16.7239.15"EN, ZHMA Table 1: Comparison between GeoChallenge-90K benchmark and existing geometry problem solving benchmarks. AG: Automatic Generation. IF: Input Format, T for text and I for image. CR: Complexity Rating. Avg PL: Average Proof Length. Avg DL: Average Description Length. FA: Formal Annotation. LT: Language Type, EN for English and ZH for Chinese. QT: Question Type, SA for single-answer, MA for multiple-answer and OE for open-ended question plification by retaining only points/clauses used in both the premise and the proofs of candidate options, and (i) bilingual rendering that maps the formal representation to English and Chinese with rule-based templates while preserving option se- mantics. For diagrams, we render figures consistent with the refined premise and explicitly annotate candi- date options for visual grounding. To support stable batch rendering beyond the default AlphaGeome- try module, we add rule-based option labeling and robustness fixes to prevent incomplete annotations and occasional non-termination. 3.2.4 Manual Verification Since symbolic descriptions cannot fully guaran- tee presentation quality, we perform manual ver- ification as a quality-control filter for the visual- izations used in the benchmark. Annotators check (i) readability, legible, unobstructed labels, (i) geometric validity,the drawing satisfies declared relations, and (i) description alignment,required elements present; no contradictory extras. Only fig- ures passing all checks are kept; otherwise they are discarded. This step does not modify the symbolic pipeline and serves purely as visualization quality control. GeoChallenge-90K is designed to evaluate diagram-grounded geometry theorem proving un- ModelMATH Geome- try3K GeoCha- llenge Gemini 1.5 Pro82.1973.8824.45 Claude 3.5 Sonnet58.0571.6521.81 GPT-4o57.7264.9217.51 Table 2: Performance comparison of different bench- marks der rigorous, scalable, and controllable settings. Built on the fully automatic symbolic pipeline in Section 3.2, all instances are machine-verifiable, en- abling scalable construction without manual proof annotation.It exhibits six key characteristics: multi-answer MCQ evaluation, automatic gener- ation, comprehensive geometric coverage diver- sity, dual-modality inputs, bilingual consistency, fine-grained complexity rating. Table 1 compares GeoChallenge-90K with representative geometry and multimodal math benchmarks. 3.3 Features of GeoChallenge-90K Multi-answer MCQ evaluation. A distinctive feature of GeoChallenge-90K is its multi-answer MCQ format, where an instance may contain more than one correct option. Compared to single- answer MCQs, this setting substantially weakens elimination-style guessing and forces per-option verification: models must assess each candidate conclusion under the premise, often requiring dif- 4 ModelEMA↑EME↑EMM↑EMH↑P↑R↑F1↑HA↑Avg #Sel Baselines Random6.256.256.256.2550.0050.0050.0046.882.13 General-Purpose Models GPT-4o17.5129.0913.819.2452.8768.8359.8158.622.18 Claude 3.5 Sonnet21.8127.2722.9410.8754.8871.7362.1963.222.20 Gemini 1.5 Pro24.4538.1822.279.2462.3176.7968.7969.742.01 llava-1.5-7B16.9637.8210.691.0948.3131.3638.0357.871.03 Qwen2-VL-7B26.6559.6417.370.061.3647.4453.5165.691.19 Reasoning-Oriented Models GPT-o367.8467.2769.0465.7680.8481.2081.0282.521.64 GPT-5-nano75.8970.5979.3175.0084.8283.7884.3085.491.61 Claude 4.5 Sonnet41.9650.0041.3830.0072.0277.9074.8576.561.75 Gemini 3 Pro38.6050.0037.2923.8144.7441.4543.0343.201.04 Human Performance Human94.7494.1294.9295.2497.9599.7198.8298.681.66 Table 3: Overall performance on GeoChallenge with both text and images provided. EMA/EME/EMM/EMH report Exact Match (EM) on the All/Easy/Medium/Hard splits, respectively. ferent proof paths or relation checks. This format supports option-level metrics and diagnoses over- /under-selection behaviors. Long-step Proofs under Concise Statements. GeoChallenge-90K targets long-step deduction. Proofs average 16.72 steps-over4×typical geom- etry benchmarks (3.92)-while statements remain similarly concise (39.15 vs. 44.98 words). This is by design that descriptions include only essen- tial relations, increasing information density per token and thus reasoning difficulty. As shown in Table 2, models suffer a clear accuracy drop on GeoChallenge-90K relative to prior benchmarks, making it a more challenging and more diagnostic testbed. Comprehensive geometric coverage and struc- tural diversity. Beyond scale, GeoChallenge- 90K is constructed to cover a broad range of ge- ometric primitives and composite structures. Fig- ure 3 summarizes the distribution of geometric ele- ments. Importantly, less frequent shapes in many benchmarks, such as trapezoids and parallelograms, are still represented at scale over 10K instances each, which improves coverage of cross-element interactions and mitigates sparsity for rare configu- rations. Dual-modality and bilingual alignment. Each instance includes both text and a rendered diagram, and the two modalities are semantically aligned: the textual statement fully specifies the geometric conditions reflected in the diagram. This align- ment enables controlled evaluation of text-only ver- sus diagram-grounded reasoning (text+image), and also facilitates vision-only studies when needed. We further provide English and Chinese versions with strict semantic equivalence, reducing con- founds from translation artifacts and enabling sys- tematic analysis of language effects. Rich annotations and controlled difficulty. GeoChallenge-90K includes structured formal rep- resentations for premises and options, along with two complementary difficulty signals: a prior dif- ficulty estimated from complexity indicators, and posterior difficulty derived from tested models’ per- formance. Problems are stratified into three diffi- culty levels with a 3:5:2 split, enabling controlled stress testing and fine-grained performance analy- sis. 4 Experiments 4.1 Experimental Setup Prompting / Inference Settings.We adopt a uni- fied prompting protocol across all evaluated mod- els. A single prompt template (included in the supplementary material due to length) is used for every example to elicit a final multiple-choice an- swer along with brief, option-wise reasoning. We disable external tools and retrieval for all models. Inference is run with greedy decoding (tempera- ture=0.0) and a maximum output length of 16,384 tokens; consequently, each instance is evaluated with one generation only, without additional sam- pling or self-consistency aggregation. Models Evaluation. To establish a human base- line, we recruited two graduate-level testers with relevant mathematical background. Each prob- lem was translated into their native language, and testers answered under a strict 3-minute limit. No- 5 Circle 74579 Collinear 12689 Equality 104178 Other 5413 Parallel line 15102 Parallelogram 14731 Rectangle 12573 Square 26180 Trapezoid 15725 Triangle 56212 Vertical line 47902 Geometry Elements Figure 3: Geometry elements in GeoChallenge-90K tably, since many items admit correct responses via direct diagram interpretation without a fully formal derivation, the reported human score may reflects a mixture of visual judgment and mathematical reasoning under the same constraint. We evaluate prominent open-source and closed- source large models selected for strong mathe- matical reasoning, covering (i) general-purpose LMM/LLMs and (i) reasoning-oriented models that allocate extra computation for deliberate rea- soning. In the multimodal setting, we test GPT- 4o (Hurst et al., 2024), Claude 3.5 Sonnet (An- thropic, 2024), Gemini 1.5 Pro (Team et al., 2024), LLaVA-1.5-7B (Liu et al., 2024), and Qwen2- VL-7B-Instruct (Yang et al., 2024), as well as reasoning-oriented models including GPT-o3-2025- 04-16 (OpenAI, 2025a), GPT-o3-mini-2025-01- 31 (OpenAI, 2025b), Claude 4.5 sonnet-20250929- thinking (Anthropic, 2025), and Gemini-3-pro- preview-11-2025 (Google, 2025). For text-only evaluations (LLM setting), we assess the same model families without visual inputs, and addition- ally include Deepseek-r1-0528 (DeepSeek-AI et al., 2025), Qwen3-235b-a22b-thinking-2507 (Yang et al., 2025), and WizardMath-7B (Luo et al., 2023). For replicability and efficiency, we run most eval- uations on GeoChallenge-small, a standardized sub- set of 908 problems sampled to match the difficulty profile of the full benchmark, enabling practical assessment of closed-source models. Evaluation Protocol. We evaluate LLMs on a multi-select benchmark. For each problemiwith K i options, the model predicts a subset ˆ S i ⊆ 1,...,K i , compared against the ground-truth subset S i . We report Exact Match (EM), which is cor- rect iff ˆ S i = S i , both overall and by difficulty (Easy/Medium/Hard) determined by our difficulty scores. To measure partial correctness, we com- pute option-level precision/recall/F1 from the over- lap between ˆ S i andS i and report macro-averages across problems. We also report Hamming Loss (HL), the average per-option error rate: HL = 1 N N X i=1 1 K i K i X j=1 1(ˆy i,j ̸= y i,j ), wherey i,j , ˆy i,j ∈ 0, 1are the ground-truth and predicted labels; we report Hamming Accuracy (HA) as1− HL. Finally, we report the average number of selected optionsE[| ˆ S i |]to characterize selection behavior. 4.2 Main Results We report overall results on GeoChallenge with both text and diagrams provided in Table 3. Since GeoChallenge is formulated as multiple-choice with long-step reasoning, we emphasize Exact Match as the primary metric; in contrast, option- level metrics (P/R/F1 and HA) may still reward partially correct selections even when the predicted answer is not fully correct. No-guess multiple-choice reveals hidden diffi- culty. Under the no-guess protocol, the bottle- neck shifts from partially identifying correct op- tions to producing a single, answer-consistent pre- diction. A key observation is the large gap between strict EM and option-level metrics, especially for general-purpose models: e.g., Gemini 1.5 Pro at- tains high F1/HA but much lower EMA, with simi- lar discrepancies for GPT-4o and Claude 4.5 Son- net. This indicates that models often recover parts of the correct option answer yet fail to output the exact answer demanded by the no-guess protocol, making heuristics such as eliminating a few options or selecting multiple plausible answers ineffective. Consistently, Avg #Sel shows that general models select close to two options on average (near the ran- dom baseline), trading precision for recall, whereas reasoning-oriented systems are better calibrated and closer to human selection cardinality. Human–model gap on long-step geometry. GeoChallenge exhibits a substantial human-model gap even with reasoning-oriented systems, and the gap remains on the Hard split. The best model in Table 3 (GPT-5-nano) remains obviously be- low human EMA, and the gap persists on the 6 ModelEMA↑EME↑EMM↑EMH↑P↑R↑F1↑HA↑Avg #Sel Baselines Random6.256.256.256.2550.0050.0050.0046.882.13 General-Purpose Models GPT-4o13.9932.008.690.043.7555.8949.0848.622.14 Claude 3.5 Sonnet17.6232.7315.370.5451.4363.4856.8360.212.02 Gemini 1.5 Pro20.5944.0014.700.060.3274.1466.5266.771.97 WizardMath-7B8.159.457.807.0738.4859.3246.6849.782.40 Reasoning-Oriented Models GPT-o3-mini67.8467.2769.0465.7680.8481.2081.0282.521.64 GPT-o362.6766.1860.8061.9672.9571.4172.1772.601.59 Claude 4.5 Sonnet36.2351.6434.3017.9366.5867.3666.9771.341.62 Gemini 3 Pro51.2162.5549.0039.6757.5454.5556.0155.971.37 Deepseek r116.4117.8216.7013.5923.1627.0024.9423.542.08 Qwen3-235b-thinking75.5581.0975.9566.3082.1882.3082.2482.741.58 Human Performance Human42.8638.2446.5540.0066.9668.7567.8572.771.69 Table 4: Overall performance on GeoChallenge with text-only provided. EMA/EME/EMM/EMH report Exact Match (EM) on the All/Easy/Medium/Hard splits, respectively. Hard split; meanwhile, general multimodal base- lines lag far behind. This suggests the bench- mark separates systems that sustain long-step, answer-consistent reasoning from those that suc- ceed mainly via partial correctness or shallow heuristics. Reasoning-oriented models achieve rel- atively strong P/R/F1, implying they often locate relevant options, but their remaining deficit under strict EM points to unresolved challenges in multi- step consistency, diagram-grounded verification, and satisfying global geometric constraints. Different degradation with increasing difficulty. As difficulty increases from Easy to Hard, general- purpose models often degrade sharply-sometimes approaching collapse-whereas reasoning-oriented systems decline more moderately and humans re- main the most stable. General models typically drop steeply from Easy to Hard, indicating that success on simpler items does not reliably transfer to long-horizon, high-constraint geometric reason- ing. In contrast, reasoning-oriented systems better preserve performance as complexity grows. These trends suggest that higher difficulty mainly ampli- fies failure modes tied to partial-cue reliance, while globally consistent reasoners are more robust under increasing constraints. 5 Detailed Findings and Analysis We next elaborate on the three findings highlighted in the Abstract and Introduction: (1) exact-match failures under the no-guess multi-answer setting, (2) weak and inconsistent visual reliance, and (3) overextended reasoning without convergence. Finding 1: Exact-match fragility under no-guess multi-answer MCQ. Under the no-guess pro- tocol, most general-purpose models fail by com- mitting to an incorrect final option answer, sug- gesting that the primary bottleneck is the answer consistency rather than partial option identifica- tion. We categorize each prediction into four mutu- ally exclusive outcomes: RIGHT_ANSWER (exact match), WRONG_ANSWER (committed but incor- rect), NO_ANSWER (uncommitted answer), and OUT_OF_LENGTH (truncation). Figure 4 shows that general-purpose models are largely driven by WRONG_ANSWER (roughly three quarters), while NO_ANSWER varies widely across systems, reflect- ing different uncertainty-handling behaviors. In contrast, reasoning-oriented models exhibit more structured trade-offs (higher RIGHT_ANSWER with mild abstention), motivating us to report error-type composition alongside EM. Additional evidence: Language shift stresses exact match. Strict EMA is more sensitive to English→Chinese reformulation than option-level metrics, indicating that linguistic changes can break exact answer consistency even when models still identify relevant options. We evaluate general- purpose models under Chinese prompts and com- pare them with English prompts to assess cross- lingual robustness, and observe a recurring over- selection pattern under Chinese prompts (higher Avg #Sel): this can maintain or even improve F1/HA, yet lowers EMA because any extra or missed option turns an exact match into zero under the no-guess protocol (see Appendix 5 for detailed results). 7 17.51% 74.34% 8.15% GPT-4o 21.81% 76.87% 1.32% Claude 3.5 Sonnet 24.45% 75.22% 0.33% Gemini 1.5 Pro 16.96% 80.40% 2.64% llava-1.5-7B 26.65% 73.35% Qwen2-VL-7B 67.84% 25.55% 6.61% GPT-o3 76.11% 16.81% 0.88% 6.19% GPT-5-nano 42.48% 57.52% Claude 4.5 Sonnet 8.15% 87.67% 4.19% WizardMath-7B 38.94% 7.08% 5.31% 48.67% Gemini 3 Pro 67.84% 25.55% 6.61% GPT-o3-mini 16.41% 15.20% 6.39% 62.00% Deepseek r1 75.55% 11.12% 0.11% 13.22% Qwen3-235b-thinking 94.69% 5.31% human Right answerWrong answerNo answerOut of length Figure 4: Error type across different models Finding 2: Weak and inconsistent diagram grounding. Humans rely heavily on diagrams, whereas current LLMs under-use or inconsistently integrate visual evidence. To probe diagram re- liance, we compare multimodal (text+image) per- formance against text-only performance, and ad- ditionally report a human text-only baseline. Hu- mans show strong dependence on diagrams: re- moving the diagram causes a 51.88 EMA drop, while option-level quality remains comparatively strong, suggesting that people can partially recon- struct the figure from text and preserve partial cor- rectness even when exact selection becomes harder. In contrast, most LLMs are only weakly diagram- dependent: performance usually declines but not catastrophically, and the benefit of visual input is in- consistent across models; in some cases, text-only can even outperform multimodal. Overall, diagram usage emerges as a key capability dimension: hu- mans treat diagrams as the primary substrate for geometry, whereas current LLMs do not reliably ground deductions in visual evidence. Finding 3: Overextended reasoning without con- vergence.A non-trivial fraction of failures stems from non-convergent long-step reasoning that does not reach a stable final selection within the decod- ing budget, recorded as OUT_OF_LENGTH. With max_tokens=16,384, OUT_OF_LENGTH typically indicates that the model keeps expanding or revis- ing its reasoning without committing to a verifiable answer set, rather than being merely verbose. This failure mode is especially visible in models that attempt prolonged, open-ended deliberation (e.g., DeepSeek-R1 in Figure 4), and it becomes increas- ingly harmful under strict EM: even near-correct intermediate judgments are not credited unless the model converges to a final, consistent option set. 6 Conclusion In this work, we presented GeoChallenge-90K, a large-scale benchmark for evaluating diagram- grounded geometry theorem proving in a rigorous and scalable setting. Our benchmark is constructed through a symbolic generation-and-verification pipeline, provides aligned text-diagram inputs with bilingual consistency, and exposes controllable complexity for fine-grained analysis. To better reflect real reasoning ability, we further adopt a no-guess, multi-answer multiple-choice protocol that enables strict exact-match evaluation while still allowing complementary option-level diagnostics. Across comprehensive experiments and analy- ses, GeoChallenge-90K consistently separates shal- low pattern matching from long-step, globally con- sistent reasoning: current general-purpose models struggle under strict evaluation, reasoning-oriented models improve substantially yet remain behind human solvers, and the gap widens as complexity increases. Our diagnostic studies suggest that the remaining challenges are not merely harder prob- lems, but failures in answer consistency, conver- gence, and reliable integration of diagram evidence. We hope GeoChallenge-90K will serve as a prac- tical testbed for developing and measuring future systems that reason over long proofs, verify global constraints, and ground deductions in diagrams more reliably. 8 7 Limitations Our work has three main limitations. First, while GeoChallenge-90K supports rigorous outcome- level evaluation (e.g., strict exact match, option- level metrics, and error-type composition), we do not conduct fine-grained, step-by-step process analyses to localize errors to specific intermedi- ate decisions or proof-state transitions.Second, al- though complexity control and text-only ablations are useful diagnostics, they do not causally iden- tify why models fail. They suggest weaknesses in visual grounding and long-step consistency, but cannot pinpoint which visual cues (e.g., anno- tations or intersections) or reasoning operations (e.g., parsing or constraint propagation) are the primary error sources; targeted perturbation stud- ies would be needed.Third, some failure modes- notably NO_ANSWER and OUT_OF_LENGTH-are sensitive to prompting and decoding choices. Varia- tions in answer-format constraints, refusal behavior, or search strategies can shift abstention and non- convergence rates, affecting error-type composition even when underlying competence is similar. References Anthropic. 2024. Claude 3.5 sonnet model card adden- dum. Technical report, Anthropic. Anthropic. 2025. Introducing claude sonnet 4.5. Tech- nical report, OpenAI. Patrik Bak. 2020. Geogen.https://github.com/ PatrikBak/GeoGen. Accessed April 22, 2025. Shihao Cai, Keqin Bao, Hangyu Guo, Jizhi Zhang, Jun Song, and Bo Zheng. 2024. Geogpt4v: To- wards geometric multi-modal large language models with geometric image generation. arXiv preprint arXiv:2406.11503. Jie Cao and Jing Xiao. 2022. An augmented benchmark dataset for geometric question answering through dual parallel text encoding. In Proceedings of the 29th international conference on computational lin- guistics, pages 1511–1520. Jiaqi Chen, Tong Li, Jinghui Qin, Pan Lu, Liang Lin, Chongyu Chen, and Xiaodan Liang. 2022. Uni- geo: Unifying geometry logical reasoning via re- formulating mathematical expression. arXiv preprint arXiv:2212.02746. Jiaqi Chen, Jianheng Tang, Jinghui Qin, Xiaodan Liang, Lingbo Liu, Eric P Xing, and Liang Lin. 2021. Geoqa: A geometric question answering benchmark towards multimodal numerical reasoning. arXiv preprint arXiv:2105.14517. Xinyun Chen, Ryan A Chi, Xuezhi Wang, and Denny Zhou. 2024.Premise order matters in reason- ing with large language models. arXiv preprint arXiv:2402.08939. Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xi- aomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le, and Thang Luong. 2025. Gold-medalist performance in solving olympiad geometry with alphageometry2. Preprint, arXiv:2502.03544. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, and 1 others. 2021.Training verifiers to solve math word problems.arXiv preprint arXiv:2110.14168. Weichen Dai, Rafael Medeiros Cabral, Ziyi Shou, Yan Cao, litingzhe, Hongfei Ai, Jing Yang, Pengcheng Tang, SHEN XIN, and Dongcai Lu. 2025. From sym- bolic perception to logical deduction: A framework for guiding language models in geometric reasoning. DeepSeek-AI, Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhi- hong Shao, Zhuoshu Li, Ziyi Gao, and 181 others. 2025. Deepseek-r1: Incentivizing reasoning capa- bility in llms via reinforcement learning. Preprint, arXiv:2501.12948. Linger Deng, Yuliang Liu, Bohan Li, Dongliang Luo, Liang Wu, Chengquan Zhang, Pengyuan Lyu, Ziyang Zhang, Gang Zhang, Errui Ding, and 1 others. 2024a. R-cot: Reverse chain-of-thought problem generation for geometric reasoning in large multimodal models. arXiv preprint arXiv:2410.17885. Linger Deng, Linghao Zhu, Yuliang Liu, Yu Wang, Qunyi Xie, Jingjing Wu, Gang Zhang, Yingying Zhu, and Xiang Bai. 2024b. Theorem-validated reverse chain-of-thought problem generation for geometric reasoning. arXiv preprint arXiv:2410.17885. Yuan Feng, Yue Yang, Xiaohan He, Jiatong Zhao, Jian- long Chen, Zijun Chen, Daocheng Fu, Qi Liu, Renqiu Xia, Bo Zhang, and Junchi Yan. 2025. Geobench: Re- thinking multimodal geometric problem-solving via hierarchical evaluation. Preprint, arXiv:2512.24119. Daocheng Fu, Zijun Chen, Renqiu Xia, Qi Liu, Yuan Feng, Hongbin Zhou, Renrui Zhang, Shiyang Feng, Peng Gao, Junchi Yan, and 1 others. 2025a. Trust- geogen: Scalable and formal-verified data engine for trustworthy multi-modal geometric problem solving. arXiv preprint arXiv:2504.15780. Yumeng Fu, Jiayin Zhu, Lingling Zhang, Bo Zhao, Shaoxuan Ma, Yushun Zhang, Yanrui Wu, and Wen- jun Wu. 2025b. Geolaux: A benchmark for eval- uating mllms’ geometry performance on long-step problems requiring auxiliary lines. arXiv preprint arXiv:2508.06226. 9 Jiahui Gao, Renjie Pi, Jipeng Zhang, Jiacheng Ye, Wan- jun Zhong, Yufei Wang, Lanqing Hong, Jianhua Han, Hang Xu, Zhenguo Li, and 1 others. 2023. G-llava: Solving geometric problem with multi-modal large language model. arXiv preprint arXiv:2312.11370. Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Caroline Falk- man Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, and 1 others. 2024. Fron- tiermath: A benchmark for evaluating advanced mathematical reasoning in ai.arXiv preprint arXiv:2411.04872. Google. 2025. Gemini 3 developer guide. Technical report, Google. Yihan Hao, Mingliang Zhang, Fei Yin, and Lin-Lin Huang. 2022. Pgdp5k: A diagram parsing dataset for plane geometry problems. In 2022 26th inter- national conference on pattern recognition (ICPR), pages 1763–1769. IEEE. Kaivalya Hariharan, Uzay Girit, Atticus Wang, and Ja- cob Andreas. 2025. Breakpoint: Scalable evalua- tion of system-level reasoning in llm code agents. Preprint, arXiv:2506.00172. Chaoqun He, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Leng Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, and 1 oth- ers. 2024. Olympiadbench: A challenging bench- mark for promoting agi with olympiad-level bilin- gual multimodal scientific problems. arXiv preprint arXiv:2402.14008. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Ja- cob Steinhardt. 2021. Measuring mathematical prob- lem solving with the math dataset. arXiv preprint arXiv:2103.03874. Zihan Huang, Tao Wu, Wang Lin, Shengyu Zhang, Jingyuan Chen, and Fei Wu. 2025. Autogeo: Au- tomating geometric image dataset creation for en- hanced geometry understanding. IEEE Transactions on Multimedia. Aaron Hurst, Adam Lerer, Adam P Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Ostrow, Akila Welihinda, Alan Hayes, Alec Radford, and 1 others. 2024. Gpt-4o system card. arXiv preprint arXiv:2410.21276. Mehran Kazemi, Hamidreza Alvari, Ankit Anand, Jialin Wu, Xi Chen, and Radu Soricut. 2023. Geomverse: A systematic evaluation of large models for geomet- ric reasoning. arXiv preprint arXiv:2312.12241. Fangyu Lei, Qian Liu, Yiming Huang, Shizhu He, Jun Zhao, and Kang Liu. 2024. S3Eval: A synthetic, scal- able, systematic evaluation suite for large language model. In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Tech- nologies (Volume 1: Long Papers), pages 1259–1286, Mexico City, Mexico. Association for Computational Linguistics. Zhuowan Li, Bhavan Jasani, Peng Tang, and Shabnam Ghadar. 2024. Synthesize step-by-step: Tools tem- plates and llms as data generators for reasoning-based chart vqa. In Proceedings of the IEEE/CVF Confer- ence on Computer Vision and Pattern Recognition, pages 13613–13623. Haotian Liu, Chunyuan Li, Yuheng Li, and Yong Jae Lee. 2024. Improved baselines with visual instruc- tion tuning. In Proceedings of the IEEE/CVF Con- ference on Computer Vision and Pattern Recognition, pages 26296–26306. Pan Lu, Hritik Bansal, Tony Xia, Jiacheng Liu, Chun- yuan Li, Hannaneh Hajishirzi, Hao Cheng, Kai- Wei Chang, Michel Galley, and Jianfeng Gao. 2023. Mathvista: Evaluating mathematical reasoning of foundation models in visual contexts. arXiv preprint arXiv:2310.02255. Pan Lu, Ran Gong, Shibiao Jiang, Liang Qiu, Siyuan Huang, Xiaodan Liang, and Song-Chun Zhu. 2021. Inter-gps: Interpretable geometry problem solving with formal language and symbolic reasoning. arXiv preprint arXiv:2105.04165. Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jian- guang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, and Dongmei Zhang. 2023. Wiz- ardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct. arXiv preprint arXiv:2308.09583. Shixian Luo, Zezhou Zhu, Yu Yuan, Yuncheng Yang, Lianlei Shan, and Yong Wu. 2025. Geogrambench: Benchmarking the geometric program reasoning in modern llms. Preprint, arXiv:2505.17653. OpenAI. 2025a. Openai o3 and o4-mini system card. Technical report, OpenAI. OpenAI. 2025b. Openai o3-mini system card. Techni- cal report, OpenAI. Yicheng Pan, Zhenrong Zhang, Pengfei Hu, Jiefeng Ma, Jun Du, Jianshu Zhang, Quan Liu, Jianqing Gao, and Feng Ma. 2025. Enhancing the geometric problem- solving ability of multimodal llms via symbolic- neural integration. Preprint, arXiv:2504.12773. AAB Prasetyanto, TB Adji, and I Hidayah. 2020. Au- tomatic question generator system conceptual model for mathematic and geometry parallel question repli- cation. In Journal of Physics: Conference Series, volume 1577, page 012023. IOP Publishing. Minjoon Seo, Hannaneh Hajishirzi, Ali Farhadi, Oren Etzioni, and Clint Malcolm. 2015. Solving geometry problems: Combining text and diagram interpretation. In Proceedings of the 2015 conference on empirical methods in natural language processing, pages 1466– 1476. 10 Kai Sun, Yushi Bai, Ji Qi, Lei Hou, and Juanzi Li. 2024. Mm-math: Advancing multimodal math evaluation with process evaluation and fine-grained classifica- tion. arXiv preprint arXiv:2404.05091. Gemini Team, Petko Georgiev, Ving Ian Lei, Ryan Burnell, Libin Bai, Anmol Gulati, Garrett Tanzer, Damien Vincent, Zhufeng Pan, Shibo Wang, and 1 others. 2024. Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context. arXiv preprint arXiv:2403.05530. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. 2024.Solving olympiad ge- ometry without human demonstrations.Nature, 625(7995):476–482. Xiaofeng Wang, Yiming Wang, Wenhong Zhu, and Rui Wang. 2025. Do large language models truly understand geometric structures?arXiv preprint arXiv:2501.13773. Colin White, Samuel Dooley, Manley Roberts, Arka Pal, Ben Feuer, Siddhartha Jain, Ravid Shwartz-Ziv, Neel Jain, Khalid Saifullah, Sreemanti Dey, Shubh- Agrawal, Sandeep Singh Sandha, Siddartha Naidu, Chinmay Hegde, Yann LeCun, Tom Goldstein, Willie Neiswanger, and Micah Goldblum. 2025. Livebench: A challenging, contamination-limited llm benchmark. Preprint, arXiv:2406.19314. Shangyu Xing, Changhao Xiang, Yuteng Han, Yifan Yue, Zhen Wu, Xinyu Liu, Zhangtai Wu, Fei Zhao, and Xinyu Dai. 2024. Gepbench: Evaluating fun- damental geometric perception for multimodal large language models. arXiv preprint arXiv:2412.21036. Cheng Xu, Nan Yan, Shuhao Guan, Changhong Jin, Yuke Mei, Yibing Guo, and Tahar Kechadi. 2025. DCR: Quantifying data contamination in LLMs eval- uation. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, pages 23002–23020, Suzhou, China. Association for Computational Linguistics. An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Day- iheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge, Haoran Wei, Huan Lin, Jialong Tang, and 41 others. 2025. Qwen3 technical report. Preprint, arXiv:2505.09388. An Yang, Baosong Yang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Zhou, Chengpeng Li, Chengyuan Li, Dayiheng Liu, Fei Huang, Guanting Dong, Hao- ran Wei, Huan Lin, Jialong Tang, Jialin Wang, Jian Yang, Jianhong Tu, Jianwei Zhang, Jianxin Ma, and 43 others. 2024. Qwen2 technical report. Preprint, arXiv:2407.10671. Jian Zhang, Zhangqi Wang, Haiping Zhu, Kangda Cheng, Kai He, Bo Li, Qika Lin, Jun Liu, and Erik Cambria. 2025a. Mars: Multi-agent adaptive rea- soning with socratic guidance for automated prompt optimization. Preprint, arXiv:2503.16874. Jian Zhang, Zhiyuan Wang, Zhangqi Wang, Fangzhi Xu, Qika Lin, Lingling Zhang, Rui Mao, Erik Cambria, and Jun Liu. 2025b. Maps: Multi-agent personal- ity shaping for collaborative reasoning. Preprint, arXiv:2503.16905. Jian Zhang, Bifan Wei, Shihao Qi, haiping Zhu, Jun Liu, and Qika Lin. 2025c. Gkg-llm: A unified frame- work for generalized knowledge graph construction. Preprint, arXiv:2503.11227. Jiaxin Zhang, Zhongzhi Li, Mingliang Zhang, Fei Yin, Chenglin Liu, and Yashar Moshfeghi. 2024a. Geoe- val: Benchmark for evaluating llms and multi-modal models on geometry problem-solving.Preprint, arXiv:2402.10104. Ming-Liang Zhang, Fei Yin, and Cheng-Lin Liu. 2023a. A multi-modal neural geometric solver with tex- tual clauses parsed from diagram. arXiv preprint arXiv:2302.11097. Renrui Zhang, Dongzhi Jiang, Yichi Zhang, Haokun Lin, Ziyu Guo, Pengshuo Qiu, Aojun Zhou, Pan Lu, Kai-Wei Chang, Yu Qiao, and 1 others. 2024b. Math- verse: Does your multi-modal llm truly see the dia- grams in visual math problems? In European Confer- ence on Computer Vision, pages 169–186. Springer. Renrui Zhang, Xinyu Wei, Dongzhi Jiang, Yichi Zhang, Ziyu Guo, Chengzhuo Tong, Jiaming Liu, Aojun Zhou, Bin Wei, Shanghang Zhang, and 1 others. 2024c. Mavis: Mathematical visual instruction tun- ing. arXiv e-prints, pages arXiv–2407. Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang, Xiaoxiao Jin, Yanjun Guo, Chenyang Mao, Yang Li, Zhe Zhu, and 1 others. 2023b.For- malgeo: An extensible formalized framework for olympiad geometric problem solving. arXiv preprint arXiv:2310.18021. Minfeng Zhu, Zi Wang, Sizhe Ji, Zhengtong Du, Jun- ming Ke, Xiao Deng, Zanlang Yin, Xiuqi Huang, Heyu Wang, and Wei Chen. 2025. Genesisgeo: Tech- nical report. arXiv preprint arXiv:2509.21896. A Examples of Clauses, Constructions, and Premises Clausestriangle: This clause created three points to construct a triangle. midpoint a b: This clause uniquely determines a point based on the positions of points A and B. angle_bisector a b c : This clause describes the set of points that lie in the angle bisector of∠ABC. Constructionsa b c = triangle: This construc- tion created three points to construct a triangle. x = angle_bisector a b c, on_line a c: This construction uniquely determines the intersection point between the angle bisector of∠ABCand the line AC. 11 x = midpoint a b, midpoint a c(invalid): This is an invalid construction, as the midpoints of AB and AC generally do not intersect at a single, well-defined point. Premise abc = ieq_triangle(a,b,c); d = reflect(d,c,a,b); e = on_line(e,d,a), eqdistance(e,d,a,b); f = on_dia(f,b,e), on_circle(f,a,c). This premise captures six point elements and their geometric relationships, which enables the con- struction of a diagram that matches the description (Figure 5) A B C D E F Figure 5: the diagram corresponding to the premise above B Forward Chaining Algorithm This section details our forward-chaining conclu- sion search strategy: starting from the premise, we iteratively match theorems and derive algebraic facts under a maximum depthN, accumulating all newly derived conclusions until no further updates occur. C GeoChallenge Details The GeoChallenge-90K dataset comprises 90,279 automatically generated geometric proof problems. As detailed in Table 6 of the Appendix C, all problems presented in our dataset are offered with images and solutions of the problem, with both English and Chinese version of the problem provided. the dataset exhibits a stratified diffi- culty distribution with 27,083 easy-level (30.0%), 45,140 medium-level (50.0%), and 18,056 hard- level (20.0%) problems. This partitioning follows a 3:5:2 ratio based on a priori complexity scores derived from the weighted function shown in main text. Algorithm 1 Conclusion search via forward chain- ing Input: Premise Parameter: max_level N Output: All derived conclusions 1: C ← Read(Premise) 2: level← 0 3: while level < N do 4: T ← match_theorems(R) 5: T ← T∪ derive_algebra(R) 6:if Not_empty(T ) then 7: C ← C∪ T 8:else 9:break 10:end if 11: end while 12: return C D Predefined Clause Templates This appendix summarizes the predefined clause templates used in our automatic geometry-problem generation pipeline; the complete list is provided in Table 7. E Predefined Rules This appendix lists the predefined inference rules employed by the symbolic reasoning engine for forward deduction; the full rule set is presented in Table 8. FCross-lingual robustness under Chinese prompts We evaluate general-purpose models under Chi- nese prompts and compare them with their English- prompt counterparts to assess cross-lingual robust- ness, reporting strict exact-match accuracy (EMA) alongside option-level metrics (F1, HA) and the average number of selected options (Avg #Sel). Across models, EMA is consistently more sensitive to language shifts than option-level metrics, indi- cating that changes in linguistic formulation can disrupt exact answer consistency even when partial option identification remains similar. As shown in table 5, in the multimodal setting (text + images), GPT-4o degrades substantially from English to Chinese (EMA -5.62, F1 -13.43, HA -12.78), and Claude 3.5 Sonnet also drops con- sistently (EMA -4.19, F1 -4.24, HA -2.37), whereas Gemini 1.5 Pro remains largely stable (EMA - 0.22) with slightly improved F1/HA, suggesting 12 ModelEMA↑EME↑EMM↑EMH↑P↑R↑F1↑HA↑Avg #Sel Both text and images provided GPT-4o11.8919.649.137.0740.2754.6646.3845.842.25 Claude 3.5 Sonnet17.6230.1813.598.7052.3764.8657.9560.852.05 Gemini 1.5 Pro24.2338.5521.1610.3362.8582.9871.5271.312.12 llava-1.5-7B12.1125.098.242.1737.0023.7628.9450.611.05 Qwen2-VL-7B24.0158.9112.470.057.1648.9752.7563.131.41 Text-only provided GPT-4o9.5819.277.570.043.4568.8153.2646.722.71 Claude 3.5 Sonnet12.7823.6411.360.048.3969.3757.0257.742.34 Gemini 1.5 Pro23.3554.9113.590.063.4274.0868.3468.721.86 WizardMath-7B7.7110.187.135.4338.3448.5542.8547.582.07 Table 5: General-purpose models’ performance on GeoChallenge, where the same problems are presented with Chinese prompts rather than English. Statistics Total Problems90,279 Coverage (Img / Sol / EN / ZH) 100% / 100% / 100% / 100% Difficulty90,279 * Easy27,083 (30.0%) * Medium45,140 (50.0%) * Hard18,056 (20.0%) Geometry Relations258,963 * Equality104,178 * Parallel15,012 * Vertical47,092 * Collinear12,689 * Circle-related74,579 * Others5,413 Table 6: Detailed statistics of the GeoChallenge dataset. EN and ZH denote English and Chinese statements, respectively. stronger cross-lingual robustness. We also observe a recurring over-selection pattern under Chinese prompts: Qwen2-VL-7B shows a smaller EMA decrease (26.65 to 24.01) but selects more options (+0.22 Avg #Sel), and under text-only evaluation GPT-4o exhibits the same mechanism more clearly (EMA -4.41 vs. F1 +4.18 with Avg #Sel +0.57). Taken together, language-induced over-selection can preserve or even improve F1/HA by increas- ing coverage of correct options, while reducing EMA because any extra or missing option breaks the exact match. G LLM Prompt Templates All model evaluations were conducted using care- fully designed and standardized system prompts to ensure full reproducibility across different exper- imental settings. The prompt templates remained consistent throughout all evaluation scenarios, with minor adaptations made only for modality-specific requirements. For text-only model evaluations, we maintained strict prompt consistency by using identical textual templates across all comparable experiments. No- tably, despite the visual nature of some tasks, we intentionally omitted any special instructions re- garding missing images in text-only settings. This design choice was based on two key considera- tions: (1) our problem descriptions maintain high text-image consistency, allowing models to theo- retically reconstruct the visual information from textual descriptions alone (though this capability may be challenging for current models), and (2) we observed that models typically wouldn’t refuse to answer due to absent images when provided with sufficiently detailed textual descriptions. For text+image evaluations, we employed the structured prompt templates illustrated in Figure 6 and 7 for English and Chinese versions respec- tively. These multimodal prompts systematically incorporated both the textual instructions and vi- sual content, with clear markers distinguishing be- tween image inputs and textual components. The visual examples accompanying each prompt were carefully selected to be representative of the task requirements while avoiding potential biases in im- age content or composition. H More Problems in GeoChallenge Dataset Figures 8, 9, and 10 illustrate representative ex- amples of easy, medium, and hard problems, re- spectively. A clear progression in complexity is observable across these difficulty levels: the tex- tual descriptions grow significantly longer, incor- porating more intricate logical constraints and nu- 13 Multimodal model input prompts You are an expert in the field of mathematics, specializing in logical reasoning and problem-solving. Your task is to carefully analyze the following question and rigorously verify the correctness of each option through deductive reasoning. First, provide the final answer composed of the letter(s) of the correct option(s), followed by a step-by-step reasoning process for each option, including the justification for its inclusion or exclusion. Question: question_en Options: A. a_en B. b_en C. c_en D. d_en Please respond in the following format: [Answer][Final option letter(s)] [Option A] (analysis) [Option B] (analysis) [Option C] (analysis) [Option D] (analysis) Figure 6: English version of prompt to LLMs Multimodal model input prompts 你是一个数学领域专家，专注于逻辑推理和问题解决。现在需要仔细分析以下问题，通过严谨的推导验证每个选项 的正确性。请首先给出由你认为正确选项字母组成的最终答案，随后逐个选项地输出选项的推理过程，或被排除的 具体原因。 问题：question_zh 选项： A. a_zh B. b_zh C. c_zh D. d_zh 请按照以下格式回答： [答案][最终选项字母] [选项A] [选项B] [选项C] [选项D] Figure 7: Chinese version of prompt to LLMs anced phrasing, while the accompanying images exhibit a marked increase in structural sophistica- tion, evidenced by the rising number of geometric points, connecting lines, and layered annotations. Notably, the easy-level problems typically involve straightforward deductions with minimal interme- diate reasoning steps, whereas medium and hard problems demand deeper theorem applications, of- ten requiring multi-hop inference chains and care- ful consideration of implicit spatial relationships. This escalation in cognitive demand aligns closely with human intuition—the harder problems not only present more visual clutter but also necessi- tate greater mental effort in parsing, planning, and executing solutions. The deliberate stratification of difficulty ensures that the benchmark captures a wide spectrum of reasoning capabilities, from basic pattern recognition to advanced geometric theorem synthesis, mirroring the gradual skill development observed in human problem-solving. Furthermore, the consistency between objective complexity met- rics (e.g., token count, graph density) and subjec- tive human assessment underscores the validity of our difficulty calibration methodology. 14 "Question_en": "Given a right trapezoid ABCD with AB∥CD, and ∠A as the right angle. G is a free point. Through point B, two tangents BI and BJ are drawn to the circle ⊙A with radius AG, with the point of tangency at I and J, respectively.", "A_en": "AD is not perpendicular to CD", "B_en": "AI:BI = AJ:BJ", "C_en": "AD is parallel to IJ", "D_en": "A is the circumcenter of △GIJ", "Answer": "BCD", "Prior_Difficulty": 59.0, "Posterior_Difficulty": 0.75, "SimplifiedFormalText": "a b c d = r_trapezoid a b c d; g = free g; i j = tangent i j b a g", "UsedPoints": ["a","b","c","d","g","i","j"], "premises": ["AB ∥ CD [00]","AB ⟂ AD [01]","AI = AG [02]","BI ⟂ AI [03]","AJ = AG [04]","BJ ⟂ AJ [05]"], "ProofSteps_A": "001. AB ⟂ AD [00] & AB ∥ CD [01] ⇒ CD ⟂ AD ", "ProofSteps_B": "001. AI = AG [00] & AJ = AG [02] ⇒ A is the circumcenter of \ JGI [04] 002. A is the circumcenter of \ JGI [04] & BI ⟂ AI [01] ⇒ ∠JIB = ∠JGI [05] 003. A is the circumcenter of \ JGI [04] & BJ ⟂ AJ [03] ⇒ ∠BJI = ∠JGI [06] 004. ∠JIB = ∠JGI [05] & ∠BJI = ∠JGI [06] ⇒ ∠BJI = ∠JIB [07] 005. ∠BJI = ∠JIB [07] ⇒ IB = JB [08] 006. AI = AG [00] & AJ = AG [02] & IB = JB [08] ⇒ IA:IB = JA:JB ", "ProofSteps_C": "001. AJ = AG [04] & AI = AG [02] ⇒ A is the circumcenter of \ JGI [06] 002. A is the circumcenter of \ JGI [06] & BI ⟂ AI [03] ⇒ ∠JIB = ∠JGI [07] 003. A is the circumcenter of \ JGI [06] & BJ ⟂ AJ [05] ⇒ ∠BJI = ∠JGI [08] 004. BI ⟂ AI [03] & BJ ⟂ AJ [05] ⇒ ∠BJA = ∠BIA [09] 005. ∠BJA = ∠BIA [09] ⇒ A,J,B,I are concyclic [10] 006. A,J,B,I are concyclic [10] ⇒ ∠BJI = ∠BAI [11] 007. AB ⟂ AD [01] & BI ⟂ AI [03] ⇒ ∠BAI = ∠(AD-BI) [12] 008. ∠JIB = ∠JGI [07] & ∠BJI = ∠JGI [08] & ∠BJI = ∠BAI [11] & AB ∥ CD [00] & ∠BAI = ∠(AD-BI) [12] ⇒ ∠(AD-BI) = ∠JIB [13] 009. ∠(AD-BI) = ∠JIB [13] ⇒ AD ∥ JI ", "ProofSteps_D": "001. AJ = AG [01] & AI = AG [00] ⇒ A is the circumcenter of \ JGI " Figure 8: Example of easy level problem in GeoChallenge "Question_en": "Given square ABCD. Construct the nine-point circle ⊙H of △CBA, intersecting BA, CA, CB at E, F, G, respectively. ∠GFI=45°, IC=GA. Line FI intersects the perpendicular bisector of EF at K.", "A_en": "∠(AH-BK) ≠ ∠GDE", "B_en": "AE:AK = DG:DK", "C_en": "BK is perpendicular to CH", "D_en": "EH is not perpendicular to EK", "Answer": "BC", "Prior_Difficulty": 176.0, "Posterior_Difficulty": 0, "SimplifiedFormalText": "a b c d = isquare a b c d; e f g h = ninepoints e f g h c b a; i = s_angle g f i 45, eqdistance i c g a; k = on_line k f i, on_bline k e f", "UsedPoints": ["a","b","c","d","e","f","g","h","i","k"], "premises": ["AB = BC [00]","AB ⟂ BC [01]","E,A,B are collinear [02]","EB = EA [03]","C,F,A are collinear [04]","FA = FC [05]","C,G,B are collinear [06]","GC = GB [07]","HE = HF [08]","HF = HG [09]","∠IFG = 1_PI/4 [10]","KE = KF [11]","F,I,K are collinear [12]","∠KEF = ∠EFK [13]"], "ProofSteps_A": "001. AB ⟂ BC [00] & BC ∥ AD [02] & AB ∥ CD [03] ⇒ ∠ADC = ∠ABC [19] 002. AB ⟂ BC [00] & BC ∥ AD [02] & AB ∥ CD [03] ⇒ AD ⟂ DC [20] 003. ∠ADC = ∠ABC [19] ⇒ C,D,A,B are concyclic [21] 004. AB ∥ CD [03] & BC ∥ AD [02] ⇒ ∠CDA = ∠DCB [22] 005. AB ∥ CD [03] & BC ∥ AD [02] ⇒ ∠ADC = ∠CBA [23] 006. C,D,A,B are concyclic [21] & ∠CDA = ∠DCB [22] ⇒ CA = DB [24] ...... 112. ∠BKG = ∠EDG [129] & ∠EHA = ∠HGK [127] & H,G,E are collinear [103] ⇒ ∠(BK-AH) = ∠EDG ", "ProofSteps_B": "......", "ProofSteps_C": "......", "ProofSteps_D": "......" Figure 9: Example of medium level problem in GeoChallenge 15 namemeaning X = angle_bisector(A,B,C)Construct point X on the angle bisector of∠ ABC X = angle_mirror(A,B,C)Construct point X such that BC is the bisector of∠ ABX X,Y,Z,I = centroid(A,B,C)Construct point I as the centroid of△ABC with midpoints X, Y, Z X = circle(A,B,C)Construct point X as the circumcenter of△ABC A,B,C,D = eq_quadrangle()Construct quadrilateral ABCD with AD = BC A,B,C,D = eq_trapezoid()Construct trapezoid ABCD with AD = BC X = eq_triangle(B,C)Construct point X such that△XBC is an equilateral triangle X = eqangle2(A,B,C)Construct point X such that∠ BAX =∠ XCB X = eqangle3(A,B,D,E,F)Construct point X such that∠ AXB =∠ EDF A,B,C,D = eqdia_quadrangle()Construct quadrilateral ABCD with AC = BD X = eqdistance(A,B,C)Construct point X such that XA = BC X = excenter(A,B,C)Construct point X as the excenter of△ABC X = foot(A,B,C)Construct point X as the foot of A on BC A,B,C = ieq_triangle()Construct equilateral triangle△ABC X = incenter(A,B,C)Construct point X as the incenter of△ABC X = intersect(f,g)Construct point X as function f()∩ g() X = intersection_lc(A,O,B)Construct point X as circle O∩ line AB X = intersection_l(A,B,C,D)Construct point X as line AB∩ line CD X = intersection_lp(A,B,C,M,N)Construct point X as line AB∩ line through C parallel to line MN X = intersection_lt(A,B,C,D,E)Construct point X as line AB∩ line through C perpendicular to line DE X = intersection_p(A,B,C,D,E,F)Construct point X such that line XA∥ line BC and line XD∥ line EF X = intersection_t(A,B,C,D,E,F)Construct point X such that line XA⊥ line BC and line XD⊥ line EF A,B,C = iso_triangle()Construct A, B, C such that AB = AC A,B,C,D = isquare()Construct square ABCD X = lc_tangent(A,O)Construct point X such that OA is perpendicular to AX X = midpoint(A,B)Construct point X as the midpoint of AB X = mirror(A,B)Construct point X such that B is the midpoint of AX X,Y,Z,I = ninepoints(A,B,C)Construct midpoints X, Y, Z and point I as the circumcenter of△XYZ X = nsquare(A,B)Construct point X such that XB is the right isosceles triangle X = on_aline(A,B,C,D,E)Construct point X such that∠ XAB =∠ CDE X = on_bline(X,A,B)Construct point X on the perpendicular bisector of AB X = on_ circle(O,A)Construct point X such that OA = OX X = on_circum(A,B,C)Construct point X on the circumcircle of A, B, C X = on_dia(A,B)Construct point X such that AX is perpendicular to BX X = on_line(A,B)Construct point X on line AB X = on_pline(A,B,C)Construct point X such that XA is parallel to BC X = on_tline(A,B,C)Construct point X such that XA is perpendicular to BC X = orthocenter(A,B,C)Construct point X as the orthocenter of ABC X = parallelogram(A,B,C)Construct point X such that ABCX is a parallelogram A,B,C,D = r_trapezoid()Construct right trapezoid ABCD A,B,C = r_triangle()Construct right triangle ABC A,B,C,D = rectangle()Construct rectangle ABCD X = reflect(A,B,C)Construct point X as the reflection of A about BC A,B,C = risos()Construct point X as the isosceles triangle ABC X = s_angle(A,B,α)Construct point X such that∠ ABX = α A,B = segment()Construct segment AB X = shift(B,C,D)Construct point X such that XB=CD and XC=BD X Y = square(A,B)Construct point X, Y such that XYAB is a square X,Y = tangent(A,O,B)Construct point X,Y as the tangent touch points from A to circle (O,B) A,B,C,D = trapezoid()Construct trapezoid ABCD A,B,C = triangle()Construct triangle ABC Table 7: Predefined Clause Templates for Generating Geometric Problems (Adapted and modified from Work AlphaGeometry) 16 premise(s)conclusion perp A B C D, perp C D E F, ncoll A B Epara A B E F cong O A O B, cong O B O C, cong O C O Dcyclic A B C D eqangle A B P Q C D P Qpara A B C D cyclic A B P Qeqangle P A P B Q A Q B eqangle6 P A P B Q A Q B, ncoll P Q A Bcyclic A B P Q cyclic A B C P Q R, eqangle C A C B R P R Qcong A B P Q midp E A B, midp F A Cpara E F B C midp E A B, midp F A C, midp G B Ccong E F G B midp E A B, midp F A C, midp G B Ccong E F G C para A B C D, coll O A C, coll O B Deqratio3 A B C D O O perp A B C D, perp E F G H, npara A B E Feqangle A B E F C D G H eqangle A B C D M N P Q, eqangle C D E F P Q R Ueqangle A B E F M N R U eqratio A B C D M N P Q, eqratio C D E F P Q R Ueqratio A B E F M N R U eqratio6 D B D C A B A C, Coll D B C, ncoll A B Ceqangle6 A B A D A D A C eqangle6 A B A D A D A C, Coll D B C, ncoll A B Ceqratio6 D B D C A B A C cong O A O B, ncoll O A Beqangle O A A B A B O B eqangle6 A O A B B A B O, ncoll O A Bcong O A O B circle O A B C, perp O A A Xeqangle A X A B C A C B circle O A B C, eqangle A X A B C A C Bperp O A A X circle O A B C, midp M B Ceqangle A B A C O B O M circle O A B C, coll M B C, eqangle A B A C O B O M midp M B C perp A B B C, midp M A Ccong A M B M circle O A B C, coll O A Cperp A B B C cyclic A B C D, para A B C Deqangle A D C D C D C B midp M A B, perp O M A Bcong O A O B cong A P B P, cong A Q B Qperp A B P Q cong A P B P, cong A Q B Q, cyclic A B P Qperp P A A Q midp M A B, midp M C Dpara A C B D midp M A B, para A C B D, para A D B Cmidp M C D eqratio O A A C O B B D, coll O A C, coll O B D, ncoll A B C, sameside A O C B O D para A B C D para A B A Ccoll A B C midp M A B, midp N C Deqratio M A A B N C C D eqangle A B P Q C D U V, perp P Q U Vperp A B C D eqratio A B P Q C D U V, cong P Q U Vcong A B C D Table 8: Rules Used by the Symbolic Reasoning Engine for Deriving New Conclusions 17 "Question_en": "Given square ABCD. Construct the nine-point circle ⊙H of △CDB, intersecting DB, CB, CD at E, F, G, respectively. Through point F, draw a line parallel to BH, and this line intersects circle determined by points F, D, and C at J. M is the midpoint of DJ. N is the midpoint of AJ.", "A_en": "CN ≠ JN", "B_en": "∠AMF ≠ ∠GND", "C_en": "AM:HN ≠ HM:GM", "D_en": "AM is parallel to GN", "Answer": "D", "Prior_Difficulty": 413.5, "Posterior_Difficulty": 0, "SimplifiedFormalText": "a b c d = isquare a b c d; e f g h = ninepoints e f g h c d b; j = on_circum j f d c, on_pline j f b h; m = midpoint m d j; n = midpoint n a j", "UsedPoints": ["a","b","c","d","e","f","g","h","j","m","n"], "premises": ["AB = BC [00]","AB ⟂ BC [01]","AB ∥ CD [02]","AD ∥ BC [03]","E,D,B are collinear [04]","ED = EB [05]","F,B,C are collinear [06]","FB = FC [07]","G,D,C are collinear [08]","GC = GD [09]","HE = HF [10]","HF = HG [11]","J,F,D,C are concyclic [12]","JF ∥ BH [13]","J,M,D are collinear [14]","MD = MJ [15]","A,J,N are collinear [16]","NJ = NA [17]"], "ProofSteps_A": "001. FC = FB [07] & OD = OA [21] ⇒ FC:FB = OD:OA [22] 002. AB ∥ CD [02] & F,B,C are collinear [06] & A,O,D are collinear [20] & FC:FB = OD:OA [22] ⇒ FO ∥ CD [23] 003. F,B,C are collinear [06] & A,O,D are collinear [20] & AB ⟂ BC [00] & AB ∥ CD [02] & FO ∥ CD [23] & BC ∥ AD [03] ⇒ ∠FCD = ∠FOD [24] ......247. ∠(JO-ED) = ∠(JC-OG) [54] & E,D,B are collinear [04] & GO ⟂ HG [67] & BD ⟂ AC [50] & GO ∥ AC [52] & OG ∥ JO [143] & BE ⟂ GO [80] & H,F,G are collinear [92] & BD ∥ FG [63] & ∠(CO-EI) = ∠(AC-GI) [118] & CO ∥ EI [116] & ∠(CO-EI) = ∠GOI [156] & ∠BDG = ∠NEO [263] & G,D,C are collinear [08] & E,F,O are collinear [36] & EF ∥ CD [34] & ∠OGM = ∠AEN [266] & A,E,C are collinear [61] & GM ∥ CJ [267] ⇒ JC ⟂ CA [268] 248. JC ⟂ CA [268] & N is midpoint of AJ [37] ⇒ JN = CN ", "ProofSteps_B": "......", "ProofSteps_C": "......", "ProofSteps_D": "......" Figure 10: Example of hard level problem in GeoChallenge 18