論文の概要: VEL: A Formally Verified Reasoner for OWL2 EL Profile

• arxiv url: http://arxiv.org/abs/2412.08739v1
• Date: Wed, 11 Dec 2024 19:17:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-13 13:31:04.344172
• Title: VEL: A Formally Verified Reasoner for OWL2 EL Profile
• Title（参考訳）: VEL:OWL2 ELプロファイルのための形式的に検証された推論器
• Authors: Atalay Mert Ileri, Nalen Rangarajan, Jack Cannell, Hande McGinty,
• Abstract要約: VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。 本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the reliability of deductive reasoning within these systems remains challenging, as evidenced by inconsistencies among popular reasoners in recent competitions. This evidence underscores the limitations of current testing-based methodologies, particularly in high-stakes domains such as healthcare. To mitigate these issues, in this paper, we have developed VEL, a formally verified EL++ reasoner equipped with machine-checkable correctness proofs that ensure the validity of outputs across all possible inputs. This formalization, based on the algorithm of Baader et al., has been transformed into executable OCaml code using the Coq proof assistant's extraction capabilities. Our formalization revealed several errors in the original completeness proofs, which led to changes to the algorithm to ensure its completeness. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.
• Abstract（参考訳）: 過去20年間、Web Ontology Language(OWL)は、オントロジーと知識グラフの開発を推進し、データのセマンティックな統合を強化する構造化されたフレームワークを提供してきた。 しかし、近年の競争における人気推論者の不整合が証明されているように、これらのシステム内での帰納的推論の信頼性は依然として困難である。 この証拠は、特に医療のような高度な領域において、現在のテストベースの方法論の限界を浮き彫りにする。 これらの問題を緩和するため,本論文では,マシンチェック可能な正当性証明を具備した検証済みのEL++推論器であるVELを開発した。 この形式化は、Baaderらによるアルゴリズムに基づいて、Coq証明アシスタントの抽出機能を使用して実行可能なOCamlコードに変換されている。 我々の定式化は、元の完全性証明におけるいくつかの誤りを明らかにし、その完全性を保証するためにアルゴリズムを変更した。 本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。

関連論文リスト

• From Scientific Texts to Verifiable Code: Automating the Process with Transformers [2.536225150399618]
  トランスフォーマーは 研究論文を読めます 正式な証明を持つアルゴリズムを 提案し これらの証明を 検証可能なコードに翻訳します このアプローチは形式的検証の障壁を大幅に減らすことができると我々は主張する。
  論文  参考訳（メタデータ） (2025-01-09T14:03:35Z)
• 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)
• Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
  満足度に基づく自動推論は、ソフトウェア工学において複雑なソフトウェアを検証するのに成功している。 我々は、FOL*不満足な結果の正しさを検証するという課題に取り組む。 我々は,不満足の原因を説明するために,証明に基づく診断法を開発した。
  論文  参考訳（メタデータ） (2024-09-13T22:25:58Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Lyra: Orchestrating Dual Correction in Automated Theorem Proving [63.115422781158934]
  Lyraは新しいフレームワークで、ツール補正とConjecture Correctionという2つの異なる補正メカニズムを採用している。 ツール補正は幻覚の緩和に寄与し、それによって証明の全体的な精度が向上する。 Conjecture Correctionは命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。
  論文  参考訳（メタデータ） (2023-09-27T17:29:41Z)
• Verify-and-Edit: A Knowledge-Enhanced Chain-of-Thought Framework [26.7264686036634]
  大規模言語モデル(LLM)がNLPの標準となり、生成および推論タスクのパフォーマンスが向上した。 最も致命的な欠点の1つは、事実の正しさの欠如である。 非現実的なテキストを生成することは、パフォーマンスを低下させるだけでなく、アプリケーションの信頼性と妥当性を低下させる。
  論文  参考訳（メタデータ） (2023-05-05T03:49:14Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  本研究は,NFに基づく多次元条件(後)密度推定器の検証診断を容易にすることを提案する。 また、局所的な一貫性の結果に基づいた理論的保証も提供する。 この作業は、より良い特定モデルの設計を支援したり、新しいSBIアルゴリズムの開発を促進するのに役立つだろう。
  論文  参考訳（メタデータ） (2022-11-17T15:48:06Z)
• A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm [9.349616752756024]
  そこで我々はShorの素因数分解アルゴリズムのエンド・ツー・エンド実装を初めて公式に認定した。 私たちのフレームワークを活用することで、ヒューマンエラーの影響を著しく低減できます。
  論文  参考訳（メタデータ） (2022-04-14T17:02:34Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)
• Understanding the QuickXPlain Algorithm: Simple Explanation and Formal Proof [0.0]
  本稿では,Ulrich Junker の QuickXPlain アルゴリズムの正当性を示す。 他のアルゴリズムを証明するためのガイダンスとして使用できる。 また、QuickXPlainによって計算された結果に依存するシステムの"ギャップレス"な正しさを提供する可能性も提供する。
  論文  参考訳（メタデータ） (2020-01-07T01:37:41Z)

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

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