論文の概要: Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4

• arxiv url: http://arxiv.org/abs/2602.18767v1
• Date: Sat, 21 Feb 2026 09:12:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-24 17:42:02.30331
• Title: Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
• Title（参考訳）: Nazrin: リーン4での定理証明のためのグラフニューラルネットワークのアトミック戦術
• Authors: Leni Aniva, Iori Oikawa, David Dill, Clark Barrett,
• Abstract要約: 本稿では,機械支援定理証明が直面する障害に対処するための新しい概念と能力を紹介する。 Nazrin Proverは、原子戦術とExprGraphを用いたグラフニューラルネットワークに基づく定理証明エージェントである。
• 参考スコア（独自算出の注目度）: 0.4030494018340581
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a conjecture in a proof assistant. In this work, we introduce several novel concepts and capabilities to address obstacles faced by machine-assisted theorem proving. We first present a set of \textbf{atomic tactics}, a small finite set of tactics capable of proving any provable statement in Lean. We then introduce a \textbf{transposing atomization} algorithm which turns arbitrary proof expressions into a series of atomic tactics. We next introduce the \textbf{ExprGraph} data structure, which provides a succinct representation for Lean expressions. Finally, we present the \textbf{Nazrin Prover}, a graph neural network-based theorem proving agent using atomic tactics and ExprGraph. Nazrin circumvents many challenges faced by existing proving agents by exclusively dispatching atomic tactics, and it is robust enough to both train and evaluate on consumer-grade hardware. We demonstrate the potential of tools like Nazrin using theorems from Lean's standard library and from Mathlib.
• Abstract（参考訳）: 機械支援定理証明において、定理証明エージェントは、証明アシスタントで予想を証明できる一連の式と戦術を探索する。 本研究では,機械支援定理証明が直面する障害に対処する,いくつかの新しい概念と能力を紹介する。 まず最初に、リーンで証明可能な言明を証明できる小さな有限の戦術である、‘textbf{atomic tactics}’のセットを提示します。 次に、任意の証明式を一連のアトミックな戦術に変換する「textbf{transposing atomization」アルゴリズムを導入する。 次に、リーン表現の簡潔な表現を提供する、textbf{ExprGraph}データ構造を紹介します。 最後に、原子戦術とExprGraphを用いたグラフニューラルネットワークに基づく定理証明エージェントである「textbf{Nazrin Prover}」を提案する。 ナズリンは、既存の証明エージェントが直面する多くの課題を回避し、アトミック戦術のみを派遣し、消費者階級のハードウェアでトレーニングと評価を行うのに十分堅牢である。 リーンの標準ライブラリとMathlibの定理を使って、Nazrinのようなツールの可能性を示します。

関連論文リスト

• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。 IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。 シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
  論文  参考訳（メタデータ） (2025-07-31T17:00:30Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge [0.0]
  Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。 Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。 現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
  論文  参考訳（メタデータ） (2020-12-20T18:15:12Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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