論文の概要: Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization

• arxiv url: http://arxiv.org/abs/2604.16347v1
• Date: Mon, 16 Mar 2026 14:19:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-04 02:32:13.915185
• Title: Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
• Title（参考訳）: Lean Atlas: スケーラブルなHuman-AIコラボレーションの形式化のための統合的な証明環境
• Authors: Banri Yanahama, Akiyoshi Sannai,
• Abstract要約: 本稿では,人間科学者とAIが共同で公式な証明を行う,ループ型アプローチを提案する。 Lean Atlasはリーン4プロジェクトの依存性グラフをインタラクティブなWebビューアとして視覚化するツールです。 コア機能であるLean Compassは、選択された定理セットが与えられたら、自動的にプロジェクト固有のノードを抽出するアルゴリズムである。
• 参考スコア（独自算出の注目度）: 1.711666249985278
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI-driven autoformalization of mathematics is advancing rapidly. However, the type checker of a proof assistant guarantees only the logical correctness of proofs; it does not verify whether propositions and definitions faithfully capture their intended mathematical content. Consequently, AI-generated formal proofs can exhibit semantic hallucination-passing the type checker yet failing to express the intended mathematics. We propose a human-in-the-loop approach in which human scientists and AI collaboratively produce formal proofs, with humans responsible for the semantic verification of propositions and definitions. To realize this approach, we develop Lean Atlas, a Lean 4 tool that visualizes the dependency graph of a Lean 4 project as an interactive web viewer, enabling human scientists to grasp the overall structure of a formalization efficiently. Its core feature, Lean Compass, is an algorithm that, given a selected theorem set, automatically extracts the project-specific nodes whose semantic correctness can affect those target statements, thereby reducing the candidate set for semantic review in large-scale formalizations. We further define *aligned Lean code* as formalization code that has undergone human semantic verification, and propose it as a quality standard for AI-generated formalizations. We evaluate the tool on six Lean 4 formalization projects with different structural characteristics; proof-heavy projects (PrimeNumberTheoremAnd, Carleson, Brownian Motion) achieved 94-99% average node reduction, a 6-theorem milestone subset of FLT achieved 59.8%, mixed PhysLib 69.0%, and definition-heavy XMSS 27.3%. Lean Atlas is available as open-source software at https://github.com/NyxFoundation/lean-atlas .
• Abstract（参考訳）: AIによる数学の自己形式化は急速に進んでいる。 しかし、証明アシスタントの型チェッカーは証明の論理的正当性のみを保証する。 その結果、AIが生成した形式証明は、意図した数学を表現できない型チェッカーを通した意味幻覚を示すことができる。 本稿では,人間科学者とAIが共同で公式な証明を作成し,命題や定義のセマンティックな検証に責任を負う,ループ型アプローチを提案する。 このアプローチを実現するために,リーン4プロジェクトの依存性グラフをインタラクティブなWebビューアとして視覚化するLean 4ツールであるLean Atlasを開発した。 その中核的な特徴であるLean Compassは、選択された定理セットを与えられたアルゴリズムであり、意味的正しさが対象のステートメントに影響を与える可能性のあるプロジェクト固有のノードを自動的に抽出し、大規模な形式化における意味的レビューの候補セットを減らす。 我々はさらに、人間の意味的検証を行う形式コードとして*整列したリーンコード*を定義し、AI生成の形式化の品質標準として提案する。 我々は,このツールを6つのLean 4形式化プロジェクトで異なる構造特性で評価した。証明量の多いプロジェクト(PrimeNumberTheoremAnd,Carleson,Brownian Motion)は94～99%の平均ノード削減,FLTの6つの理論的なサブセットサブセットは59.8%,混合PhysLib 69.0%,定義量の多いXMSS 27.3%を達成した。 Lean Atlasはオープンソースソフトウェアとしてhttps://github.com/NyxFoundation/lean-atlasで公開されている。

関連論文リスト

• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
  論文  参考訳（メタデータ） (2026-04-26T13:24:20Z)
• Evaluating Frontier LLMs on PhD-Level Mathematical Reasoning: A Benchmark on a Textbook in Theoretical Computer Science about Randomized Algorithms [14.853721511192736]
  大規模言語モデル(LLM)は、自動数学的推論と科学的発見の突破口となった。 GP-5-Thinking、Gemini-3-Pro、Claude-Sonnet-4.5-Thinking、Grok-4の4つのフロンティアモデルのベンチマークを示す。 上位モデルの精度は高いが,他のモデルでは一貫性が著しく低下していることがわかった。
  論文  参考訳（メタデータ） (2025-12-16T00:34:55Z)
• Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph [7.606625807305093]
  リーンの予想レベルの形式化のためのシステムであるAriaを紹介します。 Ariaは、2フェーズのGraph-of-Thoughtプロセスを通じて、人間の専門家による推論をエミュレートする。 AriaScorerは、用語レベルの接地のためにMathlibから定義を検索する。
  論文  参考訳（メタデータ） (2025-10-06T06:25:11Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)

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

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