論文の概要: An In-Context Learning Agent for Formal Theorem-Proving

• arxiv url: http://arxiv.org/abs/2310.04353v4
• Date: Thu, 8 Feb 2024 00:32:00 GMT
• ステータス: 処理完了
• システム内更新日: 2024-02-09 18:57:27.660369
• Title: An In-Context Learning Agent for Formal Theorem-Proving
• Title（参考訳）: 形式的定理作成のための文脈内学習エージェント
• Authors: Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, Swarat Chaudhuri
• Abstract要約: 我々は、LeanやCoqのような環境で、形式的定理コンテキストのための即興学習エージェントを提示します。 COPRAは大規模言語モデルに対して、ステートフルなバックトラック検索から戦術的応用を提案することを何度も求めている。 我々はCompCertプロジェクトのMiniF2FベンチマークとCoqタスクセットに対するCOPRAの実装を評価した。
• 参考スコア（独自算出の注目度）: 11.433505167967983
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present an in-context learning agent for formal theorem-proving in environments like Lean and Coq. Current state-of-the-art models for the problem are finetuned on environment-specific proof data. By contrast, our approach, called COPRA, repeatedly asks a high-capacity, general-purpose large language model (GPT-4) to propose tactic applications from within a stateful backtracking search. Proposed tactics are executed in the underlying proof environment. Feedback from the execution is used to build the prompt for the next model query, along with selected information from the search history and lemmas retrieved from an external database. 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 few-shot invocations of GPT-4. It also compares favorably against finetuning-based approaches, outperforming REPROVER, a state-of-the-art finetuned approach for Lean, in terms of the pass@1 metric. Our code and data are available at https://github.com/trishullab/copra.
• Abstract（参考訳）: リーンやCoqのような環境での形式的定理証明のためのコンテキスト内学習エージェントを提案する。 この問題の現在の最先端モデルは、環境固有の証明データに基づいて微調整されている。 対照的に,本手法はCOPRAと呼ばれ,高能率汎用大言語モデル (GPT-4) を用いて,ステートフルなバックトラック探索から戦術的応用を提案する。 提案手法は基礎となる証明環境において実行される。 実行からのフィードバックは、検索履歴と外部データベースから取得したレムマから選択された情報とともに、次のモデルクエリのプロンプトを構築するために使用される。 我々はCompCertプロジェクトのMiniF2FベンチマークとCoqタスクセットに対するCOPRAの実装を評価した。 これらのベンチマークでは、COPRAはGPT-4の数発の呼び出しを著しく上回っている。 また、pass@1メトリックの観点から、リーンの最先端の微調整アプローチであるREPROVERよりも優れた微調整ベースのアプローチも好適に比較しています。 私たちのコードとデータは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)

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

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