論文の概要: Relating Answer Set Programming and Many-sorted Logics for Formal Verification

• arxiv url: http://arxiv.org/abs/2502.09230v1
• Date: Thu, 13 Feb 2025 11:52:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-14 13:44:18.806666
• Title: Relating Answer Set Programming and Many-sorted Logics for Formal Verification
• Title（参考訳）: 形式的検証のための解集合プログラミングと多種論理の関係
• Authors: Zachary Hansen,
• Abstract要約: 私の研究課題は、ASP検証をアクセス可能で日常的なタスクにする意図で、3つの問題に対処することに集中しています。 ASP の代替セマンティクスを,この辺りで多種多様な一階述語論理の論理への変換に基づいて検討した。 これらのセマンティクスは、論理プログラムのモジュラー理解を促進し、基底をバイパスし、自動定理プロバーを使用してプログラムのプロパティを自動検証することを可能にする。
• 参考スコア（独自算出の注目度）: 1.223779595809275
• License:
• Abstract: Answer Set Programming (ASP) is an important logic programming paradigm within the field of Knowledge Representation and Reasoning. As a concise, human-readable, declarative language, ASP is an excellent tool for developing trustworthy (especially, artificially intelligent) software systems. However, formally verifying ASP programs offers some unique challenges, such as 1. a lack of modularity (the meanings of rules are difficult to define in isolation from the enclosing program), 2. the ground-and-solve semantics (the meanings of rules are dependent on the input data with which the program is grounded), and 3. limitations of existing tools. My research agenda has been focused on addressing these three issues with the intention of making ASP verification an accessible, routine task that is regularly performed alongside program development. In this vein, I have investigated alternative semantics for ASP based on translations into the logic of here-and-there and many-sorted first-order logic. These semantics promote a modular understanding of logic programs, bypass grounding, and enable us to use automated theorem provers to automatically verify properties of programs.
• Abstract（参考訳）: Answer Set Programming(ASP)は知識表現と推論の分野における重要な論理プログラミングパラダイムである。 簡潔で可読性の高い宣言型言語であるASPは、信頼できる(特に人工的な)ソフトウェアシステムを開発するための優れたツールです。 しかし、ASPプログラムを正式に検証することは、モジュール性の欠如(囲いプログラムから分離してルールを定義するのが難しい)、基礎と解決の意味論(ルールの意味はプログラムが根拠となる入力データに依存する)、既存のツールの制限など、いくつかのユニークな課題をもたらす。 私の研究課題は、ASPをプログラム開発と一緒に定期的に実行される、アクセス可能で日常的なタスクにすることを目的として、これらの3つの課題に対処することに集中しています。 そこで本研究では,この一階述語論理の論理への翻訳に基づいて,ASPの代替セマンティクスについて検討した。 これらのセマンティクスは、論理プログラムのモジュラー理解を促進し、基底をバイパスし、自動定理プロバーを使用してプログラムのプロパティを自動検証することを可能にする。

関連論文リスト

• Combining Logic with Large Language Models for Automatic Debugging and Repair of ASP Programs [1.0650780147044159]
  FormHeは、ロジックベースのテクニックと大規模言語モデルを組み合わせて、Answer Set Programmingの課題を特定し、修正するツールである。 以上の結果から,FormHeは94%の症例の欠陥を正確に検出し,誤りの58%を修復することに成功した。
  論文  参考訳（メタデータ） (2024-10-28T12:30:48Z)
• Finite Groundings for ASP with Functions: A Journey through Consistency [21.53198582611571]
  関数シンボルによるASPの強化は、基本的な推論問題を極めて決定不能にすることが知られている。 高レベルの不決定性に対する直感を与える縮小を示す。 これらの洞察は、ASP プログラムを "frugal" と "non-proliferous" と特徴づける、よりきめ細かい分析を可能にする。
  論文  参考訳（メタデータ） (2024-05-08T11:50:08Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
  本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。 具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。 コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
  論文  参考訳（メタデータ） (2023-08-29T17:22:39Z)
• Coupling Large Language Models with Logic Programming for Robust and General Reasoning from Text [5.532477732693001]
  大規模言語モデルは, 意味論的に非常に効果的な数ショットとして機能することを示す。 自然言語文を論理形式に変換し、応答集合プログラムの入力として機能する。 本手法は,bAbI, StepGame, CLUTRR, gSCAN など,いくつかのベンチマークにおいて最先端性能を実現する。
  論文  参考訳（メタデータ） (2023-07-15T03:29:59Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。 まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。 我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
  論文  参考訳（メタデータ） (2023-05-22T06:11:15Z)
• Tools and Methodologies for Verifying Answer Set Programs [0.0]
  ASP.NETは強力な宣言型プログラミングパラダイムで、検索と最適化の課題を解決するのによく使われます。 知識表現と推論へのアプローチとして、ASPはその単純さ、簡潔さ、厳密に定義されたセマンティクスから恩恵を受ける。 私の研究は、ASPプロガムの検証をサポートする理論とツールの拡張に関するものです。
  論文  参考訳（メタデータ） (2022-08-05T10:50:21Z)
• Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
  本稿では,関連する入力に対する出力プログラム間の整合性を利用して,スプリアスプログラムの影響を低減することを提案する。 より一貫性のあるフォーマリズムは、一貫性に基づくトレーニングを必要とせずに、モデルパフォーマンスを改善することにつながります。
  論文  参考訳（メタデータ） (2021-07-13T03:48:04Z)
• How could Neural Networks understand Programs? [67.4217527949013]
  ソースコードにnlpプリトレーニング技術を直接適用するか、あるいはtheshelfによってモデルに機能を追加するかで、プログラムをより理解するためのモデルを構築するのは難しい。 本研究では,(1)操作セマンティクスの基本操作とよく一致する表現と(2)環境遷移の情報からなる情報から,モデルが学ぶべき新しいプログラムセマンティクス学習パラダイムを提案する。
  論文  参考訳（メタデータ） (2021-05-10T12:21:42Z)
• A Machine Learning guided Rewriting Approach for ASP Logic Programs [0.0]
  機械学習(ML)に基づいて、書き換えるかどうかを自動決定するアプローチについて説明する。 特に、ASPプログラムと入力事実のセットが与えられた場合、我々のアプローチは、それらの構造特性とドメイン情報を測定する一連の機能に基づいて、入力ルールを書き換えるかどうかと方法を選択する。
  論文  参考訳（メタデータ） (2020-09-22T00:51:13Z)
• The ILASP system for Inductive Learning of Answer Set Programs [79.41112438865386]
  我々のシステムは、通常の規則、選択規則、厳しい制約を含むアンサーセットプログラムを学習する。 まず、ILASPの学習フレームワークとその機能の概要を説明します。 続いて、ILASPシステムの進化を概観する。
  論文  参考訳（メタデータ） (2020-05-02T19:04:12Z)

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

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