論文の概要: On Incorrectness Logic and Kleene Algebra With Top and Tests

• arxiv url: http://arxiv.org/abs/2108.07707v1
• Date: Tue, 17 Aug 2021 15:50:21 GMT
• ステータス: 処理完了
• システム内更新日: 2021-08-18 15:52:03.217071
• Title: On Incorrectness Logic and Kleene Algebra With Top and Tests
• Title（参考訳）: トップとテストによる誤り論理とクリーネ代数について
• Authors: Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
• Abstract要約: トップ要素を持つKATの拡張であるTop and Tests (TopKAT) を用いて、Kleene代数を研究する。 我々は,TopKATがコドメイン演算を表現し,誤り度三重項を表現し,誤り度論理のすべての規則を証明するのに十分であることを示す。
• 参考スコア（独自算出の注目度）: 22.539797604999553
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about \emph{incorrectness}, instead, as embodied by Ohearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.
• Abstract（参考訳）: kleene algebra with tests (kat) はプログラムを推論するための基礎的な方程式のフレームワークであり、プログラム変換やネットワーク、コンパイラの最適化などに応用されている。 コーゼンは論文の中で、KAT が命題ホア論理を仮定することを証明し、KAT の方程式理論を用いてプログラムをプログラムしている間の(部分的な)正しさを推論できることを示した。 本研究では,最近提案された誤り論理の具体例として,kat が \emph{incorrectness} を推論するために提供するサポートについて検討する。 KATは誤り論理を直接表現できないことを示す。 この制限の主な理由は、katがコドメインの概念を明示的に表現できないためであり、これは不正確な三重項を表現するのに必須である。 この問題に対処するため、トップ要素を持つ KAT の拡張である Top and Tests (TopKAT) を用いて、Kleene 代数を研究する。 我々は,TopKATがコドメイン演算を表現し,誤り度三重項を表現し,誤り度論理のすべての規則を証明するのに十分であることを示す。 これは、TopKATの方程式理論を用いて、時のようなプログラムの誤りを推論できることを示している。

関連論文リスト

• Markov Chain of Thought for Efficient Mathematical Reasoning [10.678633785012691]
  多段階の思考の連鎖(CoT)は、推論ステップとタスク固有のアクションの論理構造から恩恵を受ける。 我々は、標準多段階CoTを思考のマルコフ連鎖(MCoT)として概念化する。
  論文  参考訳（メタデータ） (2024-10-23T07:53:29Z)
• Mitigating Misleading Chain-of-Thought Reasoning with Selective Filtering [59.495717939664246]
  大規模言語モデルは、複雑な問題を解くためにチェーン・オブ・ソート(CoT)推論技術を活用することで、顕著な能力を示した。 本稿では,選択フィルタリング推論(SelF-Reasoner)と呼ばれる新しい手法を提案する。 SelF-ReasonerはScienceQA、ECQA、LastLetterタスクに対して、微調整されたT5ベースラインを一貫して改善する。
  論文  参考訳（メタデータ） (2024-03-28T06:28:35Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• Normative Conditional Reasoning as a Fragment of HOL [0.0]
  本稿では(参照に基づく)条件付き規範推論の機械化について論じる。 我々の焦点は条件付き義務のためのAqvistのシステムEとその拡張である。 フレームワークの2つの可能性について検討する。
  論文  参考訳（メタデータ） (2023-08-21T12:47:30Z)
• Invalid Logic, Equivalent Gains: The Bizarreness of Reasoning in Language Model Prompting [9.683505038585988]
  論理的にtextitinvalid Chain-of-Thought (CoT) プロンプトを使用すると、論理的に textitinvalid CoT プロンプトと同じくらいの性能が向上する。 論理的に無効なCoTプロンプトが論理的に有効なプロンプトと同じレベルのパフォーマンスゲインを提供するかどうかをテストする。
  論文  参考訳（メタデータ） (2023-07-20T04:28:53Z)
• Certified Deductive Reasoning with Language Models [37.51289654360009]
  Emphguidesと呼ばれる言語モデルのためのツールのクラスを導入し、ステートとインクリメンタルな制約を使って生成をガイドします。 モデルによってガイドを呼び出すことで、自身の生成を有効なステートメントのセットに制約することができる。 論理的推論のための一般的なシステムが,textscLogicGuideと呼ばれるガイドとしてどのように使用できるかを示す。
  論文  参考訳（メタデータ） (2023-06-06T21:49:00Z)
• GRACE: Discriminator-Guided Chain-of-Thought Reasoning [75.35436025709049]
  本稿では, 正しい推論手順を導出するために, GRACE (CorrectnEss Discriminator) を用いたチェーン・オブ・シークレット・リAsoningを提案する。 GRACEは、正しいステップと間違ったステップに対して対照的な損失で訓練された判別器を採用しており、復号時に次のステップ候補を採点するために使用される。
  論文  参考訳（メタデータ） (2023-05-24T09:16:51Z)
• Towards Understanding Chain-of-Thought Prompting: An Empirical Study of What Matters [82.84696222087396]
  CoT(Chain-of-Thought)の促進により,大規模言語モデル(LLM)の多段階推論能力が劇的に向上する 無効な実演でもCoT推論が可能であることを示す。
  論文  参考訳（メタデータ） (2022-12-20T05:20:54Z)
• Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanations [71.2950434944196]
  ノイズや一貫性のない言語モデルでさえも問題に対する正しい答えを推測するMaieutic Promptingを開発する。 Maieutic Promptingは最先端のプロンプト法よりも最大20%精度が高い。
  論文  参考訳（メタデータ） (2022-05-24T06:36:42Z)
• Verification of Locally Tight Programs [8.005641341294732]
  プログラム完了は、論理プログラムの言語から一階理論の言語への変換である。 この定理の厳密性条件は、より制限の少ない「局所的厳密性」要件に置き換えることができることを示す。 証明アシスタントAnthem-p2pは、局所的に密なプログラム間の等価性を検証できると結論付ける。
  論文  参考訳（メタデータ） (2022-04-18T23:22:54Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。 8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
  論文  参考訳（メタデータ） (2020-06-05T10:56:52Z)

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

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