論文の概要: Towards Large Language Models as Copilots for Theorem Proving in Lean

• arxiv url: http://arxiv.org/abs/2404.12534v1
• Date: Thu, 18 Apr 2024 22:54:08 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-22 16:34:43.304702
• Title: Towards Large Language Models as Copilots for Theorem Proving in Lean
• Title（参考訳）: リーンにおける定理証明のコパイロットとしての大規模言語モデルを目指して
• Authors: Peiyang Song, Kaiyu Yang, Anima Anandkumar,
• Abstract要約: 大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
• 参考スコア（独自算出の注目度）: 81.94024084598598
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Theorem proving is an important challenge for large language models (LLMs), as formal proofs can be checked rigorously by proof assistants such as Lean, leaving no room for hallucination. Existing LLM-based provers try to prove theorems in a fully autonomous mode without human intervention. In this mode, they struggle with novel and challenging theorems, for which human insights may be critical. In this paper, we explore LLMs as copilots that assist humans in proving theorems. We introduce Lean Copilot, a framework for running LLM inference in Lean. It enables programmers to build various LLM-based proof automation tools that integrate seamlessly into the workflow of Lean users. Using Lean Copilot, we build tools for suggesting proof steps (tactic suggestion), completing intermediate proof goals (proof search), and selecting relevant premises (premise selection) using LLMs. Users can use our pretrained models or bring their own ones that run either locally (with or without GPUs) or on the cloud. Experimental results demonstrate the effectiveness of our method in assisting humans and automating theorem proving process compared to existing rule-based proof automation in Lean. We open source all codes under a permissive MIT license to facilitate further research.
• Abstract（参考訳）: 定理証明は大きな言語モデル(LLM)にとって重要な課題であり、形式的な証明はリーンのような証明アシスタントによって厳格にチェックでき、幻覚の余地は残っていない。 既存のLLMベースのプローバーは、人間の介入なしに完全に自律的な方法で定理を証明しようとする。 このモードでは、人間の洞察が批判的な、斬新で挑戦的な定理に苦しむ。 本稿では,LLMを人間による定理証明を支援するコピロとして探索する。 リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 プログラマは、リーンユーザのワークフローにシームレスに統合する、さまざまなLCMベースの証明自動化ツールを構築できる。 Lean Copilotを使用することで、証明ステップ(戦術的提案)の提案、中間的証明目標(防御探索)の完了、LLMを使用して関連する前提(前提選択)を選択するためのツールを構築します。 トレーニング済みのモデルを使用したり、ローカルで(GPUの有無に関わらず)あるいはクラウド上で実行する独自のモデルを持ってくることができる。 実験の結果,従来のリーンのルールベースの証明自動化と比較して,人間の支援や定理証明プロセスの自動化に本手法の有効性が示された。 我々は、さらなる研究を促進するために、寛容なMITライセンスの下ですべてのコードをオープンソースにしています。

関連論文リスト

• zsLLMCode: An Effective Approach for Functional Code Embedding via LLM with Zero-Shot Learning [6.976968804436321]
  大型言語モデル(LLM)はゼロショット学習の能力を持ち、訓練や微調整を必要としない。 LLMを用いた関数型コード埋め込みを生成する新しいアプローチであるzsLLMCodeを提案する。
  論文  参考訳（メタデータ） (2024-09-23T01:03:15Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Efficient Tool Use with Chain-of-Abstraction Reasoning [65.18096363216574]
  大規模言語モデル(LLM)は、現実世界の知識に対する推論の基礎となる必要がある。 マルチステップ推論問題におけるツールの実行には,微調整LDMエージェントの課題が残されている。 マルチステップ推論におけるツールの活用方法として, LLM の新しい手法を提案する。
  論文  参考訳（メタデータ） (2024-01-30T21:53:30Z)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  大規模言語モデル(LLM)は、知識探索タスクにおける高い性能のため、知識ベースとして扱われてきた。 LLMが実際に正しい答えを連続的に生成する能力をどのように評価するか。 LLMの信頼性を直接測定するための新しい指標であるMOdel kNowledge relIabiliTy score (MONITOR)を提案する。
  論文  参考訳（メタデータ） (2023-10-15T12:40:30Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
  Self-Checkerはファクトチェックを容易にするプラグインとプレイモジュールからなるフレームワークである。 このフレームワークは、低リソース環境でファクトチェックシステムを構築するための、高速で効率的な方法を提供する。
  論文  参考訳（メタデータ） (2023-05-24T01:46:07Z)

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

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