論文の概要: 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コンペティションの強いヴァンパイアスケジュールを得る難しさ(あるいは容易さ)を議論し、スケジュールがいかにして未確認問題に一般化され、どのような要因がこの特性に影響を及ぼすかを明らかにする。
関連論文リスト
- On Sequential Fault-Intolerant Process Planning [60.66853798340345]
我々は、逐次的フォールトトレラントプロセス計画(SFIPP)と呼ばれる計画問題を提案し、研究する。
SFIPPは、全ての段階が成功する場合にのみ計画が成功すると判断される多くの連続した多段階決定問題に共通する報酬構造をキャプチャする。
私たちは、異なるアクションを選択して、それぞれのステージで成功の確率を未知にする必要がある設定のために、確実に厳密なオンラインアルゴリズムを設計します。
論文 参考訳(メタデータ) (2025-02-07T15:20:35Z) - Chain-of-Retrieval Augmented Generation [72.06205327186069]
本稿では,o1-like RAGモデルを学習し,最終回答を生成する前に段階的に関連情報を抽出・推論する手法を提案する。
提案手法であるCoRAGは,進化状態に基づいて動的にクエリを再構成する。
論文 参考訳(メタデータ) (2025-01-24T09:12:52Z) - Pruning All-Rounder: Rethinking and Improving Inference Efficiency for Large Vision Language Models [42.124670377223175]
我々は Pruning All-Rounder (PAR) と呼ばれる推論加速のための新しいフレームワークを提案する。
自己教師付き学習方式により,提案手法は性能と効率のバランスが良好である。特にPARは柔軟であり,複数のプルーニングバージョンを提供し,様々なプルーニングシナリオに対処する。
論文 参考訳(メタデータ) (2024-12-09T13:02:35Z) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。