論文の概要: Understanding the QuickXPlain Algorithm: Simple Explanation and Formal
Proof
- arxiv url: http://arxiv.org/abs/2001.01835v3
- Date: Thu, 4 Aug 2022 15:39:00 GMT
- ステータス: 処理完了
- システム内更新日: 2023-01-13 21:10:22.846634
- Title: Understanding the QuickXPlain Algorithm: Simple Explanation and Formal
Proof
- Title（参考訳）: quickxplainアルゴリズムの理解:簡単な説明と形式的証明
- Authors: Patrick Rodler
- Abstract要約: 本稿では,Ulrich Junker の QuickXPlain アルゴリズムの正当性を示す。
他のアルゴリズムを証明するためのガイダンスとして使用できる。
また、QuickXPlainによって計算された結果に依存するシステムの"ギャップレス"な正しさを提供する可能性も提供する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: In his seminal paper of 2004, Ulrich Junker proposed the QuickXPlain
algorithm, which provides a divide-and-conquer computation strategy to find
within a given set an irreducible subset with a particular (monotone) property.
Beside its original application in the domain of constraint satisfaction
problems, the algorithm has since then found widespread adoption in areas as
different as model-based diagnosis, recommender systems, verification, or the
Semantic Web. This popularity is due to the frequent occurrence of the problem
of finding irreducible subsets on the one hand, and to QuickXPlain's general
applicability and favorable computational complexity on the other hand.
However, although (we regularly experience) people are having a hard time
understanding QuickXPlain and seeing why it works correctly, a proof of
correctness of the algorithm has never been published. This is what we account
for in this work, by explaining QuickXPlain in a novel tried and tested way and
by presenting an intelligible formal proof of it. Apart from showing the
correctness of the algorithm and excluding the later detection of errors (proof
and trust effect), the added value of the availability of a formal proof is,
e.g., (i) that the workings of the algorithm often become completely clear only
after studying, verifying and comprehending the proof (didactic effect), (ii)
the shown proof methodology can be used as a guidance for proving other
recursive algorithms (transfer effect), and (iii) the possibility of providing
"gapless" correctness proofs of systems that rely on (results computed by)
QuickXPlain, such as numerous model-based debuggers (completeness effect).
- Abstract（参考訳）: 2004年の論文の中で、ウルリッヒ・ユンカー(Ulrich Junker)は、特定の(単調)特性を持つ既約部分集合を与えられた集合内で見つけるための分割・対数計算戦略を提供するQuickXPlainアルゴリズムを提案した。
制約満足度の問題領域での当初の応用に加えて、このアルゴリズムは、モデルベースの診断、推奨システム、検証、セマンティックwebなど、さまざまな領域で広く採用されている。
この人気は、一方で既約部分集合を見つけるという問題が頻繁に発生し、他方でQuickXPlainの一般適用性と計算複雑性が好まれることによるものである。
しかし、(定期的に経験している)人々はQuickXPlainを理解するのに苦労しており、なぜそれが正しく機能するのかを目の当たりにしています。
これは、QuickXPlainが試行錯誤されテストされた小説で説明し、それの無知な公式な証明を提示することによる、この作品における私たちの説明である。
アルゴリズムの正確性を示すことや、後の誤りの検出(証明と信頼効果)を除外することとは別に、形式的な証明の可用性の付加価値は例えば、加算される。
(i)証明を検証し、理解した後のみ、アルゴリズムの動作が完全に明確になることが多いこと(ダイダクティック効果)
(ii)示された証明方法論は、他の再帰的アルゴリズム(転送効果)を証明するためのガイダンスとして使用できる。
(iii)多数のモデルベースのデバッガ(完全性効果)など、quickxplain(計算結果)に依存するシステムの「ガップレス」な正当性証明を提供する可能性。
関連論文リスト
- 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) - Sample-Efficient Agnostic Boosting [19.15484761265653]
経験的リスク最小化(Empirical Risk Minimization, ERM)は、既知のすべてのブースティングアルゴリズムよりも4次的に標本効率が高いという、不可知的なブースティング手法を超越している。
アルゴリズムの重要な特徴は、一様収束引数のブラックボックスアプリケーションで得られるものよりも厳密な一般化誤差を保証しつつ、複数ラウンドのブースティングのサンプルを再利用する能力を活用することである。
論文 参考訳（メタデータ） (2024-10-31T04:50:29Z) - MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
大規模言語モデル(LLM)は、高い精度で算術語問題を解くことができるが、訓練された言語よりも複雑な問題にどのように一般化するかは、ほとんど分かっていない。
本研究では、任意に複雑な算術証明問題に対する LLM の評価フレームワーク、MathGAP を提案する。
論文 参考訳（メタデータ） (2024-10-17T12:48:14Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10～26。
論文 参考訳（メタデータ） (2024-05-23T10:35:08Z) - Understanding and Mitigating Classification Errors Through Interpretable
Token Patterns [58.91023283103762]
容易に解釈可能な用語でエラーを特徴付けることは、分類器が体系的なエラーを起こす傾向にあるかどうかを洞察する。
正しい予測と誤予測を区別するトークンのパターンを発見することを提案する。
提案手法であるPremiseが実際によく動作することを示す。
論文 参考訳（メタデータ） (2023-11-18T00:24:26Z) - FastDiagP: An Algorithm for Parallelized Direct Diagnosis [64.65251961564606]
FastDiagは、競合を事前に決定せずに診断計算をサポートする典型的な直接診断アルゴリズムである。
本稿では,投機的プログラミングのアイデアに基づく新しいアルゴリズムであるFastDiagPを提案する。
このメカニズムは、高速な回答で一貫性チェックを提供し、アルゴリズムのランタイムパフォーマンスを高めるのに役立つ。
論文 参考訳（メタデータ） (2023-05-11T16:26:23Z) - The Adversary Bound Revisited: From Optimal Query Algorithms to Optimal
Control [0.0]
このノートは"One-Way Ticket to Las Vegas and the Quantum Adversary"という論文を補完している。
私は、Barnum-Saks-Szegedyと同じ視点で、逆境界-普遍アルゴリズムの双対性を異なる形で開発する。
論文 参考訳（メタデータ） (2022-11-29T15:25:45Z) - The Familiarity Hypothesis: Explaining the Behavior of Deep Open Set
Methods [86.39044549664189]
特徴ベクトルデータに対する異常検出アルゴリズムは異常を外れ値として識別するが、外れ値検出はディープラーニングではうまく機能しない。
本論文は, 新規性の有無ではなく, 慣れ親しんだ特徴の欠如を検知しているため, これらの手法が成功するというFamiliarity仮説を提案する。
本論文は,親しみやすさの検出が表現学習の必然的な結果であるかどうかを論じる。
論文 参考訳（メタデータ） (2022-03-04T18:32:58Z) - Part-X: A Family of Stochastic Algorithms for Search-Based Test
Generation with Probabilistic Guarantees [3.9119084077397863]
ファルシフィケーションはサイバー物理システムにおける誤動作を発見するための実用的で効果的な方法であることが証明されている。
ファルシフィケーション法の性能と適用性は常に改善されているにもかかわらず、それらは共通の特徴を共有している。
テスト予算が枯渇したときの誤動作(偽装者)の欠如を保証しない最善策である。
論文 参考訳（メタデータ） (2021-10-20T19:05:00Z) - Improved Algorithms for Agnostic Pool-based Active Classification [20.12178157010804]
プールに依存しない環境でのバイナリ分類のためのアクティブラーニングを検討する。
我々のアルゴリズムは、画像分類データセットにおけるアートアクティブな学習アルゴリズムの状況よりも優れている。
論文 参考訳（メタデータ） (2021-05-13T18:24:30Z) - Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。
ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。
本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
論文 参考訳（メタデータ） (2020-10-07T08:19:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。