Fugu-MT 論文翻訳(概要): An In-Context Learning Agent for Formal Theorem-Proving

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

arxiv url: http://arxiv.org/abs/2310.04353v5
Date: Thu, 8 Aug 2024 04:15:31 GMT
ステータス: 処理完了
システム内更新日: 2024-08-09 21:09:27.622226
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の実装を評価した。
参考スコア（独自算出の注目度）: 10.657173216834668
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の数発の呼び出しを著しく上回っている。また、Pas@1メトリックの観点から、リーンの最先端の微調整アプローチであるReProverよりも優れた微調整ベースのアプローチも好適に比較しています。私たちのコードとデータはhttps://github.com/trishullab/copra.comで公開されています。

関連論文リスト

Scenario-Wise Rec: A Multi-Scenario Recommendation Benchmark [54.93461228053298]
6つの公開データセットと12のベンチマークモデルと、トレーニングと評価パイプラインで構成されるベンチマークである textbfScenario-Wise Rec を紹介します。このベンチマークは、研究者に先行研究から貴重な洞察を提供することを目的としており、新しいモデルの開発を可能にしている。
論文参考訳（メタデータ） (2024-12-23T08:15:34Z)
Large Language Model Can Be a Foundation for Hidden Rationale-Based Retrieval [12.83513794686623]
本稿では,隠れ合理性検索という,より困難なタイプの検索タスクを提案し,検討する。このような問題に対処するためには、命令調整付き大規模言語モデル(LLM)とクロスエンコーダアーキテクチャが妥当な選択である可能性がある。我々は、RaHoReによってこの検索フレームワークを命名し、感情支援会話(ESC)におけるゼロショットおよび微調整性能上の優位性を検証した。
論文参考訳（メタデータ） (2024-12-21T13:19:15Z)
Context-DPO: Aligning Language Models for Context-Faithfulness [80.62221491884353]
本研究では,大規模言語モデルの文脈信頼度を高めるためのアライメント手法を提案する。 ConFiQAから提供されたコンテキストの質問に対する忠実で頑健な応答を活用することで、Context-DPOは直接の選好最適化を通じてLLMを調整します。大規模な実験により、私たちのContext-DPOは、一般的なオープンソースモデルで35%から280%の改善を達成し、コンテキスト忠実性を大幅に改善します。
論文参考訳（メタデータ） (2024-12-18T04:08:18Z)
Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
不確実性定量化は機械学習アプリケーションにおいて重要な要素である。最新のUQベースラインの集合を実装した新しいベンチマークを導入する。我々は、11タスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も効果的なアプローチを特定した。
論文参考訳（メタデータ） (2024-06-21T20:06:31Z)
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)
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)

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

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