論文の概要: Regularization in Spider-Style Strategy Discovery and Schedule Construction
- arxiv url: http://arxiv.org/abs/2403.12869v1
- Date: Tue, 19 Mar 2024 16:12:25 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-20 13:34:19.953483
- Title: Regularization in Spider-Style Strategy Discovery and Schedule Construction
- Title(参考訳): スパイダースタイル戦略発見とスケジュール構築における規則化
- Authors: Filip Bártek, Karel Chvalovský, Martin Suda,
- Abstract要約: 本稿では,ヴァンパイア証明のための大規模実験について報告する。
アンドレイ・ヴォロンコフ(Andrei Voronkov)のシステムスパイダー(Spider)のアイデアに基づいてスケジュールを構築する。
- 参考スコア(独自算出の注目度): 1.6385815610837162
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In this paper, we report on a large-scale experiment with discovering strategies for the Vampire prover, targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Andrei Voronkov's system Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, and establish how well a schedule can be expected to generalize to unseen problems and what factors influence this property.
- Abstract(参考訳): 最高の性能を達成するために、自動定理証明者は、与えられた問題に対して(順次または平行に)試すべき様々な証明戦略のスケジュールに依存することが多い。
本稿では,アンドレイ・ヴォロンコフのシステムスパイダーのアイデアに基づいて,TPTPライブラリのFOFフラグメントをターゲットとした,ヴァンパイア証明のための戦略を発見するための大規模な実験について報告する。
様々な角度からプロセスを調べ、CASCコンペティションの強いヴァンパイアスケジュールを得る難しさ(あるいは容易さ)を議論し、スケジュールがいかにして未確認問題に一般化され、どのような要因がこの特性に影響を及ぼすかを明らかにする。
関連論文リスト
- Parallel Strategies for Best-First Generalized Planning [51.713634067802104]
汎用計画(GP)は、複数の古典的な計画インスタンスを解くことができるアルゴリズムのようなソリューションの自動合成を研究するAIの研究分野である。
現在の進歩の1つはBest-First Generalized Planning (BFGP) の導入である。
本稿では,並列探索手法をBFGPに適用し,性能ギャップを埋める上で重要な要素であることを示す。
論文 参考訳(メタデータ) (2024-07-31T09:50:22Z) - Test-Time Domain Generalization for Face Anti-Spoofing [60.94384914275116]
Face Anti-Spoofing (FAS) は、顔認識システムをプレゼンテーション攻撃から保護するために重要である。
本稿では,テストデータを活用してモデルの一般化性を高める新しいテスト時間領域一般化フレームワークについて紹介する。
テスト時間スタイル投影 (TTSP) とディバーススタイルシフトシミュレーション (DSSS) によって構成された本手法は, 目に見えないデータを領域空間に効果的に投影する。
論文 参考訳(メタデータ) (2024-03-28T11:50:23Z) - The Capacity and Robustness Trade-off: Revisiting the Channel
Independent Strategy for Multivariate Time Series Forecasting [50.48888534815361]
本稿では、Channel Dependent(CD)戦略でトレーニングされたモデルが、Channel Dependent(CD)戦略でトレーニングされたモデルよりも優れていることを示す。
以上の結果から,CD手法は高いキャパシティを持つが,分散ドリフト時系列を正確に予測する堅牢性に欠けることがわかった。
本稿では,CI戦略を超越した正規化(PRReg)による予測残差法(Predict Residuals with Regularization, PRReg)を提案する。
論文 参考訳(メタデータ) (2023-04-11T13:15:33Z) - Consistency Regularization for Deep Face Anti-Spoofing [69.70647782777051]
顔認証システムでは、顔認証(FAS)が重要な役割を担っている。
このエキサイティングな観察によって、異なる視点の特徴整合性を促進することが、FASモデルを促進するための有望な方法かもしれないと推測する。
FASにおけるEPCR(Embeddding-level and Prediction-level Consistency Regularization)とEPCR(Embeddding-level Consistency Regularization)を併用した。
論文 参考訳(メタデータ) (2021-11-24T08:03:48Z) - An Investigation of Replay-based Approaches for Continual Learning [79.0660895390689]
連続学習(CL)は機械学習(ML)の大きな課題であり、破滅的忘れ(CF)を伴わずに連続的に複数のタスクを学習する能力を記述する。
いくつかの解クラスが提案されており、その単純さと堅牢性から、いわゆるリプレイベースのアプローチは非常に有望であるように思われる。
連続学習におけるリプレイに基づくアプローチを実証的に検討し,応用の可能性を評価する。
論文 参考訳(メタデータ) (2021-08-15T15:05:02Z) - Variance Reduction in Training Forecasting Models with Subgroup Sampling [34.941630385114216]
一般的に用いられる勾配(例)の予測モデルを示す。
sgd) 大きなばらつきがあり、長時間のトレーニングが必要となる。
この問題を軽減するために,サブグループサンプリングというサンプリング戦略を提案する。
SCottは勾配と壁面時計の両方の目標に対してより高速に収束することを示す。
論文 参考訳(メタデータ) (2021-03-02T22:23:27Z) - Grid Tagging Scheme for Aspect-oriented Fine-grained Opinion Extraction [34.698208867292394]
本稿では,AFOEタスクを1つの統一グリッドタギングタスクのみでエンドツーエンドに処理するための新しいタグ付け方式であるGrid Tagging Scheme(GTS)を提案する。
CNN, BiLSTM, BERTに基づく3つの異なるGTSモデルを実装し, アスペクト指向の意見対抽出と意見三重項抽出データセットの実験を行った。
論文 参考訳(メタデータ) (2020-10-09T15:33:50Z) - Few-shots Parallel Algorithm Portfolio Construction via Co-evolution [31.069132566211675]
一般化、すなわち、システム設計と開発フェーズで利用できない問題のインスタンスを解く能力は、インテリジェントシステムにとって重要な目標である。
本稿では,この課題に対する対策として,CEPSの共進化(Co-Evolution of CEPS)という新たな競争的共進化手法を提案する。
トラベルセールスマン問題(TSP)と同時ピックアップ・デリバリ・アンド・タイムウィンドウ(VRPSPDTW)の2つの具体的なアルゴリズムが提示される。
論文 参考訳(メタデータ) (2020-07-01T14:02:19Z) - Theory-Inspired Path-Regularized Differential Network Architecture
Search [206.93821077400733]
差分アーキテクチャサーチ(DARTS)における高速ネットワーク最適化に対するスキップ接続の影響と,他のタイプの操作に対する競争上の優位性について検討する。
i)操作間の不当競争を避けるために各操作に導入された差分群構造スパース二乗ゲートと,(ii)浅部より収束する深部アーキテクチャの探索を誘導するために用いられる経路深度正規化の2つの主要なモジュールからなる理論に着想を得た経路規則化DARTSを提案する。
論文 参考訳(メタデータ) (2020-06-30T05:28:23Z) - Flexible and Efficient Long-Range Planning Through Curious Exploration [13.260508939271764]
The Curious Sample Planner can realize temporallyextended plan for a wide range of really 3D task。
対照的に、標準的な計画と学習の方法は、多くの場合、これらのタスクを全く解決しなかったり、膨大な数のトレーニングサンプルでのみ実行できなかったりします。
論文 参考訳(メタデータ) (2020-04-22T21:47:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。