論文の概要: Neural Termination Analysis
- arxiv url: http://arxiv.org/abs/2102.03824v1
- Date: Sun, 7 Feb 2021 15:45:30 GMT
- ステータス: 処理完了
- システム内更新日: 2021-02-10 03:07:55.014490
- Title: Neural Termination Analysis
- Title（参考訳）: 神経終末解析
- Authors: Mirco Giacobbe, Daniel Kroening, Julian Parsert
- Abstract要約: ニューラルネットワークをトレーニングしてランキング関数として機能します。
プログラムの状態は、プログラムの実行時に下からバウンドされ、減少する値にマップします。
有効なランキング関数の存在は、プログラムが終了することを証明する。
- 参考スコア（独自算出の注目度）: 9.973499664140158
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We introduce a novel approach to the automated termination analysis of
computer programs: we train neural networks to act as ranking functions.
Ranking functions map program states to values that are bounded from below and
decrease as the program runs. The existence of a valid ranking function proves
that the program terminates. While in the past ranking functions were usually
constructed using static analysis, our method learns them from sampled
executions. We train a neural network so that its output decreases along
execution traces as a ranking function would; then, we use formal reasoning to
verify whether it generalises to all possible executions. We present a custom
loss function for learning lexicographic ranking functions and use
satisfiability modulo theories for verification. Thanks to the ability of
neural networks to generalise well, our method succeeds over a wide variety of
programs. This includes programs that use data structures from standard
libraries. We built a prototype analyser for Java bytecode and show the
efficacy of our method over a standard dataset of benchmarks.
- Abstract（参考訳）: 我々はニューラルネットワークをトレーニングしてランキング関数として機能させるという,コンピュータプログラムの自動終端解析に新たなアプローチを導入する。
ランク付け関数は、プログラムが実行するときに下からバウンドされ減少する値にプログラムをマップする。
有効なランキング関数の存在は、プログラムが終了することを証明する。
過去のランキング関数は通常静的解析を用いて構築されているが,本手法はサンプル実行から学習する。
ニューラルネットワークをトレーニングして、ランキング機能として実行トレースに沿って出力が減少するようにします。次に、すべての実行に一般化するかどうかを形式的な推論で検証します。
辞書ランキング関数を学習し、満足度変調理論を用いて検証するカスタム損失関数を提案する。
ニューラルネットワークをうまく一般化する能力のおかげで、我々の手法は様々なプログラムで成功している。
これには標準ライブラリのデータ構造を使用するプログラムが含まれる。
Javaバイトコード用のプロトタイプアナライザを構築し、ベンチマークの標準データセットに対するメソッドの有効性を示した。
関連論文リスト
- ReasonAgain: Using Extractable Symbolic Programs to Evaluate Mathematical Reasoning [54.70811660561151]
既存の数学データセットは、最終回答または静的例から派生した中間推論ステップを用いて、大規模言語モデル(LLM)の推論能力を評価する。
モデルがプログラムへの様々な入力に対して常に正しい最終回答を生成できる場合、シンボルプログラムを自動評価の手段として利用したいと考えている。
提案手法は, 従来の静的な例と比較して, 精度の低下を観測し, 現状のLLMにおける数学推論の脆弱さを示唆する。
論文 参考訳（メタデータ） (2024-10-24T18:02:37Z) - Neural Algorithmic Reasoning with Causal Regularisation [18.299363749150093]
我々は重要な観察を行う: アルゴリズムが特定の中間計算を同一に実行する多くの異なる入力が存在する。
この洞察により、アルゴリズムの中間軌道が与えられた場合、ターゲットアルゴリズムが全く同じ次の軌道ステップを持つような入力を生成するデータ拡張手順を開発することができる。
我々は、Hint-Relicと呼ばれる結果の手法が、推論器のOOD一般化能力を改善することを証明した。
論文 参考訳（メタデータ） (2023-02-20T19:41:15Z) - Using Graph Neural Networks for Program Termination [0.0]
フォーマルな方法から脱して、マシンラーニングモデルの性質を受け入れるのです。
グラフニューラルネットワークを用いて,プログラムのグラフ表現を利用する。
我々は、これまで他のアプリケーションドメインで使われていた注意とセマンティックセグメンテーションの概念をプログラムに適用する。
論文 参考訳（メタデータ） (2022-07-28T12:16:37Z) - Benchmarking Node Outlier Detection on Graphs [90.29966986023403]
グラフの外れ値検出は、多くのアプリケーションにおいて、新しいが重要な機械学習タスクである。
UNODと呼ばれるグラフに対して、最初の包括的教師なしノード外乱検出ベンチマークを示す。
論文 参考訳（メタデータ） (2022-06-21T01:46:38Z) - Refining neural network predictions using background knowledge [68.35246878394702]
学習システムにおける論理的背景知識を用いて,ラベル付きトレーニングデータの不足を補うことができることを示す。
そこで本研究では,修正された予測を元の予測に近い精度で検出する微分可能精細関数を提案する。
このアルゴリズムは、複雑なSATの公式に対して、非常に少ない繰り返しで最適に洗練され、勾配降下ができない解がしばしば見つかる。
論文 参考訳（メタデータ） (2022-06-10T10:17:59Z) - Towards Neural Functional Program Evaluation [0.5586191108738562]
本稿では,意味論的に等価なプログラムに対して,構文糖を制御できる新しいプログラム生成機構を提案する。
実験によると、神経機能プログラムの評価は驚くほど良く、90%の正確なプログラムマッチスコアを達成している。
論文 参考訳（メタデータ） (2021-12-09T00:20:29Z) - Learnable Graph Matching: Incorporating Graph Partitioning with Deep
Feature Learning for Multiple Object Tracking [58.30147362745852]
フレーム間のデータアソシエーションは、Multiple Object Tracking(MOT)タスクの中核にある。
既存の手法は、主にトラックレットとフレーム内検出の間のコンテキスト情報を無視する。
そこで本研究では,学習可能なグラフマッチング手法を提案する。
論文 参考訳（メタデータ） (2021-03-30T08:58:45Z) - Replacing Rewards with Examples: Example-Based Policy Search via
Recursive Classification [133.20816939521941]
標準的なマルコフ決定プロセス形式では、ユーザーは報酬関数を書き留めてタスクを指定する。
多くのシナリオでは、ユーザーはタスクを単語や数字で記述できないが、タスクが解決された場合の世界がどのように見えるかを簡単に示すことができる。
この観察に動機づけられた制御アルゴリズムは、成功した結果状態の例だけを考慮すれば、成功する結果につながる確率の高い状態を訪問することを目的としている。
論文 参考訳（メタデータ） (2021-03-23T16:19:55Z) - GRAPHSPY: Fused Program Semantic-Level Embedding via Graph Neural
Networks for Dead Store Detection [4.82596017481926]
低オーバーヘッドで不必要なメモリ操作をインテリジェントに識別するための学習精度の高いアプローチを提案する。
プログラムセマンティクスの抽出にいくつかの有意なグラフニューラルネットワークモデルを適用することにより,新しいハイブリッドなプログラム埋め込み手法を提案する。
その結果、我々のモデルは精度の90%を達成でき、最先端ツールのオーバーヘッドの半分程度しか発生しないことがわかった。
論文 参考訳（メタデータ） (2020-11-18T19:17:15Z) - Learning to Execute Programs with Instruction Pointer Attention Graph
Neural Networks [55.98291376393561]
グラフニューラルネットワーク(GNN)は、ソフトウェアエンジニアリングタスクを学習するための強力なツールとして登場した。
リカレントニューラルネットワーク(RNN)は、長いシーケンシャルな推論の連鎖に適しているが、プログラム構造を自然に組み込んでいるわけではない。
本稿では,新しいGNNアーキテクチャ,IPA-GNN(Instruction Pointer Attention Graph Neural Networks)を導入する。
論文 参考訳（メタデータ） (2020-10-23T19:12:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。