@inproceedings{duan-etal-2026-gold,
    title = "Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions",
    author = "Duan, Boyan  and
      Liang, Xiao  and
      Lu, Shuai  and
      Wang, Yaoxiang  and
      Shen, Yelong  and
      Chang, Kai-Wei  and
      Wu, Ying Nian  and
      Yang, Mao  and
      Chen, Weizhu  and
      Gong, Yeyun",
    editor = "Liakata, Maria  and
      Moreira, Viviane P.  and
      Zhang, Jiajun  and
      Jurgens, David",
    booktitle = "Proceedings of the 64th Annual Meeting of the {A}ssociation for {C}omputational {L}inguistics (Volume 1: Long Papers)",
    month = jul,
    year = "2026",
    address = "San Diego, California, United States",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-acl/2026.acl-long.991/",
    pages = "21725--21747",
    ISBN = "979-8-89176-390-6",
    abstract = "Automated theorem proving in Euclidean geometry, particularly for International Mathematical Olympiad (IMO) level problems, remains a major challenge and an important research focus in Artificial Intelligence. In this paper, we present a highly efficient method for geometry theorem proving that runs entirely on CPUs without relying on neural network{--}based inference. Our initial study shows that a simple random strategy for adding auxiliary points can achieve ``silver-medal'' level human performance on IMO. Building on this, we propose HAGeo, a Heuristic-based method for adding Auxiliary points in Geometric deduction that solves 28 of 30 problems on the IMO-30 benchmark, achieving ``gold-medal'' level performance and surpassing AlphaGeometry, a competitive neural network{--}based approach, by a notable margin. To evaluate our method and existing approaches more comprehensively, we further construct HAGeo, a benchmark consisting of 409 geometry problems with human-assessed difficulty levels. Compared with the widely used IMO-30, our benchmark poses greater challenges and provides a more precise evaluation, setting a higher bar for geometry theorem proving."
}