論文の概要: Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4

• arxiv url: http://arxiv.org/abs/2410.16429v1
• Date: Mon, 21 Oct 2024 18:49:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-23 14:29:31.858395
• Title: Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
• Title（参考訳）: Pantograph: リーン4の高度な定理証明,高レベルの推論,データ抽出のための,マシン間インタラクションインターフェース
• Authors: Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, Sanmi Koyejo,
• Abstract要約: PantographはLean 4の証明アシスタントに汎用的なインターフェースを提供するツールである。 Pantographはモンテカルロ木探索のような強力な探索アルゴリズムによる効率的な証明検索を可能にする。 PantographはLean 4の推論ステップをより堅牢に扱えるようにすることで、高いレベルの推論を可能にします。
• 参考スコア（独自算出の注目度）: 12.07461387498206
• License:
• Abstract: Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a surge of interest in using machine learning models in conjunction with proof assistants to perform this task. In this paper, we introduce Pantograph, a tool that provides a versatile interface to the Lean 4 proof assistant and enables efficient proof search via powerful search algorithms such as Monte Carlo Tree Search. In addition, Pantograph enables high-level reasoning by enabling a more robust handling of Lean 4's inference steps. We provide an overview of Pantograph's architecture and features. We also report on an illustrative use case: using machine learning models and proof sketches to prove Lean 4 theorems. Pantograph's innovative features pave the way for more advanced machine learning models to perform complex proof searches and high-level reasoning, equipping future researchers to design more versatile and powerful theorem provers.
• Abstract（参考訳）: 機械支援定理証明(英: Machine-assisted theorem proving)とは、数学的定理の証明を自動的に生成する構造的推論を実行する過程を指す。 近年、機械学習モデルと証明アシスタントを併用してこの課題を実行することへの関心が高まっている。 本稿では,Pantographについて紹介する。PantographはLean 4の証明アシスタントに汎用的なインタフェースを提供し,モンテカルロ木探索のような強力な探索アルゴリズムによる効率的な証明検索を可能にするツールである。 さらに、PantographはLean 4の推論ステップをより堅牢に扱えるようにすることで、高いレベルの推論を可能にします。 この記事では、Pantographのアーキテクチャと機能の概要を紹介する。 機械学習モデルと証明スケッチを使ってLean 4の定理を証明します。 パンタグラフのイノベーティブな特徴は、より高度な機械学習モデルが複雑な証明探索と高レベルの推論を実行し、将来の研究者がより汎用的で強力な定理プローバーを設計する道を開く。

関連論文リスト

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Autograding Mathematical Induction Proofs with Natural Language Processing [0.12289361708127876]
  本稿では,自由形式の数学的証明を自動分解できる一連のトレーニング手法とモデルを提案する。 モデルは、誘導問題によって4つの異なる証明から収集された証明データを用いて訓練される。 我々は、トレーニングデータと同じ証明を格付けするために、人間のグルーパーを雇い、最高のグルーパーモデルが、ほとんどの人間のグルーパーよりも正確であることに気付きました。
  論文  参考訳（メタデータ） (2024-06-11T15:30:26Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Struc-Bench: Are Large Language Models Really Good at Generating Complex Structured Data? [49.688233418425995]
  Struc-Benchは、大きな言語モデル(LLM)を特徴とする包括的なベンチマークである。 Pスコア(Prompting Score)とHスコア(Heuristical Score)の2つの革新的な指標を提案する。 実験の結果,LLaMA-7Bに構造認識の微調整を適用すると,性能が大幅に向上することがわかった。
  論文  参考訳（メタデータ） (2023-09-16T11:31:58Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs [30.57062828812679]
  本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。 大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
  論文  参考訳（メタデータ） (2022-10-21T22:37:22Z)
• 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)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• IsarStep: a Benchmark for High-level Mathematical Reasoning [20.96474618260995]
  本稿では,高レベルな数学的推論のためのベンチマークを提案し,ニューラルシークエンス・ツー・シーケンスモデルの推論能力について検討する。 我々は、人間の専門家が定理証明器で記述した最大の証明のリポジトリから、非合成データセットを構築した。
  論文  参考訳（メタデータ） (2020-06-13T21:09:23Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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