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

論文の概要: Verification of Locally Tight Programs

arxiv url: http://arxiv.org/abs/2204.10789v2
Date: Thu, 14 Dec 2023 16:24:24 GMT
ステータス: 処理完了
システム内更新日: 2023-12-16 05:41:56.535119
Title: Verification of Locally Tight Programs
Title（参考訳）: 局所的タイトプログラムの検証
Authors: Jorge Fandinno, Vladimir Lifschitz, Nathan Temple
Abstract要約: プログラム完了は、論理プログラムの言語から一階理論の言語への変換である。この定理の厳密性条件は、より制限の少ない「局所的厳密性」要件に置き換えることができることを示す。証明アシスタントAnthem-p2pは、局所的に密なプログラム間の等価性を検証できると結論付ける。
参考スコア（独自算出の注目度）: 8.005641341294732
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Program completion is a translation from the language of logic programs into the language of first-order theories. Its original definition has been extended to programs that include integer arithmetic, accept input, and distinguish between output predicates and auxiliary predicates. For tight programs, that generalization of completion is known to match the stable model semantics, which is the basis of answer set programming. We show that the tightness condition in this theorem can be replaced by a less restrictive "local tightness" requirement. From this fact we conclude that the proof assistant anthem-p2p can be used to verify equivalence between locally tight programs. Under consideration for publication in Theory and Practice of Logic Programming
Abstract（参考訳）: プログラム補完は論理プログラムの言語から一階理論の言語への翻訳である。その本来の定義は整数演算、入力を受け付け、出力述語と補助述語を区別するプログラムにまで拡張されている。タイトなプログラムでは、完備の一般化は、解集合プログラミングの基盤である安定なモデル意味論と一致することが知られている。この定理の厳密性条件は、制限の少ない「局所的厳密性」要件に置き換えることができることを示す。この事実から、証明アシスタント anthem-p2p は局所的タイトなプログラム間の等価性を検証できると結論付ける。論理プログラミングの理論と実践における出版の考察

関連論文リスト

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)

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