論文の概要: MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
- arxiv url: http://arxiv.org/abs/2608.02295v1
- Date: Mon, 03 Aug 2026 14:24:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-04 15:07:25.596051
- Title: MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
- Title（参考訳）: MechGeo: リーン4におけるユークリッド幾何学の自動化と証明
- Abstract要約: 本稿では,真正な自己形式化とユークリッド幾何学の証明構築を共同で扱うMathlibネイティブエージェントフレームワークであるMechGeoを紹介する。
GeoFormalizerはGeoIRの非公式な問題を表し、決定論的にそれらをLean 4に翻訳し、候補ステートメントを反復的に修復する。
GeoProverは幾何学的証明計画を構築し、中間補題を導出し、Leanで検証されたライブラリを通して適切なサブゴールを選択的に代数化する。
- 参考スコア（独自算出の注目度）: 5.103695715197289
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean's kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP's Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.
- Abstract（参考訳）: 本稿では,真正な自己形式化とユークリッド幾何学の証明構築を共同で扱うMathlibネイティブエージェントフレームワークであるMechGeoを紹介する。
このフレームワークでは、GeoFormalizerはGeoIRの非公式な問題を表現し、決定論的にそれらをLean 4に翻訳し、構造診断とセマンティック評価を使用して候補ステートメントを反復的に修復する。
GeoProverは幾何学的証明計画を構築し、中間補題を導出し、Leanで検証されたライブラリを通して適切なサブゴールを選択的に代数化する。
SingularやSymPyは代数的な証明書を生成するが、結果の証明と反例はすべてLeanのカーネルによってチェックされる。
LLMバックボーンの7つの実験は、特により弱い直接翻訳性能を持つモデルにおいて、オートフォーマル化の大幅な改善を示している。
43の歴史的IMO幾何学問題において、GeoFormalizerは29のケースでGeoProverが証明した公式なステートメントを生成する。
IMO 2026 Issue 2と合わせて、私たちの知る限り、IMOの幾何学的問題に対する自動化されたカーネルチェック済みのリーン証明のコレクションが報告されている最大のものになります。
LEAPのLean-IMO-Benchの14の幾何学的ステートメントでは、MechGeoが初めて12を証明し、残りの2つを正式に否定し、どちらも修復されたステートメントを証明している。
これらの結果は、信頼性の高い形式幾何学の実践的基礎として、診断、幾何学的推論、証明された記号計算の逆例を確立している。
関連論文リスト
- Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean [7.28030691695892]
Eucleanは、ネイティブのMathlibで自動的に幾何学を定式化するフレームワークである。
ヒトの評価では48.89%のTOP1と73.33%のTOP5が正確である。
論文 参考訳（メタデータ） (2026-06-17T15:27:17Z) - Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning [5.723373368342653]
Hilbert-Geoは、固体幾何学のための最初の統一形式言語フレームワークである。
本稿では,まず2段階の推論を含むParse2Reason法を提案する。
提案手法は,SolidFGeo2kで77.3%,MathVerse-Solidで84.1%の性能を実現する。
論文 参考訳（メタデータ） (2026-05-11T13:42:41Z) - Geoparsing: Diagram Parsing for Plane and Solid Geometry with a Unified Formal Language [60.70116693224378]
我々は平面と固体の幾何学を統合した統一形式言語を設計し、幾何学構造と意味関係を包括的に網羅する。
GDP-29Kは,実世界の様々な情報源から収集した20k平面と9k固体形状のサンプルからなる大規模データセットである。
論文 参考訳（メタデータ） (2026-04-13T15:09:56Z) - Achieving Olympia-Level Geometry Large Language Model Agent via Complexity Boosting Reinforcement Learning [66.79506488139707]
大規模言語モデル(LLM)エージェントは強力な数学的問題解決能力を示す。
本研究では,メダリストレベルのメダリストレベルのLLMエージェントの構築とインターンジオメトリの紹介を行う。
InternGeometryは、命題と補助的な構成を反復的に提案することで幾何学の限界を克服し、それらを記号エンジンで検証する。
InternThinker-32BをベースとしたInternGeometryは、50 IMOの幾何学的問題の44を解き、平均金メダリストスコア(40.9)を超える。
論文 参考訳（メタデータ） (2025-12-11T11:05:04Z) - LeanGeo: Formalizing Competitional Geometry problems in Lean [22.345645897808357]
Lean 4定理証明器内の幾何学的問題を形式化し、解決するための統一的な形式システムであるLeanGeoを紹介します。
LeanGeoはLeanの基本ロジックを備えた高度な幾何学的定理の包括的なライブラリを備えており、厳密な検証を可能にしている。
また、IMO(International Mathematical Olympiad)や他の先進的な情報源からの問題を含むLeanGeoの形式的幾何ベンチマークであるLeanGeo-Benchについても紹介する。
論文 参考訳（メタデータ） (2025-08-20T11:55:19Z) - TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving [106.04001249574786]
TrustGeoGenは、標準的で信頼性の高いベンチマークを確立するために、正式に検証された幾何問題を生成するデータエンジンである。
1)ダイアグラム,テキスト,ステップバイステップのソリューションの生成を同期するマルチモーダルアライメント,2)すべての推論パスがルール準拠であることを保証する形式検証,3)接続思考,ブリッジング,ヒューマンライクな論理ステップとの論理的推論,4)複数のソリューションと自己回帰バックトラックを備えた多種多様な問題を生成できるTextitGeoExploreシリーズアルゴリズム。
論文 参考訳（メタデータ） (2025-04-22T10:45:23Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。