Fugu-MT 論文翻訳(概要): An Expressive Trace Logic for Recursive Programs

論文の概要: An Expressive Trace Logic for Recursive Programs

arxiv url: http://arxiv.org/abs/2411.13125v1
Date: Wed, 20 Nov 2024 08:35:29 GMT
ステータス: 翻訳完了
システム内更新日: 2024-11-21 16:12:41.665445
Title: An Expressive Trace Logic for Recursive Programs
Title（参考訳）: 再帰的プログラムのための表現的トレース論理
Authors: Dilian Gurov, Reiner Hähnle,
Abstract要約: 本稿では, 2進状態述語, チョップ, 最小不動点に基づく, トレース式上の表現論理について述べる。プログラムとトレース公式の両方に、直接的なスタイル、完全な構成的、意味論的意味論が備わっている。我々の結果は、プログラミング構造と論理連結体との対応に光を当てた。
参考スコア（独自算出の注目度）: 0.36832029288386137
License:
Abstract: We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points, for precise specification of programs with recursive procedures. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.
Abstract（参考訳）: 本稿では, 2進状態述語, チョップ, 最小固定点に基づくトレース式上の表現論理を, 再帰的手順によるプログラムの正確な仕様化のために提案する。プログラムとトレース公式の両方に、再帰的プログラムの標準SOSと一致する直接型、完全な構成的、意味論的意味論が備わっている。有限トレースプログラム特性を証明するための合成証明計算を設計し、(相対的な)完全性だけでなく音質も証明する。本稿では,各プログラムを意味論的保存トレース公式にマッピングし,その逆もわずかに拡張されたプログラム上の正規プログラムにマッピングできることを示し,その結果,プログラムと公式間のガロア接続を実現する。我々の結果は、プログラミング構造と論理連結体との対応に光を当てた。

関連論文リスト

Origami: (un)folding the abstraction of recursion schemes for program synthesis [0.0]
遺伝的プログラミングは入力仕様を満たす正しいプログラムを探索する。特定の課題はループと再帰を扱う方法であり、終わらないプログラムを避けることである。再帰スキーマは、データ生産と消費の組み合わせを一般化する。
論文参考訳（メタデータ） (2024-02-21T14:17:45Z)
Hierarchical Programmatic Reinforcement Learning via Learning to Compose Programs [58.94569213396991]
プログラムポリシーを作成するための階層型プログラム強化学習フレームワークを提案する。提案するフレームワークは,プログラム作成の学習を通じて,アウト・オブ・ディストリビュータの複雑な動作を記述するプログラムポリシーを作成することができる。 Karel ドメインの実験結果から,提案するフレームワークがベースラインより優れていることが示された。
論文参考訳（メタデータ） (2023-01-30T14:50:46Z)
A Divide-Align-Conquer Strategy for Program Synthesis [8.595181704811889]
本稿では,大規模プログラムの探索を複数の小さなプログラム合成問題に分割する例によって,構成セグメント化がプログラミングに応用可能であることを示す。入力と出力における構成部品の構造的アライメントは、プログラム探索を導くのに使用されるペアワイズ対応に繋がる。
論文参考訳（メタデータ） (2023-01-08T19:10:55Z)
Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
2つのプログラムは、1つのプログラムをもう1つのプログラムに書き換える、書き換え規則の一連の適用が存在する場合と同値である。本稿では,プログラムペア間の等価性の証明を生成するために,トランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。我々のシステムであるS4Eqは、1万対の等価プログラムをキュレートしたデータセット上で97%の証明成功を達成した。
論文参考訳（メタデータ） (2021-09-22T01:37:08Z)
Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
本稿では,関連する入力に対する出力プログラム間の整合性を利用して,スプリアスプログラムの影響を低減することを提案する。より一貫性のあるフォーマリズムは、一貫性に基づくトレーニングを必要とせずに、モデルパフォーマンスを改善することにつながります。
論文参考訳（メタデータ） (2021-07-13T03:48:04Z)
Latent Execution for Neural Program Synthesis Beyond Domain-Specific Languages [97.58968222942173]
入力出力の例からCプログラムを合成する第一歩を踏み出す。特に,部分生成プログラムの実行を近似するために潜在表現を学習するLa Synthを提案する。これらのプログラムのトレーニングにより,Karel と C のプログラム合成における予測性能がさらに向上することを示す。
論文参考訳（メタデータ） (2021-06-29T02:21:32Z)
Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
プログラム合成エンジンにおける部分的なプログラム表現手法について紹介する。モジュラーニューラルネットワークとして実装された近似実行モデルを学ぶ。これらのハイブリッドニューロシンボリック表現は、実行誘導型シンセサイザーがより強力な言語構成を使うことができることを示す。
論文参考訳（メタデータ） (2020-12-23T20:40:18Z)
Sequential composition of propositional logic programs [0.0]
本稿では,非循環プログラムを単一ルールプログラムに分解し,任意のプログラムに対して一般的な分解結果を提供する。プログラムの即時結果演算子は、演算子への明示的な参照を伴わずに最小モデルを計算することができる構成によって表現できることを示す。
論文参考訳（メタデータ） (2020-09-12T11:57:30Z)
Process Discovery for Structured Program Synthesis [70.29027202357385]
プロセスマイニングにおける中核的なタスクは、イベントログデータから正確なプロセスモデルを学ぶことを目的としたプロセス発見である。本稿では,ターゲットプロセスモデルとして(ブロック-)構造化プログラムを直接使用することを提案する。我々は,このような構造化プログラムプロセスモデルの発見に対して,新たなボトムアップ・アグリメティブ・アプローチを開発する。
論文参考訳（メタデータ） (2020-08-13T10:33:10Z)
LogicalFactChecker: Leveraging Logical Operations for Fact Checking with Graph Module Network [111.24773949467567]
ファクトチェックに論理演算を活用するニューラルネットワークアプローチであるLogicalFactCheckerを提案する。大規模なベンチマークデータセットであるTABFACT上での最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2020-04-28T17:04:19Z)
Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model [0.0]
本研究では,2つのプログラム間の等価性の問題を,セマンティクスに則った書き直し規則の集合を一方から他方へ保存する問題として定式化する。そこで我々は,プログラム等価性のための最初のグラフからシーケンスまでのニューラルネットワークシステムを開発した。
論文参考訳（メタデータ） (2020-02-17T06:43:00Z)

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