Fugu-MT 論文翻訳(概要): Verification of Locally Tight Programs

論文の概要: Verification of Locally Tight Programs

arxiv url: http://arxiv.org/abs/2204.10789v1
Date: Mon, 18 Apr 2022 23:22:54 GMT
ステータス: 処理完了
システム内更新日: 2022-05-01 09:28:15.161778
Title: Verification of Locally Tight Programs
Title（参考訳）: 局所的タイトプログラムの検証
Authors: Jorge Fandinno, Vladimir Lifschitz
Abstract要約: ANTHEMは、応答セットグラウンドGRINGOの入力言語におけるタイトなプログラムの正しさを検証するために使用できる証明アシスタントである。
参考スコア（独自算出の注目度）: 7.513733974830771
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: ANTHEM is a proof assistant that can be used for verifying the correctness of tight programs in the input language of the answer set grounder GRINGO with respect to specifications expressed by first-order formulas. We define the concept of a locally tight program and prove that the verification process used by ANTHEM is applicable in this more general setting. Unlike tightness, the local tightness condition allows some forms of recursion. In particular, some programs describing effects of actions are locally tight. Under consideration for publication in Theory and Practice of Logic Programming
Abstract（参考訳）: ANTHEMは、一階式で表される仕様に関して、回答セットグラウンドGRINGOの入力言語におけるタイトなプログラムの正しさを検証するために使用できる証明アシスタントである。本稿では,局所的に厳密なプログラムの概念を定義し,ANTHEMが使用する検証プロセスがより一般的な設定で適用可能であることを示す。タイトネスとは異なり、局所的タイトネス条件はいくつかの再帰を許容する。特に、行動の効果を記述するプログラムは局所的に厳密である。論理プログラミングの理論と実践における出版の考察

関連論文リスト

Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
論文参考訳（メタデータ） (2023-12-07T17:51:43Z)
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)
Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis [0.0]
最適化されたサブプログラムが元のサブプログラムを置き換えることができるかどうかを自動的に検証できるツールを持つことが望ましい。そのため、翻訳ツールのアンセムが開発された。 2つのプログラムが強い同値であることを検証するために、古典論理のための自動定理証明器と併用することができる。
論文参考訳（メタデータ） (2023-10-11T08:19:22Z)
Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文参考訳（メタデータ） (2023-09-25T15:42:18Z)
Natural Language to Code Translation with Execution [82.52142893010563]
実行結果-プログラム選択のための最小ベイズリスク復号化。そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
論文参考訳（メタデータ） (2022-04-25T06:06:08Z)
Thirty years of Epistemic Specifications [8.339560855135575]
我々は、主観的リテラルと呼ばれるモーダル構造を持つ安定モデルセマンティクスの下で、解法論理プログラムを拡張した。主観的リテラルを用いることで、プログラムのすべての安定モデルで正規リテラルが真かどうかを確認することができる。形式的な意味論によって言語の基礎となる直観を捉えようとするいくつかの試みが与えられた。
論文参考訳（メタデータ） (2021-08-17T15:03:10Z)
Non-ground Abductive Logic Programming with Probabilistic Integrity Constraints [2.624902795082451]
本稿では,変数の確率的推論に対処する,よりリッチな論理言語について考察する。まず, 分配セマンティックスに基づいて, 全体としての帰納的言語とその意味を提示する。次に,前述したものを拡張して得られた証明手順を導入し,その健全性と完全性を証明する。
論文参考訳（メタデータ） (2021-08-06T10:22:12Z)
Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
本稿では,関連する入力に対する出力プログラム間の整合性を利用して,スプリアスプログラムの影響を低減することを提案する。より一貫性のあるフォーマリズムは、一貫性に基づくトレーニングを必要とせずに、モデルパフォーマンスを改善することにつながります。
論文参考訳（メタデータ） (2021-07-13T03:48:04Z)
Latent Programmer: Discrete Latent Codes for Program Synthesis [56.37993487589351]
プログラム合成や文書要約などの多くのシーケンス学習タスクにおいて、重要な問題は出力シーケンスの広い空間を探索することである。本稿では,検索対象とする出力の表現を学習することを提案する。本稿では,まず入力/出力サンプルから離散潜在コードを予測するプログラム合成手法であるemphLatent Programmerを紹介し,そのプログラムを対象言語で生成する。
論文参考訳（メタデータ） (2020-12-01T10:11:35Z)
Verifying Tight Logic Programs with anthem and Vampire [7.804960968120875]
プログラム完了の定義を、ASPのグルーダーグリンゴの入力言語のサブセットで入力と出力を持つプログラムに拡張する。本稿では,この文脈における安定モデルと完成度の関係について検討し,2つのソフトウェアツールを用いた予備実験について述べる。
論文参考訳（メタデータ） (2020-08-05T10:01:33Z)

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