論文の概要: 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes

• arxiv url: http://arxiv.org/abs/2410.11133v1
• Date: Mon, 14 Oct 2024 23:13:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-16 14:01:23.934916
• Title: 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
• Title（参考訳）: 3D-Prover: 決定的ポイントプロセスによる多様性駆動理論の証明
• Authors: Sean Lamont, Christian Walder, Amir Dezfouli, Paul Montague, Michael Norrish,
• Abstract要約: 自動形式推論における重要な課題は、証明の深さとともに指数関数的に成長する、難解な探索空間である。 セマンティックな多様性と高品質な戦術を活用する新しいフィルタリング機構を提案する。 提案手法は, 総合的な証明率の向上と, 戦術的成功率, 実行時間, 多様性の大幅な向上につながることを示す。
• 参考スコア（独自算出の注目度）: 12.466379414976046
• License:
• Abstract: A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof. This branching is caused by the large number of candidate proof tactics which can be applied to a given goal. Nonetheless, many of these tactics are semantically similar or lead to an execution error, wasting valuable resources in both cases. We address the problem of effectively pruning this search, using only synthetic data generated from previous proof attempts. We first demonstrate that it is possible to generate semantically aware tactic representations which capture the effect on the proving environment, likelihood of success and execution time. We then propose a novel filtering mechanism which leverages these representations to select semantically diverse and high quality tactics, using Determinantal Point Processes. Our approach, 3D-Prover, is designed to be general, and to augment any underlying tactic generator. We demonstrate the effectiveness of 3D-Prover on the miniF2F-valid and miniF2F-test benchmarks by augmenting the ReProver LLM. We show that our approach leads to an increase in the overall proof rate, as well as a significant improvement in the tactic success rate, execution time and diversity.
• Abstract（参考訳）: 自動形式推論における重要な課題は、証明の深さとともに指数関数的に成長する、難解な探索空間である。 この分岐は、与えられた目標に適用可能な多数の候補証明戦術によって引き起こされる。 それにもかかわらず、これらの戦術の多くは意味的に類似しているか、実行エラーを引き起こし、両方のケースで貴重なリソースを浪費している。 従来の証明実験から得られた合成データのみを用いて,この探索を効果的に刈り取る問題に対処する。 まず, 実演環境, 成功可能性, 実行時間に影響を及ぼすような, 意味的に認識された戦術表現を生成できることを実証する。 そこで我々は,これらの表現を活用して,決定的ポイントプロセスを用いて,意味的に多様かつ高品質な戦術を選択する新しいフィルタリング機構を提案する。 我々のアプローチである3D-Proverは汎用的に設計され、基礎となる戦術生成装置を増強する。 ReProver LLMの拡張により, miniF2F-valid および miniF2F-test ベンチマークにおける 3D-Prover の有効性を示す。 提案手法は, 総合的な証明率の向上と, 戦術的成功率, 実行時間, 多様性の大幅な向上につながることを示す。

関連論文リスト

• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• Two Heads are Better than One: Towards Better Adversarial Robustness by Combining Transduction and Rejection [34.0779912244438]
  トランスダクティブ・セッティングにおけるトラマーの分類器・検出技法の新たな応用により、ロバストな一般化のためのサンプル・複雑度が大幅に向上することを示す。 理論的構成は計算的に非効率であるが、選択モデルを学ぶための効率的なトランスダクティブアルゴリズムを特定するのに役立つ。
  論文  参考訳（メタデータ） (2023-05-27T17:06:17Z)
• Versatile Weight Attack via Flipping Limited Bits [68.45224286690932]
  本研究では,展開段階におけるモデルパラメータを変更する新たな攻撃パラダイムについて検討する。 有効性とステルスネスの目標を考慮し、ビットフリップに基づく重み攻撃を行うための一般的な定式化を提供する。 SSA(Single sample attack)とTSA(Singr sample attack)の2例を報告した。
  論文  参考訳（メタデータ） (2022-07-25T03:24:58Z)
• Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
  凸最適化における総和係数法に着想を得て,広範な分岐関数を持つネットワーク上での検証クエリを解析するための新しい手法を提案する。 標準ケース分析に基づく完全探索手順の拡張は、各検索状態で実行される凸手順をDeepSoIに置き換えることによって達成できる。
  論文  参考訳（メタデータ） (2022-03-19T15:05:09Z)
• Diverse Knowledge Distillation for End-to-End Person Search [81.4926655119318]
  人物検索は、画像ギャラリーから特定の人物をローカライズし識別することを目的としている。 最近の手法は2つのグループ、すなわち2段階とエンドツーエンドのアプローチに分類できる。 ボトルネックを解消するために、多様な知識蒸留を備えたシンプルで強力なエンドツーエンドネットワークを提案します。
  論文  参考訳（メタデータ） (2020-12-21T09:04:27Z)
• Weakly Supervised Generative Network for Multiple 3D Human Pose Hypotheses [74.48263583706712]
  単一画像からの3次元ポーズ推定は、欠落した深さのあいまいさに起因する逆問題である。 逆問題に対処するために,弱い教師付き深層生成ネットワークを提案する。
  論文  参考訳（メタデータ） (2020-08-13T09:26:01Z)
• Robust Uncertainty-Aware Multiview Triangulation [20.02647320786556]
  マルチビュー三角測量と不確実性推定のための頑健で効率的な手法を提案する。 まず、中間点法を用いた2視点RANSACを用いた外乱除去方式を提案する。 第二に、初期解と不整集合を精製する異なる局所最適化法を比較する。 第三に、三角点の不確かさを、カメラの数、平均再投影誤差、最大パララックス角の3つの要素の関数としてモデル化する。
  論文  参考訳（メタデータ） (2020-08-04T00:47:42Z)
• TEAM: We Need More Powerful Adversarial Examples for DNNs [6.7943676146532885]
  敵対的な例はディープニューラルネットワーク(DNN)の誤分類につながる可能性がある 本稿では,従来の手法よりも強力な逆例を生成する新しい手法を提案する。 攻撃成功率100% (ASR) の逆例を, より小さい摂動のみで確実に生成することができる。
  論文  参考訳（メタデータ） (2020-07-31T04:11:02Z)
• Deep Spatial Gradient and Temporal Depth Learning for Face Anti-spoofing [61.82466976737915]
  深層学習は、顔の反偽造の最も効果的な方法の1つとして証明されている。 2つの洞察に基づいて,複数フレームからの提示攻撃を検出する新しい手法を提案する。 提案手法は,5つのベンチマークデータセットの最先端結果を実現する。
  論文  参考訳（メタデータ） (2020-03-18T06:11:20Z)

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

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