Fugu-MT 論文翻訳(概要): A Language-Agent Approach to Formal Theorem-Proving

論文の概要: A Language-Agent Approach to Formal Theorem-Proving

arxiv url: http://arxiv.org/abs/2310.04353v2
Date: Mon, 11 Dec 2023 06:53:57 GMT
ステータス: 処理完了
システム内更新日: 2023-12-13 01:38:57.561285
Title: A Language-Agent Approach to Formal Theorem-Proving
Title（参考訳）: 形式的定理提示に対する言語エージェント的アプローチ
Authors: Amitayush Thakur, Yeming Wen, Swarat Chaudhuri
Abstract要約: フォーマルな定理証明への最初の言語エージェントアプローチを示す。 COPRAは,高容量のブラックボックスLCM (GPT-4) をステートフルなバックトラック検索のポリシーの一部として用いている。我々は、LeanのminiF2FベンチマークとCompcertプロジェクトからのCoqタスクセットに対するCOPRAの実装を評価した。
参考スコア（独自算出の注目度）: 14.037826400805741
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Language agents, which use a large language model (LLM) capable of in-context learning to interact with an external environment, have recently emerged as a promising approach to control tasks. We present the first language-agent approach to formal theorem-proving. Our method, COPRA, uses a high-capacity, black-box LLM (GPT-4) as part of a policy for a stateful backtracking search. During the search, the policy can select proof tactics and retrieve lemmas and definitions from an external database. Each selected tactic is executed in the underlying proof framework, and the execution feedback is used to build the prompt for the next policy invocation. The search also tracks selected information from its history and uses it to reduce hallucinations and unnecessary LLM queries. We evaluate our implementation of COPRA on the miniF2F benchmark for Lean and a set of Coq tasks from the Compcert project. On these benchmarks, COPRA significantly outperforms one-shot invocations of GPT-4, as well as state-of-the-art models fine-tuned on proof data, at finding correct proofs quickly. Our code and data are available at https://github.com/trishullab/copra.
Abstract（参考訳）: 言語エージェントは、コンテキスト内学習で外部環境と対話できる大規模言語モデル(LLM)を使用しており、タスクを制御するための有望なアプローチとして最近登場した。フォーマルな定理証明への最初の言語エージェントアプローチを示す。 COPRAは,高容量のブラックボックスLCM (GPT-4) をステートフルなバックトラック検索のポリシーの一部として用いる。検索中、ポリシーは証明戦術を選択し、外部データベースから補題や定義を取得することができる。各選択した戦術は基礎となる証明フレームワークで実行され、次のポリシー実行のプロンプトを構築するために実行フィードバックが使用される。検索はまた、選択した情報を履歴から追跡し、幻覚や不要なllmクエリを減らすために利用する。我々は、LeanのminiF2FベンチマークとCompcertプロジェクトからのCoqタスクセットに対するCOPRAの実装を評価した。これらのベンチマークでは、COPRAはGPT-4のワンショット実行と、証明データに微調整された最先端モデルよりも、迅速に正しい証明を見つけることができる。私たちのコードとデータはhttps://github.com/trishullab/copraで入手できます。

関連論文リスト

Effective Instruction Parsing Plugin for Complex Logical Query Answering on Knowledge Graphs [51.33342412699939]
知識グラフクエリ埋め込み(KGQE)は、不完全なKGに対する複雑な推論のために、低次元KG空間に一階論理(FOL)クエリを埋め込むことを目的としている。近年の研究では、FOLクエリの論理的セマンティクスをよりよく捉えるために、さまざまな外部情報(エンティティタイプや関係コンテキストなど)を統合している。コードのようなクエリ命令から遅延クエリパターンをキャプチャする効果的なクエリ命令解析(QIPP)を提案する。
論文参考訳（メタデータ） (2024-10-27T03:18:52Z)
Enhancing Legal Case Retrieval via Scaling High-quality Synthetic Query-Candidate Pairs [67.54302101989542]
判例検索は、ある事実記述の参照として類似した事例を提供することを目的としている。既存の作業は主に、長いクエリを使ったケース・ツー・ケースの検索に重点を置いている。データスケールは、既存のデータハングリーニューラルネットワークのトレーニング要件を満たすには不十分である。
論文参考訳（メタデータ） (2024-10-09T06:26:39Z)
Reinforcement Replaces Supervision: Query focused Summarization using Deep Reinforcement Learning [43.123290672073814]
クエリに基づいて文書から要約を生成するシステムを扱う。 Reinforcement Learning (RL) が自然言語生成のための Supervised Learning (SL) の一般化を提供するという知見に触発されて,本課題に RL ベースのアプローチを用いる。我々は、ROUGE、BLEU、Semantic similarityといった様々な報酬信号に基づいて訓練された複数のポリシーグラディエントネットワークを開発する。
論文参考訳（メタデータ） (2023-11-29T10:38:16Z)
Investigating Data Contamination in Modern Benchmarks for Large Language Models [27.479260572913724]
近年の観測は、膨らませたベンチマークスコアとLLMの実際の性能の相違を裏付けている。我々は,オープンソースのLLMとプロプライエタリなLLMの両方に適した2つの手法を提案し,データ汚染について検討した。いくつかの商用LCMは、様々なテストセットに欠けているオプションを驚くほど推測できる。
論文参考訳（メタデータ） (2023-11-16T11:03:04Z)
LlamaRec: Two-Stage Recommendation using Large Language Models for Ranking [10.671747198171136]
ランキングベースレコメンデーション(LlamaRec)のための大規模言語モデルを用いた2段階フレームワークを提案する。特に,ユーザインタラクション履歴に基づいて候補を検索するために,小規模なシーケンシャルレコメンデータを用いる。 LlamaRecは、推奨パフォーマンスと効率の両方において、データセットの優れたパフォーマンスを一貫して達成している。
論文参考訳（メタデータ） (2023-10-25T06:23:48Z)
DQ-LoRe: Dual Queries with Low Rank Approximation Re-ranking for In-Context Learning [66.85379279041128]
そこで本研究では,Dual Queries と Low-rank approximation Re- rank を利用して,文脈内学習のための例を自動選択するフレームワークを提案する。 DQ-LoRe は GPT-4 の自動選択において最先端の手法よりも優れ、92.5% から94.2% まで性能が向上した。
論文参考訳（メタデータ） (2023-10-04T16:44:37Z)
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。本研究では,LLM ベースの証明器 ReProver を開発した。
論文参考訳（メタデータ） (2023-06-27T17:05:32Z)
Improving Code Example Recommendations on Informal Documentation Using BERT and Query-Aware LSH: A Comparative Study [0.0]
私たちの研究の焦点は、議論やソリューションのコーディングによく使われるリソースであるStack Overflowです。コード例を数値ベクトルに変換するために,LLM(Large Language Model)のBERTを適用した。これらの数値表現が作成されると、Locality-Sensitive Hashing (LSH) を用いて近似近傍隣人(ANN)を識別する。本研究では,Random Hyperplane-based (RH) 法よりもQuery-Aware (QA) 法の方が優れた性能を示した。
論文参考訳（メタデータ） (2023-05-04T17:43:19Z)
UnifieR: A Unified Retriever for Large-Scale Retrieval [84.61239936314597]
大規模な検索は、クエリを与えられた巨大なコレクションから関連ドキュメントをリコールすることである。事前学習型言語モデル(PLM)に基づく最近の検索手法は,高密度ベクターあるいはレキシコンに基づくパラダイムに大別することができる。本論文では,高密度ベクトルとレキシコンに基づく検索を2つの表現能力を持つ1つのモデルで統合する学習フレームワークUnifieRを提案する。
論文参考訳（メタデータ） (2022-05-23T11:01:59Z)
Pre-training Is (Almost) All You Need: An Application to Commonsense Reasoning [61.32992639292889]
事前学習されたトランスモデルの微調整は、一般的なNLPタスクを解決するための標準的なアプローチとなっている。そこで本研究では,可視性ランキングタスクをフルテキスト形式でキャストする新たなスコアリング手法を提案する。提案手法は, ランダム再起動にまたがって, より安定した学習段階を提供することを示す。
論文参考訳（メタデータ） (2020-04-29T10:54:40Z)

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

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