論文の概要: Proving Theorems Recursively

• arxiv url: http://arxiv.org/abs/2405.14414v1
• Date: Thu, 23 May 2024 10:35:08 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-24 15:44:17.548537
• Title: Proving Theorems Recursively
• Title（参考訳）: 再帰的に定理を証明する
• Authors: Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, Xiaodan Liang,
• Abstract要約: 本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
• 参考スコア（独自算出の注目度）: 80.42431358105482
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in automated theorem proving leverages language models to explore expanded search spaces by step-by-step proof generation. However, such approaches are usually based on short-sighted heuristics (e.g., log probability or value function scores) that potentially lead to suboptimal or even distracting subgoals, preventing us from finding longer proofs. To address this challenge, we propose POETRY (PrOvE Theorems RecursivelY), which proves theorems in a recursive, level-by-level manner in the Isabelle theorem prover. Unlike previous step-by-step methods, POETRY searches for a verifiable sketch of the proof at each level and focuses on solving the current level's theorem or conjecture. Detailed proofs of intermediate conjectures within the sketch are temporarily replaced by a placeholder tactic called sorry, deferring their proofs to subsequent levels. This approach allows the theorem to be tackled incrementally by outlining the overall theorem at the first level and then solving the intermediate conjectures at deeper levels. Experiments are conducted on the miniF2F and PISA datasets and significant performance gains are observed in our POETRY approach over state-of-the-art methods. POETRY on miniF2F achieves an average proving success rate improvement of 5.1%. Moreover, we observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
• Abstract（参考訳）: 自動定理証明の最近の進歩は、言語モデルを利用して、ステップバイステップの証明生成によって拡張された検索空間を探索している。 しかし、このようなアプローチは通常、近視的ヒューリスティック(例えば、ログ確率や値関数のスコア)に基づいており、これは潜在的に最適かサブゴールを逸脱させ、より長い証明を見つけるのを妨げている。 この課題に対処するため、イザベル定理証明器において定理を再帰的かつレベル・バイ・レベルな方法で証明するPOETRY (PrOvE Theorems RecursivelY) を提案する。 従来のステップバイステップ法とは異なり、POETRYは各レベルで証明の検証可能なスケッチを検索し、現在のレベルの定理や予想の解決に焦点を当てている。 スケッチ内の中間予想の詳細な証明は、仮に「残念」と呼ばれるプレースホルダー戦術に置き換えられ、それらの証明をその後のレベルに延期する。 このアプローチにより、定理は第一レベルで全体定理を概説し、さらに深いレベルで中間予想を解くことで漸進的に取り組まれる。 実験は miniF2F と PISA のデータセット上で行われ、PETRY による最先端手法に対する性能向上が観察された。 miniF2F上のPOETRYは平均5.1%の成功率向上を達成する。 また,POETRYが検出した最大証明長は10～26。

関連論文リスト

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving [41.23045212775232]
  探索経路の失敗から学習する訓練モデルの利点を実証する。 既存のオープンソース定理証明データセットにそのような試行錯誤データが欠如しているにもかかわらず、直観論的命題論理定理のデータセットをキュレートする。 比較的短いトライアル・アンド・エラー情報(TrialMaster)で訓練されたモデルと、正しい経路でのみ訓練されたモデルを比較し、前者が低いトライアル探索でより目に見えない定理を解くことを発見した。
  論文  参考訳（メタデータ） (2024-04-10T23:01:45Z)
• A Simple Finite-Time Analysis of TD Learning with Linear Function Approximation [2.44755919161855]
  マルコフサンプリングの下で線形関数近似を用いたTD学習の有限時間収束について検討する。 提案アルゴリズムでは,プロジェクションステップを実際に実行することなく,プロジェクションに基づく解析の単純さを維持することができることを示す。
  論文  参考訳（メタデータ） (2024-03-04T20:40:02Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)
• Investigations into Proof Structures [2.7412662946127755]
  我々は、証明をグローバルな方法で対象として操作し分析するための新しい形式論を導入し、詳述する。 これは、コヒーレントで包括的な形式的な再構築と、ルカシエヴィチによる広く研究されている問題の歴史的証明の分析に例示的に適用される。
  論文  参考訳（メタデータ） (2023-02-14T12:29:39Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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