論文の概要: Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
- arxiv url: http://arxiv.org/abs/2606.02588v1
- Date: Wed, 20 May 2026 08:15:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-07 20:42:22.567532
- Title: Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
- Title（参考訳）: Lean-GAP: 形式化された大学院代数問題のデータセット
- Abstract要約: 本稿では,PDF-to-La Algebra前処理,Lean 4への自動形式化,非公式な形式対応の検証などからなるスケーラブルなパイプラインを開発する。
コントリビューションには、(i)形式化された演習の構造化データセットの構築、(ii)教科書数学の形式化のための体系的方法論、(iii)形式化過程における繰り返しの課題の分析が含まれる。
- 参考スコア（独自算出の注目度）: 3.1963549333419388
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present Lean-GAP (Lean-Graduate Agebra Problems), 430 formalized graduate-level algebra problems from the textbook Abstract Algebra by Dummit and Foote. We develop a scalable pipeline consisting of PDF-to-LaTeX preprocessing, autoformalization into Lean 4, and verification of informal-formal correspondence. While the preprocessing and autoformalization stages can be largely automated, we find that verification remains the most subtle and labor-intensive component, requiring careful human oversight. Our contributions include (i) the construction of a structured dataset of formalized exercises, (ii) a systematic methodology for formalizing textbook mathematics, and (iii) an analysis of recurring challenges in the formalization process. We also compare the performance of different autoformalization models and highlight key bottlenecks in translating informal statements into formal language.
- Abstract（参考訳）: 本稿では,Dummit と Foote の教科書 Abstract Algebra から,Lean-GAP (Lean-Graduate Agebra Problems, 430) を公式化した。
本稿では,PDF-to-LaTeX前処理,Lean 4への自動形式化,非公式-形式対応の検証などからなるスケーラブルなパイプラインを開発する。
事前処理と自己形式化の段階は大部分が自動化できるが、検証は依然として最も微妙で労働集約的な要素であり、慎重に人間の監視を必要とする。
コントリビューションには
一 形式化された運動の構造化データセットの構築
(二)教科書数学の形式化のための体系的方法論、及び
三 形式化の過程における繰り返しの課題の分析。
また、異なる自動形式化モデルの性能を比較し、非公式な文を形式言語に翻訳する際の重要なボトルネックを強調します。
関連論文リスト
- Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance [0.3624700141426058]
コーディングエージェントはLean 4で高度な数学教科書全体を形式化できます。
本稿では,コンパイラを超えてエージェント生成形式の品質を評価するためのフレームワークを提案する。
以上の結果から,コンパイルベースのメトリクスは形式化品質を大幅に上回っていることが示唆された。
論文 参考訳（メタデータ） (2026-06-12T00:45:42Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Conjecturing: An Overlooked Step in Formal Mathematical Reasoning [10.398167568549924]
結論を導かない限り、多くの数学的問題は直接形式化できない。
本研究では,大規模言語モデルの導出能力を測定するためにConjectureBenchを開発した。
提案手法は,GPT-4.1と7とDeepSeek-V3.1の13のPutnamBench問題において,最初のエンドツーエンドの自動形式化を実現する。
論文 参考訳（メタデータ） (2025-10-13T22:29:49Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - FMC: Formalization of Natural Language Mathematical Competition Problems [12.86616278136374]
本稿では,誤りフィードバックを伴う大規模言語モデルに基づく自動形式化パイプラインを提案する。
Olympiadレベルのデータセットを、自然言語の問題をリーンの形式化と整合させます。
少数ショット学習,エラーフィードバック,サンプリング数の増加により,自動形式化プロセスが促進されることを示す。
論文 参考訳（メタデータ） (2025-07-15T12:52:47Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳（メタデータ） (2025-05-05T15:37:00Z) - Process-Driven Autoformalization in Lean 4 [30.056591518828554]
大規模言語モデルの自己形式化能力を評価するためのベンチマークを開発する。
また、Lean 4コンパイラからの正確なフィードバックを利用して自動形式化を強化するモデルも導入しています。
実験の結果,PSV法ではオートフォーマライゼーションが向上し,フィルタの少ないトレーニングデータによる精度が向上した。
論文 参考訳（メタデータ） (2024-06-04T03:48:08Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳（メタデータ） (2023-10-16T08:42:39Z) - FIMO: A Challenge Formal Dataset for Automated Theorem Proving [31.695624833932577]
FIMOは、IMOレベルでの高度な自動定理証明を容易にするように設計されている。
公式な問題文は149で、非公式な問題記述とそれに対応する非公式な証明の両方を伴っている。
論文 参考訳（メタデータ） (2023-09-08T12:34:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。