論文の概要: Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions

• arxiv url: http://arxiv.org/abs/2512.00097v1
• Date: Thu, 27 Nov 2025 01:05:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-02 19:46:34.062121
• Title: Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
• Title（参考訳）: 効率的なヒューリスティック補助構造を用いたゴールド・メダル・レベルオリンピアド幾何解法
• Authors: Boyan Duan, Xiao Liang, Shuai Lu, Yaoxiang Wang, Yelong Shen, Kai-Wei Chang, Ying Nian Wu, Mao Yang, Weizhu Chen, Yeyun Gong,
• Abstract要約: 本稿では、ニューラルネットワークに基づく推論に頼ることなく、CPU上で完全に動作する幾何定理証明の高効率な方法を提案する。 IMO(International Mathematical Olympiad)において,補助点を追加するための単純なランダム戦略により,銀・医療レベルの人的パフォーマンスが達成できることを示す。 さらに,HAGeo-409という,人為的な難易度を持つ409の幾何学的問題からなるベンチマークを構築した。
• 参考スコア（独自算出の注目度）: 129.877899436804
• License: http://creativecommons.org/licenses/by/4.0/
• 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 constructions 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-409, 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.
• Abstract（参考訳）: ユークリッド幾何学、特に国際数学オリンピック(IMO)レベルの問題で証明された自動定理は、人工知能において大きな課題であり重要な研究課題である。 本稿では,ニューラルネットワークに基づく推論に頼ることなく,CPU上で完全に動作する幾何定理の高効率な証明法を提案する。 最初の研究は、補助点を追加するための単純なランダム戦略が、IMO上での銀・医療レベルの人的パフォーマンスを達成できることを示している。 IMO-30ベンチマークで30の問題を28つ解決し、ゴールドメディカルレベルのパフォーマンスを実現し、競合するニューラルネットワークベースのアプローチであるAlphaGeometryをはるかに上回る、ヒューリスティックな手法であるHAGeoを提案する。 提案手法と既存手法をより包括的に評価するため,HAGeo-409は,409の幾何学的問題と人為的難易度からなるベンチマークである。 広く使われているIMO-30と比較して、我々のベンチマークはより大きな課題を提起し、より正確な評価を提供し、幾何定理の証明のバーを高く設定する。

関連論文リスト

• GeoGramBench: Benchmarking the Geometric Program Reasoning in Modern LLMs [7.605833826892782]
  本稿では,従来の数学的推論の複雑さではなく,幾何学的複雑性を考慮した3段階分類によって整理された500の精巧な問題のベンチマークを示す。 17個のフロンティアLSMの総合的な評価により,一貫性と顕著な欠陥が明らかとなった。 これらの結果は、プログラム駆動型空間推論によって引き起こされる独特な課題を浮き彫りにし、シンボル-空間幾何学的推論の研究を進めるための貴重な資源としてGeoGramBenchを確立した。
  論文  参考訳（メタデータ） (2025-05-23T09:17:07Z)
• PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
  本稿では,高品質なオリンピアードレベルの数学問題を自動生成する新しい手法であるPromptCoTを紹介する。 提案手法は,問題構築の背景にある数学的概念と理論的根拠に基づいて複雑な問題を合成する。 提案手法は, GSM8K, MATH-500, AIME2024などの標準ベンチマークで評価され, 既存の問題生成手法を一貫して上回っている。
  論文  参考訳（メタデータ） (2025-03-04T06:32:30Z)
• Proposing and solving olympiad geometry with guided tree search [63.824930029019995]
  木探索に基づくガイド付き問題解決を支援するユークリッド幾何学システムであるTongGeometryを紹介する。 TongGeometryは、補助的な構成を必要とする67億の幾何学定理を発見した。 トンゲメトリーはIMO-AG-30ですべての国際数学オリンピック幾何学を解き、金メダリストを初めて上回った。
  論文  参考訳（メタデータ） (2024-12-14T04:20:47Z)
• Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models [63.31878920079154]
  Olympiadレベルでの大規模言語モデルの数学的推論を評価するためのベンチマークを提案する。 既存のOlympiad関連のベンチマークとは違って、我々のデータセットは数学に特化しており、厳密な人間のアノテーションを使った4428の競合レベルの問題の膨大なコレクションを含んでいる。 実験の結果,最も先進的なモデルであるOpenAI o1-miniとOpenAI o1-previewでさえ,60.54%と52.55%の精度で,オリンピアードレベルの問題に悩まされ,オリンピアードレベルの数学的推論において重大な課題が浮き彫りにされていることがわかった。
  論文  参考訳（メタデータ） (2024-10-10T14:39:33Z)
• Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry [16.41436428888792]
  我々は、AlphaGeometryで導入されたIMO-AG-30 Challengeを再考し、Wuの手法が驚くほど強いことを発見した。 ウーの方法だけでは15の問題を解くことができ、そのうちのいくつかは他の方法では解けない。 IMO-AG-30では,30問題中27を解き,IMOゴールドメダリストに勝るAI手法として,新たな最先端の自動定理を定めている。
  論文  参考訳（メタデータ） (2024-04-09T15:54:00Z)
• FGeo-TP: A Language Model-Enhanced Solver for Geometry Problems [1.137457877869062]
  本稿では,FGeo-TP (Theorem Predictor)を導入し,この言語モデルを用いて定理列の予測を行い,幾何学的問題を解く。 本研究では,FormalGeo7kデータセット上での言語モデル強化FGeo-TPの問題解決率を著しく向上させることを示す。
  論文  参考訳（メタデータ） (2024-02-14T09:44:28Z)
• GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning [172.36214872466707]
  我々は、テキスト記述、視覚図、定理知識の包括的理解を必要とする幾何学的問題を解くことに注力する。 そこで本研究では,5,010の幾何学的問題を含む幾何学的質問応答データセットGeoQAを提案する。
  論文  参考訳（メタデータ） (2021-05-30T12:34:17Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  3,002の幾何学的問題と密接なアノテーションを形式言語に含む新しい大規模ベンチマークGeometry3Kを構築します。 我々は、Interpretable Geometry Problemsolvr (Inter-GPS)と呼ばれる形式言語と記号推論を用いた新しい幾何学的解法を提案する。 イントラGPSは定理の知識を条件付き規則として取り入れ、記号的推論を段階的に行う。
  論文  参考訳（メタデータ） (2021-05-10T07:46:55Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。