論文の概要: Lyra: Orchestrating Dual Correction in Automated Theorem Proving
- arxiv url: http://arxiv.org/abs/2309.15806v3
- Date: Sat, 7 Oct 2023 07:54:19 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-13 02:58:44.807095
- 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は命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。
- 参考スコア(独自算出の注目度): 65.48893396979807
- 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) は、公式な定理証明の分野における探索の興味深い道を示す。
それにもかかわらず、幻覚の緩和と証明エラーメッセージによる洗練に関する彼らの潜在能力は、まだ完全には調査されていない領域である。
この分野におけるllmsの有効性を高めるために,ツール補正(tc)と推測補正(cc)の2つの異なる補正機構を用いる新しいフレームワークであるlyraを紹介する。
形式的証明の後処理にツール補正を実装するために、事前の知識を活用して、事前定義された証明ツール(例えば、Sledgehammer)を使って不正なツールの置き換えを導く。
ツール補正は幻覚の緩和に大きく寄与し、証明の全体的な精度を向上させる。
さらに,証明者と対話し,形式的証明予想を証明者エラーメッセージで洗練するエラーフィードバック機構であるConjecture Correctionを導入する。
従来の改良フレームワークと比較して、提案手法は命令による生成を洗練するが、ペア(生成、エラー、改良)プロンプトを収集しない。
提案手法は, MiniF2F 検証 (48.0% -> 55.3%) とテスト (45.5% -> 51.2%) の両方で最先端 (SOTA) 性能を達成した。
また,lyra が解いた3つの imo 問題についても述べる。
ツール補正(幻覚の緩和プロセス)とコンジェクチュア補正(環境との相互作用による副次的な調整)が今後の研究の道筋となると信じている。
関連論文リスト
- GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [68.82726887802856]
GenAudit - 文書基底タスクの事実チェック LLM 応答を支援するためのツール。
これらのタスクを実行するためにモデルをトレーニングし、ユーザに対して推奨の編集とエビデンスを示すインタラクティブインターフェースを設計します。
システムによってほとんどのエラーがフラグ付けされていることを保証するため,精度への影響を最小限に抑えつつエラーリコールを増大させる手法を提案する。
論文 参考訳(メタデータ) (2024-02-19T21:45:55Z) - V-STaR: Training Verifiers for Self-Taught Reasoners [75.11811592995176]
本稿では,自己改善プロセス中に生成した正解と誤解の両方を利用して検証器を訓練するV-STaRを提案する。
V-STaRは、既存の自己改善と検証アプローチよりも4%から17%の精度で改善されている。
論文 参考訳(メタデータ) (2024-02-09T15:02:56Z) - Parameter-tuning-free data entry error unlearning with adaptive
selective synaptic dampening [51.34904967046097]
本稿では,パラメータチューニングの必要性を排除した選択的シナプス減衰アンラーニング法の拡張を提案する。
本稿では,ResNet18とVision Transformerの未学習タスクにおける適応選択的シナプス減衰(ASSD)の性能を示す。
このアプローチの適用は、サプライチェーン管理などの産業環境において特に魅力的である。
論文 参考訳(メタデータ) (2024-02-06T14:04:31Z) - Diagnosing and Rectifying Fake OOD Invariance: A Restructured Causal
Approach [51.012396632595554]
不変表現学習(IRL)は、不変因果的特徴から環境から切り離されたラベルへの予測を促進する。
最近の理論的結果は、IRLによって回復されたいくつかの因果的特徴は、訓練環境ではドメイン不変のふりをするが、目に見えない領域では失敗する。
本研究では,RS-SCMに関する条件付き相互情報に基づく手法を開発し,その効果を巧みに補正する。
論文 参考訳(メタデータ) (2023-12-15T12:58:05Z) - LLMs cannot find reasoning errors, but can correct them! [0.9674641730446749]
自己補正プロセスを2つのコアコンポーネントに分割する。
BIG-Bench MistakeはChain-of-Thought推論トレースにおける論理的誤りのデータセットである。
出力補正のためのバックトラック手法を提案する。
論文 参考訳(メタデータ) (2023-11-14T20:12:38Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。