PaperlayerView exact revision on arXiv

Source-linked AI summary

Proposing and solving olympiad geometry with guided tree search

Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu, Song-Chun Zhu

arXiv:2412.10673v1cs.AIcs.LG

TL;DR

Automated geometry systems face challenges in both proposing and solving olympiad problems, including selecting suitable problems from large generated pools. TongGeometry uses guided tree search with neural models to discover, present, and prove geometry problems; it achieves super-gold-medalist performance on IMO problems and surpasses the previous state of the art.

  • Problem

    Selecting suitable problems from billions of generated candidates remains challenging, and olympiad problem proposing lacks an automatic assessment scheme.

    Source: Evaluating generated problems for… · p. 4

  • Method

    TongGeometry is a neuro-symbolic geometry system that uses guided tree search, with policy and value models supporting auxiliary construction and estimating remaining solution steps.

    Source: Conclusion · p. 7

  • Results

    TongGeometry achieved super-gold-medalist performance for the first time on IMO problems and surpassed the previous state of the art.

    Source: Conclusion · p. 7

  • Takeaways & Limitations

    TongGeometry is framed as a geometry coach that discovers, presents, and proves IMO-level geometry problems.

    Source: Conclusion · p. 7

    Current models still fail on problems requiring sequential construction of multiple interrelated new points.

    Source: Limitation · p. 20

Abstract

from arXiv · show

Mathematics olympiads are prestigious competitions, with problem proposing and solving highly honored. Building artificial intelligence that proposes and solves olympiads presents an unresolved challenge in automated theorem discovery and proving, especially in geometry for its combination of numerical and spatial elements. We introduce TongGeometry, a Euclidean geometry system supporting tree-search-based guided problem proposing and solving. The efficient geometry system establishes the most extensive repository of geometry theorems to date: within the same computational budget as the existing state-of-the-art, TongGeometry discovers 6.7 billion geometry theorems requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. Among them, 10 theorems were proposed to regional mathematical olympiads with 3 of TongGeometry's proposals selected in real competitions, earning spots in a national team qualifying exam or a top civil olympiad in China and the US. Guided by fine-tuned large language models, TongGeometry solved all International Mathematical Olympiad geometry in IMO-AG-30, outperforming gold medalists for the first time. It also surpasses the existing state-of-the-art across a broader spectrum of olympiad-level problems. The full capabilities of the system can be utilized on a consumer-grade machine, making the model more accessible and fostering widespread democratization of its use. By analogy, unlike existing systems that merely solve problems like students, TongGeometry acts like a geometry coach, discovering, presenting, and proving theorems.

Assessing TongGeometry

TongGeometry is assessed through generated-problem evaluation, benchmark solving, and expert review. Its search yields billions of auxiliary-construction problems, while its solver achieves strong IMO results and its proposals reach competition stages.

Evaluating generated problems for olympiads

  • After filtering, TongGeometry produced 6,688,310,403 problems requiring auxiliary constructions, including 4,096,680,574 symmetric problems.The search found an average of 0.7613 auxiliary-requiring configurations per unique path.Source: Evaluating generated problems for… · p. 4
  • Using statistics from 196 existing olympiad problems, the authors developed selection rubrics to address the lack of automatic assessment for proposed problems.Experts manually examined proposals before submission.Source: Evaluating generated problems for… · p. 4
  • Of 10 proposals submitted to two competitions, one was selected as the only geometry problem in the 2024 Beijing final and two reached the 2024 US Ersatz Math Olympiad shortlist.AlphaGeometry solved three of the 10 proposals.Source: Evaluating generated problems for… · p. 4

Search discovers known lemmas and base configurations

  • The search rediscovered a known rotationally symmetric lemma and used cached foundational configurations as scaffolds for more complex scenarios.The example configuration features the Mixtilinear Incircle and Incenter/Excenter Lemma.Source: Search discovers known lemmas and base… · p. 5

Performance on benchmarks

  • All 30 IMO-AG-30 problems were proved, with TongGeometry surpassing IMO gold medalists on a consumer-grade machine.The reported setup used 32 CPU cores and one RTX 4090 GPU, with a maximum solve time of 38 minutes; AlphaGeometry used 246 CPU cores and four V100 GPUs to get under 90 minutes.Source: Performance on benchmarks · p. 6
  • 81.3% of MO-TG-225 problems were solved by TongGeometry versus 45.3% by AlphaGeometry, while 55.2% of TongGeometry’s solves came from DD.The passage attributes the system’s auxiliary-construction capability to its neural models.Source: Performance on benchmarks · p. 6
  • The value model improved performance over a policy-only model by 7.1% on IMO-AG-30 and 3.4% on MO-TG-225 under constrained resources.The reported setting used 32 cores and one graphics card.Source: Performance on benchmarks · p. 6

Expert evaluation on TongGeometry results

  • Two TongGeometry solutions to IMO 2024 P4 were judged correct by an IMO gold medalist and used the same auxiliary point as the official solution.The problem had few documented solutions when TongGeometry was trained.Source: Expert evaluation on TongGeometry… · p. 7

Conclusion

TongGeometry combines guided tree search with neural models to discover, present, and prove geometry problems. Its proposals reached olympiad competitions, and its solving approach achieved super-gold-medalist performance on IMO problems.

Conclusion

  • TongGeometry is a neuro-symbolic system designed to discover, present, and prove IMO-level geometry problems through guided tree search.Its actor-critic-style inference uses a policy model to complete auxiliaries and a value model to estimate remaining steps.Source: Conclusion · p. 7
  • One proposed problem was selected for the 2024 National High School Mathematics League (Beijing), and two others were shortlisted by the 2024 US Ersatz Math Olympiad.The Beijing competition is described as a Team China qualifying competition.Source: Conclusion · p. 7
  • TongGeometry achieved super-gold-medalist performance for the first time on IMO problems and surpassed the previous state of the art.The conclusion frames the system as a geometry coach rather than a solver that only solves problems.Source: Conclusion · p. 7

Proposing and solving olympiad geometry with guided tree

The listed authors are Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu, and Song-Chun Zhu.

  • The paper lists Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu, and Song-Chun Zhu as authors.Source: search · p. 16

Supplementary Text

Automated geometry proving includes algebraic and search-based approaches, but existing methods have limitations in interpretability, efficiency, auxiliary construction, and olympiad-level performance. TongGeometry is presented as a system that both proposes problems and autonomously proves theorems.

Automated geometry theorem proposing and proving

  • Automated geometry theorem proving spans algebraic methods and search-based techniques; Wu’s method (22,23) is prominent among the algebraic methods.Source: Automated geometry theorem proposing… · p. 17
  • Wu’s method is algebraic and mechanical, with limited diagram-level meaning and high space and time complexity.The passage characterizes these properties as concerns for wider adoption and practical use.Source: Automated geometry theorem proposing… · p. 17
  • Lean geometry libraries based on Euclid’s, Hilbert’s, or Tarski’s axioms have limited olympiad-level proving ability and are less intuitive than synthetic geometry.Source: Automated geometry theorem proposing… · p. 17
  • The passages say methods do not properly address auxiliary construction, while TongGeometry not only proposes problems but also autonomously proves theorems, presenting both an unresolved construction issue and an autonomous proving capability.Source: Automated geometry theorem proposing… · p. 17
  • AlphaGeometry (2) addresses auxiliary construction with data, but its data engine leaves olympiad geometry underexplored and performance below top-tier competition standards.Source: Automated geometry theorem proposing… · pp. 17–18

Learning-based methods for theorem proving

Learning-based theorem proving uses deep learning to guide proof search, while mathematical training data remains scarce. The section describes synthetic-data approaches and the annotation cost of process-based supervision.

Learning-based methods for theorem proving

  • The section distinguishes learning-guided search from improved data curation as two streams of learning-based theorem-proving research.Source: Learning-based methods for theorem… · p. 18
  • Learning-based theorem proving uses deep learning models to guide proof-assistant actions, with action log probability often serving as a heuristic.Best-first search and beam search have solved some simple olympiad algebra and number-theory problems and certain geometry problems.Source: Learning-based methods for theorem… · p. 18
  • Mathematical data is scarce: Metamath and Mathlib contain fewer than 60,000 human-written theorems combined, while the IMO produces six problems per year.The miniF2F benchmark includes only a few hundred validation and test problems.Source: Learning-based methods for theorem… · p. 18
  • Synthetic data from specially designed symbolic systems has supported strong model performance, and researchers have also explored LLM-generated data and proof autoformalization.Source: Learning-based methods for theorem… · pp. 18–19
  • Process-based supervision labels each proof step but requires more extensive annotation than outcome-based supervision.Source: Learning-based methods for theorem… · p. 19

Explanation on the Nine-point Center

TongGeometry illustrates theorem discovery through two triangle configurations, including a nine-point-center result and properties of a constructed tangent circle. The examples also show how auxiliary constructions reveal geometric relations and symmetry.

Explanation on the Nine-point Center

  • In △ABC, the circumcenter N of △DEF is the midpoint of AO_A, linking this discovered fact to the nine-point circle and center properties.The passage describes angle chasing and symmetry across BC as a route to the result.Source: Explanation on the Nine-point Center · p. 19
  • The nine-point-center problem has mirror symmetry in B–C and E–F and can be made rotationally symmetric using circumcircles of △ACH and △ABH.Source: Explanation on the Nine-point Center · p. 19

Explanation on the Mixtilinear Incircle

  • In the mixtilinear-incircle configuration, A, B, C, E, and F are concyclic, and E and F mark arc midpoints.The circle through H, G, and I is tangent to AB, AC, and the circumcircle of △ABC; HG, BC, and IJ concur at K.Source: Explanation on the Mixtilinear Incircle · p. 19

Limitation

The authors describe limits in current models’ ability to construct multiple interrelated points and identify challenges in training data and problem translation. Human-proposed constraints can further obscure straightforward constructions.

Limitation

  • Current models fall short on problems requiring a sequence of interrelated actions, particularly those needing multiple new points.Source: Limitation · p. 20
  • The authors suggest that longer construction sequences may be harder because neural training data decreases exponentially with the number of steps.Source: Limitation · p. 20
  • Translating natural-language problems into sequential computer constructions remains underexplored, and human constraints can obscure straightforward constructions.The authors describe those intentional complexities as contributing to problem difficulty.Source: Limitation · p. 20

IMO 2024 P4 Full Solutions

The solution develops a chain of congruence, similarity, midpoint, and cyclicity relations, culminating in an angle equality involving K, I, L, X, P, and Y.

IMO 2024 P4 Full Solutions

  • The proof establishes congruence of AFI and ZfI and of AEI and ZeI, plus similarity of EFe to ZfI and EFe to ZeI.Source: IMO 2024 P4 Full Solutions · p. 20
  • Equal lengths and collinearity establish that I is the midpoint of AZ.The proof then uses this midpoint to derive ratios involving AB, AL, AC, and AK.Source: IMO 2024 P4 Full Solutions · p. 21
  • The proof establishes cyclicity for BPXZ and CPYZ, citing an angle equality between PBX and PZX for the first configuration and between PCY and PZY for the second.Source: IMO 2024 P4 Full Solutions · p. 21
  • The derivation culminates in ∠KIL = ∠XPY.This is obtained from the preceding angle relations involving AIL and AIK.Source: IMO 2024 P4 Full Solutions · p. 22

TongGeometry Proposals to 2024 USEMO

The proposals present detailed triangle constructions as olympiad proof tasks, including midpoint, cyclicity, and distance claims.

TongGeometry Proposals to 2024 USEMO

  • One proposal asks for KL = KM after constructing an acute triangle with incenter D, an excenter, two circle intersections on BC, and K as the midpoint of IJ.The construction also defines L and M through second intersections involving IF and EJ.Source: TongGeometry Proposals to 2024 USEMO · p. 22
  • Another proposal constructs circumcenters, projections, and circle intersections in an acute triangle, then asks for a cyclicity result.Its construction includes projections G and H of D and intersections I and J on the specified circles.Source: TongGeometry Proposals to 2024 USEMO · p. 22
  • A scalene-triangle proposal uses two parallelograms, two circles through A, and reflected points Q′ and P′ to ask for conditions on PQ and AF.F is defined as the intersection of DC and EB, with the condition that F be the A-excenter.Source: TongGeometry Proposals to 2024 USEMO · pp. 22–23

TongGeometry Proposals to 2024 NHSML (Beijing)

These proposals specify acute-triangle configurations built from feet, circumcenters, projections, and reflections, then pose geometric proof tasks.

TongGeometry Proposals to 2024 NHSML (Beijing)

  • A selected proposal asks to prove IF = IK using triangle feet, an orthocenter, a circumcenter, and a line parallel to EF.K is defined where CF meets the line through J parallel to EF.Source: TongGeometry Proposals to 2024 NHSML… · p. 23
  • One proposal constructs points through successive reflections and circle intersections in an acute triangle.Its setup places E on AC with ∠EBC right, reflects E over B to F and F over C to G, then defines I and J.Source: TongGeometry Proposals to 2024 NHSML… · p. 23
  • Another proposal defines a construction in an acute triangle using the angle-bisector intersection, a projection, reflections, and a circumcenter.The listed construction continues through points I, J, K, L, M, O, and P.Source: TongGeometry Proposals to 2024 NHSML… · p. 23

Proof of Proposal Acceptance

TongGeometry proposals received competition recognition: one appeared as the second problem on the 2024 NHSML (Beijing) test, and proposals were shortlisted for 2024 USEMO.

Proof of Proposal Acceptance

Related papers

Loading 2412.10673v1…