論文の概要: 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。

関連論文リスト

• How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization [1.4796543791607086]
  本稿では,最短解法を見つけるための分岐結合アルゴリズムを提案する。 この表現はすべての置換対称性を破り、それによって最先端の対称性の破れを改善する。 本実験により, SATコンペティション2002の事例では30～60%, 小型合成式では25～50%の短縮が可能であることが示唆された。
  論文  参考訳（メタデータ） (2024-11-12T17:31:35Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• SubgoalXL: Subgoal-based Expert Learning for Theorem Proving [37.115856591703974]
  SubgoalXLは、正規の定理証明を強化するために、専門家の学習とサブゴールベースの証明を相乗化する新しいアプローチである。 SubgoalXLは、標準のminiF2Fデータセット上で、Isabelleで56.1%の最先端パフォーマンスを実現する。
  論文  参考訳（メタデータ） (2024-08-20T20:10:53Z)
• 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)
• 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)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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