論文の概要: Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models

• arxiv url: http://arxiv.org/abs/2106.02452v2
• Date: Wed, 9 Jun 2021 02:42:43 GMT
• ステータス: 処理完了
• システム内更新日: 2021-06-13 14:00:24.474528
• Title: Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models
• Title（参考訳）: graph-to-sequenceニューラルモデルを用いた複素表現間の等価性証明
• Authors: Steve Kommrusch, Th\'eo Barollet and Louis-No\"el Pouchet
• Abstract要約: プログラム同値性のためのグラフ・ツー・シーケンスニューラルネットワークシステムを開発した。 我々は、リッチな多型線形代数表現言語を用いて、我々のシステムを広範囲に評価する。 我々の機械学習システムは、全ての真正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We target the problem of provably computing the equivalence between two complex expression trees. To this end, we formalize the problem of equivalence between two such programs as finding a set of semantics-preserving rewrite rules from one into the other, such that after the rewrite the two programs are structurally identical, and therefore trivially equivalent.We then develop a graph-to-sequence neural network system for program equivalence, trained to produce such rewrite sequences from a carefully crafted automatic example generation algorithm. We extensively evaluate our system on a rich multi-type linear algebra expression language, using arbitrary combinations of 100+ graph-rewriting axioms of equivalence. Our machine learning system guarantees correctness for all true negatives, and ensures 0 false positive by design. It outputs via inference a valid proof of equivalence for 93% of the 10,000 equivalent expression pairs isolated for testing, using up to 50-term expressions. In all cases, the validity of the sequence produced and therefore the provable assertion of program equivalence is always computable, in negligible time.
• Abstract（参考訳）: 2つの複雑な表現木間の等価性を確実に計算する問題をターゲットにしている。 そこで我々は,プログラム等価性のためのグラフ・ツー・シーケンス・ニューラルネットシステムを開発し,慎重に構築された自動例生成アルゴリズムを用いて,書き直し規則の集合を一方から他方へ保存し,書き直しが構造的に同一であり,したがって自明に等価であるような2つのプログラム間の等価性の問題について定式化する。 我々は,100以上のグラフ書き換え公理の任意の組み合わせを用いて,リッチな多型線形代数表現言語上でのシステムを広範囲に評価した。 我々の機械学習システムは、すべての真の負の正しさを保証し、設計によって0の偽陽性を保証する。 テスト用に分離された10,000の等価式ペアの93%に対して、最大50の式を使用して、等価性の妥当な証明を推論して出力する。 いずれの場合も、生成されたシーケンスの妥当性、従ってプログラム等価性の証明可能なアサーションは常に計算可能である。

関連論文リスト

• An Expressive Trace Logic for Recursive Programs [0.36832029288386137]
  本稿では, 2進状態述語, チョップ, 最小不動点に基づく, トレース式上の表現論理について述べる。 プログラムとトレース公式の両方に、直接的なスタイル、完全な構成的、意味論的意味論が備わっている。 我々の結果は、プログラミング構造と論理連結体との対応に光を当てた。
  論文  参考訳（メタデータ） (2024-11-20T08:35:29Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。 提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
  論文  参考訳（メタデータ） (2023-06-29T18:35:41Z)
• P(Expression|Grammar): Probability of deriving an algebraic expression with a probabilistic context-free grammar [0.0]
  与えられた文法で表現を導出する確率を計算する問題は一般には決定不可能であることを示す。 次に、線形、有理、双曲表現を生成するための具体的な文法を示す。 これらの文法に対して、任意の精度で正確な確率と効率的な近似を計算するアルゴリズムを設計する。
  論文  参考訳（メタデータ） (2022-12-01T18:36:54Z)
• Hierarchical Phrase-based Sequence-to-Sequence Learning [94.10257313923478]
  本稿では、学習中の帰納バイアスの源として階層的フレーズを取り入れ、推論中の明示的な制約として、標準的なシーケンス・ツー・シーケンス(seq2seq)モデルの柔軟性を維持するニューラルトランスデューサについて述べる。 本手法では,木が原文と対象句を階層的に整列するブラケット文法に基づく識別的導出法と,整列した句を1対1で翻訳するニューラルネットワークセク2セックモデルという2つのモデルを訓練する。
  論文  参考訳（メタデータ） (2022-11-15T05:22:40Z)
• 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)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。 精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。 導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
  論文  参考訳（メタデータ） (2021-07-30T08:27:15Z)
• Contrastive Learning with Adversarial Perturbations for Conditional Text Generation [49.055659008469284]
  seq2seqモデルのコントラスト学習のための正負のサンプルを生成する原則的な方法を提案する。 具体的には、入力シーケンスに小さな摂動を加えることで、条件付き可能性を最小限に抑えるネガティブな例を生成します。 提案手法は,3つのテキスト生成タスクにおけるSeq2seqの一般化を著しく改善することを示す。
  論文  参考訳（メタデータ） (2020-12-14T06:20:27Z)
• Pseudo-Convolutional Policy Gradient for Sequence-to-Sequence Lip-Reading [96.48553941812366]
  唇読解は唇運動系列から音声内容を推測することを目的としている。 seq2seqモデルの伝統的な学習プロセスには2つの問題がある。 本稿では,これら2つの問題に対処するために,PCPGに基づく新しい手法を提案する。
  論文  参考訳（メタデータ） (2020-03-09T09:12:26Z)
• Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model [0.0]
  本研究では,2つのプログラム間の等価性の問題を,セマンティクスに則った書き直し規則の集合を一方から他方へ保存する問題として定式化する。 そこで我々は,プログラム等価性のための最初のグラフからシーケンスまでのニューラルネットワークシステムを開発した。
  論文  参考訳（メタデータ） (2020-02-17T06:43:00Z)
• Consistency of a Recurrent Language Model With Respect to Incomplete Decoding [67.54760086239514]
  逐次言語モデルから無限長のシーケンスを受信する問題について検討する。 不整合に対処する2つの対策として、トップkと核サンプリングの一貫性のある変種と、自己終端の繰り返し言語モデルを提案する。
  論文  参考訳（メタデータ） (2020-02-06T19:56:15Z)

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

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