論文の概要: LeanGeo: Formalizing Competitional Geometry problems in Lean
- arxiv url: http://arxiv.org/abs/2508.14644v1
- Date: Wed, 20 Aug 2025 11:55:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-21 16:52:41.442544
- Title: LeanGeo: Formalizing Competitional Geometry problems in Lean
- Title（参考訳）: LeanGeo: 競争幾何学の問題をリーンで形式化する
- Authors: Chendong Song, Zihan Wang, Frederick Pu, Haiming Wang, Xiaohan Lin, Junqi Liu, Jia Li, Zhengying Liu,
- Abstract要約: Lean 4定理証明器内の幾何学的問題を形式化し、解決するための統一的な形式システムであるLeanGeoを紹介します。
LeanGeoはLeanの基本ロジックを備えた高度な幾何学的定理の包括的なライブラリを備えており、厳密な検証を可能にしている。
また、IMO(International Mathematical Olympiad)や他の先進的な情報源からの問題を含むLeanGeoの形式的幾何ベンチマークであるLeanGeo-Benchについても紹介する。
- 参考スコア（独自算出の注目度）: 22.345645897808357
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Geometry problems are a crucial testbed for AI reasoning capabilities. Most existing geometry solving systems cannot express problems within a unified framework, thus are difficult to integrate with other mathematical fields. Besides, since most geometric proofs rely on intuitive diagrams, verifying geometry problems is particularly challenging. To address these gaps, we introduce LeanGeo, a unified formal system for formalizing and solving competition-level geometry problems within the Lean 4 theorem prover. LeanGeo features a comprehensive library of high-level geometric theorems with Lean's foundational logic, enabling rigorous proof verification and seamless integration with Mathlib. We also present LeanGeo-Bench, a formal geometry benchmark in LeanGeo, comprising problems from the International Mathematical Olympiad (IMO) and other advanced sources. Our evaluation demonstrates the capabilities and limitations of state-of-the-art Large Language Models on this benchmark, highlighting the need for further advancements in automated geometric reasoning. We open source the theorem library and the benchmark of LeanGeo at https://github.com/project-numina/LeanGeo/tree/master.
- Abstract（参考訳）: 幾何学問題は、AI推論能力にとって重要なテストベッドである。
既存の幾何解法系は統合された枠組み内での問題を表現できないため、他の数学分野と統合することは困難である。
さらに、ほとんどの幾何学的証明は直感的な図式に依存しているため、幾何学的問題を検証することは特に困難である。
これらのギャップに対処するために、Lean 4定理証明器内の競合レベルの幾何学問題を形式化し、解決するための統一的な形式システムであるLeanGeoを紹介します。
LeanGeoは、Leanの基本ロジックと高レベルの幾何学的定理の包括的なライブラリを備えており、厳密な証明検証とMathlibとのシームレスな統合を可能にしている。
また、IMO(International Mathematical Olympiad)や他の先進的な情報源からの問題を含むLeanGeoの形式的幾何ベンチマークであるLeanGeo-Benchについても紹介する。
このベンチマークでは,最先端の大規模言語モデルの能力と限界を実証し,自動幾何推論のさらなる進歩の必要性を強調した。
定理ライブラリとLeanGeoのベンチマークをhttps://github.com/project-numina/LeanGeo/tree/masterで公開しています。
関連論文リスト
- Proposing and solving olympiad geometry with guided tree search [63.824930029019995]
木探索に基づくガイド付き問題解決を支援するユークリッド幾何学システムであるTongGeometryを紹介する。
TongGeometryは、補助的な構成を必要とする67億の幾何学定理を発見した。
トンゲメトリーはIMO-AG-30ですべての国際数学オリンピック幾何学を解き、金メダリストを初めて上回った。
論文 参考訳（メタデータ） (2024-12-14T04:20:47Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - G-LLaVA: Solving Geometric Problem with Multi-Modal Large Language Model [121.07873620883322]
大規模言語モデル(LLM)は、人間レベルの推論と生成能力に顕著な習熟性を示している。
G-LLaVAは幾何学的問題の解法において例外的な性能を示し、7Bパラメータしか持たないMathVistaベンチマークにおいて GPT-4-V を著しく上回っている。
論文 参考訳（メタデータ） (2023-12-18T17:36:20Z) - FormalGeo: An Extensible Formalized Framework for Olympiad Geometric
Problem Solving [9.73597821684857]
これは、私たちが過去3年間に達成した一連の研究の中で、初めての論文です。
本稿では,一貫した平面幾何学システムを構築した。
これは、IMOレベルの平面幾何学の課題と、可読性のあるAI自動推論の間に重要な橋渡しとなる。
論文 参考訳（メタデータ） (2023-10-27T09:55:12Z) - UniGeo: Unifying Geometry Logical Reasoning via Reformulating
Mathematical Expression [127.68780714438103]
計算と証明の2つの主要な幾何学問題は、通常2つの特定のタスクとして扱われる。
我々は4,998の計算問題と9,543の証明問題を含むUniGeoという大規模統一幾何問題ベンチマークを構築した。
また,複数タスクの幾何変換フレームワークであるGeoformerを提案し,計算と証明を同時に行う。
論文 参考訳（メタデータ） (2022-12-06T04:37:51Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。