Fugu-MT 論文翻訳(概要): Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

論文の概要: Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

arxiv url: http://arxiv.org/abs/2607.19374v1
Date: Wed, 17 Jun 2026 15:27:17 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-27 00:46:13.139179
Title: Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean
Title（参考訳）: Euclean: リーンで統一された検証を備えた自動幾何学問題の定式化
Abstract要約: Eucleanは、ネイティブのMathlibで自動的に幾何学を定式化するフレームワークである。ヒトの評価では48.89%のTOP1と73.33%のTOP5が正確である。
参考スコア（独自算出の注目度）: 7.28030691695892
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Recent formal reasoning systems have reached IMO-level performance, yet they leave a fragmented landscape: algebra and number theory are handled in Lean, while geometry still relies on domain-specific languages with limited formal guarantees. This split increases the trusted computing base and hinders unified model development. Existing geometry-in-Lean efforts (LeanEuclid, LeanGeo) introduce custom axiom systems incompatible with standard Mathlib, and their small scale ($<$ 1,100 problems) limits large-scale training. Native Mathlib autoformalization of geometry, however, poses distinct challenges: implicit diagrammatic assumptions (e.g., topological configuration and non-degeneracy) must be made explicit rather than deferred to external solvers, and models must adapt to Mathlib's small, rapidly evolving geometry infrastructure. We present Euclean, a four-stage framework - constraint explication, configuration anchoring, formalization mapping, and iterative repair - for automatically formalizing geometry in native Mathlib. We construct OMNI-Geometry (768 competition problems) and Numina-Geometry (177,597 problems), the largest geometry formalization dataset in Lean. Human evaluation shows 48.89% TOP1 and 73.33% TOP5 accuracy. Training Goedel v2 on our formalizations improves proof success from 13.6% to 15.1%, validating dataset quality for unified neural theorem proving. Code and datasets: https://github.com/tlb-22/Euclean.
Abstract（参考訳）: 代数と数論はリーンで扱われるが、幾何学は依然として限定的な形式保証を持つドメイン固有言語に依存している。この分裂は信頼されたコンピューティング基盤を増大させ、統一されたモデル開発を妨げる。既存の幾何学の取り組み(LeanEuclid、LeanGeo)は、標準のMathlibと互換性のないカスタム公理システムを導入し、その小規模($1100)で大規模トレーニングを制限している。暗黙的な図式的な仮定(例えば、位相的構成や非退化)は、外部の解法に従わずに明示されなければならないし、モデルは、Mathlibの小さな、急速に進化した幾何学基盤に適応しなければならない。我々は、ネイティブのMathlibでジオメトリを自動的に形式化する、4段階のフレームワークであるEucleanを紹介します。我々は,OMNI-Geometry (768の競合問題)とNumina-Geometry (177,597の問題)を構築した。ヒトの評価では48.89%のTOP1と73.33%のTOP5が正確である。フォーマル化に関するGoedel v2のトレーニングは、証明の成功を13.6%から15.1%に改善し、統一されたニューラル定理証明のためのデータセット品質を検証する。コードとデータセット:https://github.com/tlb-22/Euclean。

関連論文リスト

MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4 [5.103695715197289]
本稿では,真正な自己形式化とユークリッド幾何学の証明構築を共同で扱うMathlibネイティブエージェントフレームワークであるMechGeoを紹介する。 GeoFormalizerはGeoIRの非公式な問題を表し、決定論的にそれらをLean 4に翻訳し、候補ステートメントを反復的に修復する。 GeoProverは幾何学的証明計画を構築し、中間補題を導出し、Leanで検証されたライブラリを通して適切なサブゴールを選択的に代数化する。
論文参考訳（メタデータ） (2026-08-03T14:24:12Z)
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)
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)
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)

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

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