論文の概要: Self-Supervised Learning to Prove Equivalence Between Programs via Semantics-Preserving Rewrite Rules

• arxiv url: http://arxiv.org/abs/2109.10476v1
• Date: Wed, 22 Sep 2021 01:37:08 GMT
• ステータス: 処理完了
• システム内更新日: 2021-09-23 13:34:46.958443
• Title: Self-Supervised Learning to Prove Equivalence Between Programs via Semantics-Preserving Rewrite Rules
• Title（参考訳）: セマンティックスによるプログラム間の等価性を示す自己教師付き学習
• Authors: Steve Kommrusch, Martin Monperrus and Louis-No\"el Pouchet
• Abstract要約: プログラムペア間の等価性の公理的証明を生成するために,トランスフォーマーに基づくニューラルネットワークアーキテクチャを提案する。 我々はスカラーやベクトルを含む式を生成し、同値性を証明するためにマルチタイプ書き換えルールをサポートする。 我々のシステムであるS4Eqは1万組のプログラムに対して97%の成功を達成し、設計による偽陽性をゼロにする。
• 参考スコア（独自算出の注目度）: 12.966408977398938
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We target the problem of synthesizing proofs of semantic equivalence between two programs made of sequences of statements with complex symbolic expressions. We propose a neural network architecture based on the transformer to generate axiomatic proofs of equivalence between program pairs. We generate expressions which include scalars and vectors and support multi-typed rewrite rules to prove equivalence. For training the system, we develop an original training technique, which we call self-supervised sample selection. This incremental training improves the quality, generalizability and extensibility of the learned model. We study the effectiveness of the system to generate proofs of increasing length, and we demonstrate how transformer models learn to represent complex and verifiable symbolic reasoning. Our system, S4Eq, achieves 97% proof success on 10,000 pairs of programs while ensuring zero false positives by design.
• Abstract（参考訳）: 複雑な記号表現を持つ文列からなる2つのプログラム間の意味同値の証明を合成する問題を対象とする。 プログラムペア間の等価性の公理的証明を生成するために,トランスフォーマーに基づくニューラルネットワークアーキテクチャを提案する。 我々はスカラーやベクトルを含む式を生成し、同値性を証明するためにマルチタイプ書き換えルールをサポートする。 システムをトレーニングするために,自己教師付きサンプル選択と呼ばれる独自のトレーニング手法を開発した。 この漸進的なトレーニングは、学習モデルの品質、一般化可能性、拡張性を改善する。 そこで本研究では,本システムの有効性について検討し,トランスフォーマーモデルが複雑で検証可能な記号的推論を表現できることを示す。 我々のシステムであるS4Eqは1万組のプログラムに対して97%の成功を達成し、設計による偽陽性をゼロにする。

関連論文リスト

• An Expressive Trace Logic for Recursive Programs [0.36832029288386137]
  本稿では, 2進状態述語, チョップ, 最小不動点に基づく, トレース式上の表現論理について述べる。 プログラムとトレース公式の両方に、直接的なスタイル、完全な構成的、意味論的意味論が備わっている。 我々の結果は、プログラミング構造と論理連結体との対応に光を当てた。
  論文  参考訳（メタデータ） (2024-11-20T08:35:29Z)
• GPT is becoming a Turing machine: Here are some ways to program it [16.169056235216576]
  GPT-3モデルはループを含むプログラムを実行するために起動可能であることを示す。 1つのタスクの例をカバーすることさえできないプロンプトが、アルゴリズム的な振る舞いをトリガーできることを示します。
  論文  参考訳（メタデータ） (2023-03-25T00:43:41Z)
• Improved Tree Search for Automatic Program Synthesis [91.3755431537592]
  重要な要素は、有効なプログラムの空間における効率的な探索を可能にすることである。 ここでは2つの大きな異なるDSL上でのアート結果の状態を導くMCTSの変種を提案する。
  論文  参考訳（メタデータ） (2023-03-13T15:09:52Z)
• Hierarchical Phrase-based Sequence-to-Sequence Learning [94.10257313923478]
  本稿では、学習中の帰納バイアスの源として階層的フレーズを取り入れ、推論中の明示的な制約として、標準的なシーケンス・ツー・シーケンス(seq2seq)モデルの柔軟性を維持するニューラルトランスデューサについて述べる。 本手法では,木が原文と対象句を階層的に整列するブラケット文法に基づく識別的導出法と,整列した句を1対1で翻訳するニューラルネットワークセク2セックモデルという2つのモデルを訓練する。
  論文  参考訳（メタデータ） (2022-11-15T05:22:40Z)
• Learning from Self-Sampled Correct and Partially-Correct Programs [96.66452896657991]
  そこで本研究では,モデルが学習中にサンプリングを行い,自己サンプリングされた完全正当プログラムと部分正当プログラムの両方から学習することを提案する。 自己サンプリング型プログラムと部分修正型プログラムを併用することで,学習とサンプリングプロセスのガイドに役立てることができることを示す。 提案手法は,MLEを用いた単一の参照プログラムからの学習と比較して,パス@kの性能を3.1%から12.3%向上させる。
  論文  参考訳（メタデータ） (2022-05-28T03:31:07Z)
• Discovering Non-monotonic Autoregressive Orderings with Variational Inference [67.27561153666211]
  我々は、訓練データから高品質な生成順序を純粋に検出する、教師なし並列化可能な学習装置を開発した。 エンコーダを非因果的注意を持つトランスフォーマーとして実装し、1つのフォワードパスで置換を出力する。 言語モデリングタスクにおける経験的結果から,我々の手法は文脈認識であり,一定の順序と競合する,あるいはより優れた順序を見つけることができる。
  論文  参考訳（メタデータ） (2021-10-27T16:08:09Z)
• Searching for More Efficient Dynamic Programs [61.79535031840558]
  本稿では,プログラム変換の集合,変換プログラムの効率を評価するための単純な指標,およびこの指標を改善するための探索手順について述べる。 実際に、自動検索は初期プログラムの大幅な改善を見出すことができることを示す。
  論文  参考訳（メタデータ） (2021-09-14T20:52:55Z)
• Structured Reordering for Modeling Latent Alignments in Sequence Transduction [86.94309120789396]
  本稿では,分離可能な置換の辺りを正確に推定する効率的な動的プログラミングアルゴリズムを提案する。 結果のSeq2seqモデルは、合成問題やNLPタスクの標準モデルよりも体系的な一般化が優れている。
  論文  参考訳（メタデータ） (2021-06-06T21:53:54Z)
• Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models [0.0]
  プログラム同値性のためのグラフ・ツー・シーケンスニューラルネットワークシステムを開発した。 我々は、リッチな多型線形代数表現言語を用いて、我々のシステムを広範囲に評価する。 我々の機械学習システムは、全ての真正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の正の
  論文  参考訳（メタデータ） (2021-06-01T20:45:42Z)
• Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model [0.0]
  本研究では,2つのプログラム間の等価性の問題を,セマンティクスに則った書き直し規則の集合を一方から他方へ保存する問題として定式化する。 そこで我々は,プログラム等価性のための最初のグラフからシーケンスまでのニューラルネットワークシステムを開発した。
  論文  参考訳（メタデータ） (2020-02-17T06:43:00Z)

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

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