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

• arxiv url: http://arxiv.org/abs/2109.10476v4
• Date: Sun, 9 Jul 2023 02:22:20 GMT
• ステータス: 処理完了
• システム内更新日: 2023-07-11 23:06:01.588190
• Title: Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules
• Title（参考訳）: 書き直し規則による線形プログラム間の等価性を示す自己教師付き学習
• Authors: Steve Kommrusch, Martin Monperrus and Louis-No\"el Pouchet
• Abstract要約: 2つのプログラムは、1つのプログラムをもう1つのプログラムに書き換える、書き換え規則の一連の適用が存在する場合と同値である。 本稿では,プログラムペア間の等価性の証明を生成するために,トランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。 我々のシステムであるS4Eqは、1万対の等価プログラムをキュレートしたデータセット上で97%の証明成功を達成した。
• 参考スコア（独自算出の注目度）: 9.1570563482476
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We target the problem of automatically synthesizing proofs of semantic equivalence between two programs made of sequences of statements. We represent programs using abstract syntax trees (AST), where a given set of semantics-preserving rewrite rules can be applied on a specific AST pattern to generate a transformed and semantically equivalent program. In our system, two programs are equivalent if there exists a sequence of application of these rewrite rules that leads to rewriting one program into the other. We propose a neural network architecture based on a transformer model to generate proofs of equivalence between program pairs. The system outputs a sequence of rewrites, and the validity of the sequence is simply checked by verifying it can be applied. If no valid sequence is produced by the neural network, the system reports the programs as non-equivalent, ensuring by design no programs may be incorrectly reported as equivalent. Our system is fully implemented for one single grammar which can represent straight-line programs with function calls and multiple types. To efficiently train the system to generate such sequences, we develop an original incremental training technique, named self-supervised sample selection. We extensively study the effectiveness of this novel training approach on proofs of increasing complexity and length. Our system, S4Eq, achieves 97% proof success on a curated dataset of 10,000 pairs of equivalent programs.
• Abstract（参考訳）: 文列からなる2つのプログラム間の意味同値性の証明を自動合成する問題を対象とする。 抽象構文木(AST)を用いてプログラムを表現し、特定のASTパターンに特定のセマンティクス保存規則を適用することで、変換され、意味的に等価なプログラムを生成する。 このシステムでは、2つのプログラムが等価であり、この書き換え規則の適用順序が1つのプログラムをもう1つのプログラムに書き換える結果となる場合である。 本稿では,プログラムペア間の等価性の証明を生成するトランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。 システムは書き直しのシーケンスを出力し、そのシーケンスの妥当性は、適用可能な検証によって単純にチェックされる。 ニューラルネットワークによって有効なシーケンスが生成されない場合、システムはプログラムを等価でないと報告し、設計によってプログラムが不正に等価であると報告されないようにする。 本システムは,関数呼び出しと複数の型を持つ直線プログラムを表現可能な単一文法に対して完全に実装されている。 このようなシーケンスを生成するシステムを効率的にトレーニングするために,自己教師付きサンプル選択という独自のインクリメンタルトレーニング手法を開発した。 本稿では,この新たなトレーニング手法の有効性を,複雑さと長さの増大の証明に広く研究する。 私たちのシステムである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)

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

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