Fugu-MT 論文翻訳(概要): Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects

論文の概要: Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects

arxiv url: http://arxiv.org/abs/2409.09223v1
Date: Fri, 13 Sep 2024 22:25:58 GMT
ステータス: 処理完了
システム内更新日: 2024-09-17 21:49:17.246935
Title: Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects
Title（参考訳）: 関係対象を持つ一階述語論理の不満足性の証明による診断
Authors: Nick Feng, Lina Marsso, Marsha Chechik,
Abstract要約: 満足度に基づく自動推論は、ソフトウェア工学において複雑なソフトウェアを検証するのに成功している。我々は、FOL*不満足な結果の正しさを検証するという課題に取り組む。我々は,不満足の原因を説明するために,証明に基づく診断法を開発した。
参考スコア（独自算出の注目度）: 1.6727186769396274
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Satisfiability-based automated reasoning is an approach that is being successfully used in software engineering to validate complex software, including for safety-critical systems. Such reasoning underlies many validation activities, from requirements analysis to design consistency to test coverage. While generally effective, the back-end constraint solvers are often complex and inevitably error-prone, which threatens the soundness of their application. Thus, such solvers need to be validated, which includes checking correctness and explaining (un)satisfiability results returned by them. In this work, we consider satisfiability analysis based on First-Order Logic with relational objects (FOL*) which has been shown to be effective for reasoning about time- and data-sensitive early system designs. We tackle the challenge of validating the correctness of FOL* unsatisfiability results and deriving diagnoses to explain the causes of the unsatisfiability. Inspired by the concept of proofs of UNSAT from SAT/SMT solvers, we define a proof format and proof rules to track the solvers' reasoning steps as sequences of derivations towards UNSAT. We also propose an algorithm to verify the correctness of FOL* proofs while filtering unnecessary derivations and develop a proof-based diagnosis to explain the cause of unsatisfiability. We implemented the proposed proof support on top of the state-of-the-art FOL* satisfiability checker to generate proofs of UNSAT and validated our approach by applying the proof-based diagnoses to explain the causes of well-formedness issues of normative requirements of software systems.
Abstract（参考訳）: 満足度に基づく自動推論は、ソフトウェア工学において、安全クリティカルなシステムを含む複雑なソフトウェアを検証するためにうまく使われているアプローチである。このような推論は、要求分析から設計整合性、テストカバレッジに至るまで、多くの検証アクティビティの基礎となります。一般的には効果があるが、バックエンドの制約解決器は複雑で必然的にエラーを起こし、アプリケーションの健全性を脅かす。したがって、正当性を確認し、それらが返した(不満足な)結果を説明することを含む、そのような解法を検証する必要がある。本研究では、時間とデータに敏感な初期システム設計の推論に有効であることが示されているリレーショナルオブジェクト(FOL*)を用いた一階述語論理に基づく満足度解析について考察する。我々は、FOL*不満足な結果の正当性を検証し、不満足の原因を説明するための診断を導き出すという課題に取り組む。 SAT/SMTソルバからのUNSATの証明の概念に触発されて,UNSATへの導出のシーケンスとして解の推論ステップを追跡するための証明形式と証明規則を定義する。また、不必要な導出をフィルタリングしながらFOL*証明の正当性を検証し、不満足の原因を説明するための証明ベース診断を開発するアルゴリズムを提案する。現状のFOL*満足度チェッカー上に提案した証明支援を実装し,UNSATの証明を生成するとともに,その証明に基づく診断を適用し,ソフトウェアシステムの規範的要件の整合性問題の原因を説明することによって,我々のアプローチを検証した。

関連論文リスト

Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability [9.078413809849447]
マルチオブジェクトMaxSAT(MO-MaxSAT)最適化手法のVeriPB証明形式に基づく証明ロギングを提案する。最先端のマルチオブジェクトMaxSATソルバにVeriPBの証明ロギングを実装することで,MO-MaxSATの証明ロギングを合理的なオーバーヘッドで拡張可能であることを実証的に示す。
論文参考訳（メタデータ） (2025-01-29T09:01:26Z)
Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers [4.897782942277061]
本稿では,SSV(Semantic Self-Verification)を導入し,自然言語から解法の形式言語への推論問題を正確に定式化する手法を提案する。 SSVは一貫性に基づくアプローチを用いて、モデルによって生成され、解決者によって検証される具体的なインスタンス化を用いて、問題の強力な抽象的な形式化を生成する。このような*ほぼ確実な推論*は、多くの場合、手動検証の必要性を減らすための新しいアプローチとして提案され、より信頼性が高く自律的なAI推論システムに近づきます。
論文参考訳（メタデータ） (2025-01-28T14:04:49Z)
VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
論文参考訳（メタデータ） (2024-12-11T19:17:28Z)
Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文参考訳（メタデータ） (2024-10-05T05:21:48Z)
SHACL2FOL: An FOL Toolkit for SHACL Decision Problems [0.4895118383237099]
我々は、SHACL文書をFOL文に変換する最初の自動ツールであるSHACL2FOLを紹介する。このツールは、満足度と包含性の2つの静的解析問題に対する解を計算する。また、一連の制約に関してグラフの有効性をテストすることもできる。
論文参考訳（メタデータ） (2024-06-12T09:20:25Z)
Certified MaxSAT Preprocessing [9.717669529984349]
MaxSATはNP-hard最適化問題の解決に有効なアプローチとなっている。 MaxSATソルバの正確性を保証することは、依然として重要な関心事である。そこで本研究では,最新のMaxSATプリプロセッシング手法の正当性を証明するために,擬似ブール検定ロギングをどのように利用できるかを示す。
論文参考訳（メタデータ） (2024-04-26T10:55:06Z)
A Closer Look at the Self-Verification Abilities of Large Language Models in Logical Reasoning [73.77088902676306]
論理的推論の文脈において,大規模言語モデル(LLM)の自己検証能力について詳しく検討する。本研究の主目的は,既存のLCMが誤った推論手順を正確に識別するのに苦労し,自己検証法の有効性を保証できないことにある。
論文参考訳（メタデータ） (2023-11-14T07:13:10Z)
Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。これは、説明に表される論理述語に基づいて、反実仮説を生成する。そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文参考訳（メタデータ） (2022-05-25T03:40:59Z)
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文参考訳（メタデータ） (2022-04-28T17:57:33Z)
Comprehensible Counterfactual Explanation on Kolmogorov-Smirnov Test [56.5373227424117]
我々は,KSテストに失敗するテストデータに対して,反実的説明を生成する問題に対処する。我々は、KSテストに失敗したテストセットの指数的なサブセット数を列挙し、チェックするのを避ける効率的なアルゴリズムMOCHEを開発した。
論文参考訳（メタデータ） (2020-11-01T06:46:01Z)
Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
論文参考訳（メタデータ） (2020-10-07T08:19:48Z)

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

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