論文の概要: Lyra: Orchestrating Dual Correction in Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2309.15806v4
• Date: Sat, 24 Aug 2024 12:01:30 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-28 01:07:17.574899
• Title: Lyra: Orchestrating Dual Correction in Automated Theorem Proving
• Title（参考訳）: Lyra: 自動定理証明における二重補正のオーケストレーション
• Authors: Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, Yu Li,
• Abstract要約: Lyraは新しいフレームワークで、ツール補正とConjecture Correctionという2つの異なる補正メカニズムを採用している。 ツール補正は幻覚の緩和に寄与し、それによって証明の全体的な精度が向上する。 Conjecture Correctionは命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。
• 参考スコア（独自算出の注目度）: 63.115422781158934
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) present an intriguing avenue for exploration in the field of formal theorem proving. Nevertheless, their full potential, particularly concerning the mitigation of hallucinations and refinement through prover error messages, remains an area that has yet to be thoroughly investigated. To enhance the effectiveness of LLMs in the field, we introduce the Lyra, a new framework that employs two distinct correction mechanisms: Tool Correction (TC) and Conjecture Correction (CC). To implement Tool Correction in the post-processing of formal proofs, we leverage prior knowledge to utilize predefined prover tools (e.g., Sledgehammer) for guiding the replacement of incorrect tools. Tool Correction significantly contributes to mitigating hallucinations, thereby improving the overall accuracy of the proof. In addition, we introduce Conjecture Correction, an error feedback mechanism designed to interact with prover to refine formal proof conjectures with prover error messages. Compared to the previous refinement framework, the proposed Conjecture Correction refines generation with instruction but does not collect paired (generation, error & refinement) prompts. Our method has achieved state-of-the-art (SOTA) performance on both miniF2F validation (48.0% -> 55.3%) and test (45.5% -> 51.2%). We also present 3 IMO problems solved by Lyra. We believe Tool Correction (post-process for hallucination mitigation) and Conjecture Correction (subgoal adjustment from interaction with environment) could provide a promising avenue for future research in this field.
• Abstract（参考訳）: 大言語モデル (LLMs) は、公式な定理証明の分野における探索の興味深い道を示す。 しかし、その可能性、特に幻覚の緩和と証明エラーメッセージによる改善については、まだ徹底的に研究されていない領域である。 LLMの有効性を高めるために,ツール補正(TC)とコンジェクチュア補正(CC)の2つの異なる補正機構を取り入れた新しいフレームワークであるLyraを導入する。 形式的証明の後処理にツール補正を実装するために,事前に定義された証明ツール(例えばSledgehammer)を用いて,不正なツールの置き換えを誘導する。 ツール補正は幻覚の緩和に大きく寄与し、それによって証明の全体的な精度が向上する。 さらに,証明者と対話し,形式的証明予想を証明者エラーメッセージで洗練するエラーフィードバック機構であるConjecture Correctionを導入する。 従来の改良フレームワークと比較して、提案されたConjecture Correctionは命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。 提案手法は, MiniF2F 検証 (48.0% -> 55.3%) とテスト (45.5% -> 51.2%) の両方で最先端 (SOTA) 性能を達成した。 また、Lyraによって解決された3つのIMO問題を提示する。 ツール補正(幻覚の緩和プロセス)とコンジェクチュア補正(環境との相互作用による副次的な調整)が今後の研究の道筋となると信じている。

関連論文リスト

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• A Coin Has Two Sides: A Novel Detector-Corrector Framework for Chinese Spelling Correction [79.52464132360618]
  中国語のSpelling Correction(CSC)は、自然言語処理(NLP)の基本課題である。 本稿では,エラー検出・相関器の枠組みに基づく新しい手法を提案する。 我々の検出器は2つのエラー検出結果を得るように設計されており、それぞれ高精度とリコールが特徴である。
  論文  参考訳（メタデータ） (2024-09-06T09:26:45Z)
• Small Language Models Need Strong Verifiers to Self-Correct Reasoning [69.94251699982388]
  大規模言語モデル(LLM)の推論性能を高めるための有望なソリューションとして自己補正が登場した。 この研究は、小さい(=13B)言語モデル(LM)が、より強いLMから最小の入力で推論タスクを自己補正できるかどうかを考察する。
  論文  参考訳（メタデータ） (2024-04-26T03:41:28Z)
• GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
  GenAudit - 文書基底タスクの事実チェック LLM 応答を支援するためのツール。 これらのタスクを実行するためにモデルをトレーニングし、ユーザに対して推奨の編集とエビデンスを示すインタラクティブインターフェースを設計します。 システムによってほとんどのエラーがフラグ付けされていることを保証するため,精度への影響を最小限に抑えつつエラーリコールを増大させる手法を提案する。
  論文  参考訳（メタデータ） (2024-02-19T21:45:55Z)
• Converge to the Truth: Factual Error Correction via Iterative Constrained Editing [30.740281040892086]
  最小限の編集で事実誤り訂正(FEC)を行う新しい手法であるVENCEを提案する。 VENCEは、FEC問題を目標密度関数に対する反復サンプリング編集動作として定式化する。 公開データセットでの実験では、VENCEは以前の最遠距離で監督された手法よりもよく測定されたSARIの基準を5.3(または11.8%の相対的な改善)改善している。
  論文  参考訳（メタデータ） (2022-11-22T10:03:13Z)
• Factual Error Correction for Abstractive Summaries Using Entity Retrieval [57.01193722520597]
  本稿では,エンティティ検索後処理に基づく効率的な事実誤り訂正システムRFECを提案する。 RFECは、原文と対象要約とを比較して、原文から証拠文を検索する。 次に、RFECは、エビデンス文を考慮し、要約中のエンティティレベルのエラーを検出し、エビデンス文から正確なエンティティに置換する。
  論文  参考訳（メタデータ） (2022-04-18T11:35:02Z)
• Evidence-based Factual Error Correction [18.52583883901634]
  本稿では,事実誤り訂正の課題を紹介する。 これは、反論されるか、証拠によって部分的にのみ支持される文章を訂正するメカニズムを提供する。
  論文  参考訳（メタデータ） (2021-06-02T11:00:17Z)
• Factual Error Correction of Claims [18.52583883901634]
  本稿では,事実誤り訂正の課題を紹介する。 誤情報を含む文章を修正するメカニズムを提供します。 これは、すでに証拠によって部分的に支持されている主張に固有の説明として機能する。
  論文  参考訳（メタデータ） (2020-12-31T18:11:26Z)
• Error correction and extraction in request dialogs [12.137183622356197]
  Componentは、ユーザの2つの最後の発話を取得し、最後の発話が2番目の最後の発話の誤り訂正であるかどうかを検出する。 そして、最後の発話における誤差補正に従って第2の最終発話を補正し、抽出した再並列及び補修エンティティのペアを出力する。 1つの誤り訂正検出と1つの誤り訂正アプローチをパイプラインに組み合わせたり、エラー訂正アプローチをトレーニングしたり、エンドツーエンドで2つのコンポーネントを避けることができる。
  論文  参考訳（メタデータ） (2020-04-08T20:49:10Z)

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

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