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

• arxiv url: http://arxiv.org/abs/2310.04353v1
• Date: Fri, 6 Oct 2023 16:21:22 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-09 15:09:23.334192
• Title: A Language-Agent Approach to Formal Theorem-Proving
• Title（参考訳）: 形式的定理提示に対する言語エージェント的アプローチ
• Authors: Amitayush Thakur, Yeming Wen, Swarat Chaudhuri
• Abstract要約: フォーマルな定理証明への最初の言語エージェントアプローチを示す。 COPRAは,高容量のブラックボックスLCMを,ステートフルなバックトラック検索のポリシーの一部として用いている。 我々は、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 COPRA on the miniF2F benchmark for Lean and a set of Coq tasks from the Compcert project. On these benchmarks, COPRA is significantly better than one-shot invocations of GPT-4, as well as state-of-the-art models fine-tuned on proof data, at finding correct proofs quickly.
• Abstract（参考訳）: 言語エージェントは、コンテキスト内学習で外部環境と対話できる大規模言語モデル(LLM)を使用しており、タスクを制御するための有望なアプローチとして最近登場した。 フォーマルな定理証明への最初の言語エージェントアプローチを示す。 COPRAは,高容量のブラックボックスLCM (GPT-4) をステートフルなバックトラック検索のポリシーの一部として用いる。 検索中、ポリシーは証明戦術を選択し、外部データベースから補題や定義を取得することができる。 各選択した戦術は基礎となる証明フレームワークで実行され、次のポリシー実行のプロンプトを構築するために実行フィードバックが使用される。 検索はまた、選択した情報を履歴から追跡し、幻覚や不要なllmクエリを減らすために利用する。 我々は、LeanのminiF2FベンチマークとCompcertプロジェクトからのCoqタスクセットでCOPRAを評価した。 これらのベンチマークでは、COPRAはGPT-4のワンショット呼び出しよりもはるかに優れており、証明データに精巧に調整された最先端のモデルも素早く正しい証明を見つけることができる。

関連論文リスト

• 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)

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

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