論文の概要: Structure-Preserving Uncertainty Propagation in First-Order Proof Search
- arxiv url: http://arxiv.org/abs/2608.09190v1
- Date: Mon, 10 Aug 2026 07:00:55 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-11 19:16:37.12048
- Title: Structure-Preserving Uncertainty Propagation in First-Order Proof Search
- Title（参考訳）: 1次証明探索における構造保存不確かさ伝播
- Abstract要約: GKは、通常の解像度に基づく証明探索を拡張するクエリ指向の1次証明器である。
これは、等式や関数項を含む非基底節と直接作用する。
本稿では,そのフレームワークに構造保存量レポートを付加する。
- 参考スコア（独自算出の注目度）: 0.2538209532048867
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: GK is a query-directed first-order prover that extends ordinary resolution-based proof search with explicit positive and negative claims, numerical confidence values, and prioritized default rules with exceptions. It works directly with non-ground clauses, including equality and function terms. Candidate proofs are found by bounded first-order proof search; exception conditions of defaults are checked by further bounded searches, recursively when exceptions themselves depend on defaults. This avoids requiring a finite global grounding, while allowing incomplete searches to be reported as such. This paper adds structure-preserving quantitative reporting to that framework. Retained proof histories are used in two calculations. The first reconstructs the uncertain ground premises used by each proof and computes the probability that at least one retained proof is available, without counting shared premises independently. The second resolves positive and negative support at intermediate atoms before that support is propagated through later rules; the same calculation evaluates uncertain exception conditions for individual rule applications. Reports separate positive support, negative support, conflict, and ignorance and identify detected incomplete calculations or fallbacks. The implementation performs bounded reconstruction and dependency traversal after proof search and still requires no global grounding. Analytic examples and independent simulators reproduce the reference calculations on their stated fragments. Comparisons with probabilistic logic, probabilistic ASP, default logic, and goal-directed ASP identify cases of agreement, semantic difference, unsupported translation, and incomplete computation.
- Abstract（参考訳）: GKはクエリ指向の1次証明器で、正と負の明確なクレーム、数値信頼値、例外付きデフォルトルールを優先して、通常の解像度ベースの証明検索を拡張する。
これは、等式や関数項を含む非基底節と直接作用する。
候補証明は有界一階証明サーチによって発見され、デフォルトの例外条件は、さらに有界検索によってチェックされ、例外自体がデフォルトに依存している場合に再帰的にチェックされる。
これにより、有限な大域的な接地を必要とせず、不完全な探索を報告できる。
本稿では,そのフレームワークに構造保存量レポートを付加する。
証明履歴は2つの計算に使われている。
第1は、各証明で使用される不確実な基底前提を再構築し、共有前提を個別にカウントすることなく、少なくとも1つの保持された証明が利用可能である確率を計算する。
2つ目は、後続の規則によって支持が伝播する前に中間原子の正と負の支持を解消し、同じ計算は個々の規則適用に対する不確実な例外条件を評価する。
報告は肯定的な支持、否定的な支持、対立、無知を分離し、検出された不完全な計算やフォールバックを識別する。
この実装は証明探索後に有界再構成と依存性トラバースを行い、大域的な接地はいまだ必要としない。
分析例と独立したシミュレータは、記述されたフラグメントの参照計算を再現する。
確率論理、確率的 ASP、デフォルト論理、目標指向 ASP と比較すると、一致、意味差、サポートなし翻訳、不完全計算のケースが特定できる。
関連論文リスト
- Autoformalizing Argumentative Material Inferences [26.35292656634472]
我々は、ガード補完として議論材料推論のための自己形式化を開発する。
GUARDは、証明された信条を大幅に改善する。
シンボル的ソフトな批判と明示的な仮定層がこれらの利益の大部分を担っていることを示す。
論文 参考訳（メタデータ） (2026-09-15T11:05:26Z) - Compute-Bounded Security Assurance - Coverage, Verification, and Response under Resource Constraints [0.0]
追加の推論計算は、正しく解決されたセキュリティ保証タスクの数を増やすことができる。
我々は、成功、ユニークなカバレッジ、承認された証拠、運用上の保護を分離するリソース制約のあるフレームワークを開発する。
概念的防御アーキテクチャは、証拠分析、判断、運用権限を分離する。
論文 参考訳（メタデータ） (2026-09-07T13:07:55Z) - When benchmark inferences do not compose: Projectibility in AI evaluation [0.0]
AIベンチマークの結果が1ステップで連続的なクレームに達することはめったにない。
評価者はそれをさらなるケースに一般化し、能力の証拠として解釈し、新しいタスクに外挿し、他のシステムやサイトへ輸送する。
保証リンクは保証チェーンを自動的に作らない。
論文 参考訳（メタデータ） (2026-07-28T18:07:04Z) - Before the Action: Benchmarking LLMs on Prospective Hypothesis Discovery [95.44432473367836]
大規模言語モデル(LLM)は、事前に特定された質問に答える能力に優れるが、未解決の未解決段階をナビゲートする能力はほとんど測定されていない。
仮説探索(PHD)を導入し,不確定な証拠から,仮説空間を自律的に構築することをモデルに求める。
本稿では,6つの科学的・分析的領域にわたる988ケースのベンチマークであるHypoArenaと,オープンエンド仮説セットの評価フレームワークであるHypoEvalを紹介する。
論文 参考訳（メタデータ） (2026-07-17T08:56:43Z) - Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification [0.0]
自己構成は、情報フロー検証を2つの回路コピー上の安全性チェックに還元する。
近年のPDRに基づく手法では、複写対称性と大域的クロスコピー等価式を用いて、この重複構造を利用する。
我々はこれらの関係をPDRに公開するために、ガード付き等価述語を導入する。
論文 参考訳（メタデータ） (2026-06-20T14:25:13Z) - Finite Resources False Discovery Rate Control in Structured Hypothesis Spaces [47.16593717985932]
各仮説が有限個のヌル引き数で証明された場合にのみ、偽発見率を制御するための枠組みを提案する。
構造的ミス特定に頑健な2つの決定ルールを提示するが、正確なFDR制御と統計的パワーの間には明確なトレードオフを提供する。
論文 参考訳（メタデータ） (2026-06-13T16:56:52Z) - Finite Certificates for In-Context Determinacy and a Threshold Theory of Emergence in Language Models [0.2864713389096699]
本稿では,文脈条件付き言語モデル行動を検証するためのモデル理論フレームワークを開発する。
有限コンテキスト証明書、ペアセパレータのヒットセット、クエリ教育のディメンション、プロンプト保存基準、スケール制限証人を提供する。
論文 参考訳（メタデータ） (2026-05-30T14:07:58Z) - Exact Structural Abstraction and Tractability Limits [0.0]
正確な正確性は、誘導されたクラス $s sim_R simation' iff MathrmAdm_R(s)$ にのみ依存する。
決定、探索、近似、統計的、ランダム化された地平線、分布保証は全て同じ商-回復問題に還元される。
論文 参考訳（メタデータ） (2026-04-08T17:59:47Z) - Mitigating LLM Hallucinations via Conformal Abstention [70.83870602967625]
我々は,大言語モデルが一般ドメインでの応答をいつ無視すべきかを決定するための,原則化された手順を開発する。
我々は、幻覚率(エラー率)の厳密な理論的保証の恩恵を受けるため、共形予測手法を活用して、禁忌手順を開発する。
実験によって得られた共形禁忌法は, 種々の閉書, オープンドメイン生成質問応答データセットに, 幻覚率を確実に拘束する。
論文 参考訳（メタデータ） (2024-04-04T11:32:03Z) - Prototype-based Aleatoric Uncertainty Quantification for Cross-modal
Retrieval [139.21955930418815]
クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。
しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。
本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
論文 参考訳（メタデータ） (2023-09-29T09:41:19Z) - Sequential Predictive Two-Sample and Independence Testing [114.4130718687858]
逐次的非パラメトリック2サンプルテストと独立テストの問題点について検討する。
私たちは賭けによる(非パラメトリックな)テストの原則に基づいています。
論文 参考訳（メタデータ） (2023-04-29T01:30:33Z) - Nested Counterfactual Identification from Arbitrary Surrogate
Experiments [95.48089725859298]
観測と実験の任意の組み合わせからネスト反事実の同定について検討した。
具体的には、任意のネストされた反事実を非ネストされたものへ写像できる反ファクト的非ネスト定理(英語版)(CUT)を証明する。
論文 参考訳（メタデータ） (2021-07-07T12:51:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。