論文の概要: Automated Strategy Invention for Confluence of Term Rewrite Systems

• arxiv url: http://arxiv.org/abs/2411.06409v1
• Date: Sun, 10 Nov 2024 10:08:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-12 14:08:18.915742
• Title: Automated Strategy Invention for Confluence of Term Rewrite Systems
• Title（参考訳）: 項書き換えシステムの収束のための自動戦略発明
• Authors: Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk,
• Abstract要約: 学習誘導型自動合流証明器の開発に機械学習を適用した。 我々の発明した戦略を取り入れた場合、拡張データセットとオリジナルの人為的ベンチマークデータセットCopsの両方で人為的に設計された戦略を上回ります。
• 参考スコア（独自算出の注目度）: 3.662364375995991
• License:
• Abstract: Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system properties, automatic term rewriting tools work in an extensive parameter space. This complexity exceeds human capacity for parameter selection, motivating an investigation into automated strategy invention. In this paper, we focus on confluence, an important property of term rewrite systems, and apply machine learning to develop the first learning-guided automatic confluence prover. Moreover, we randomly generate a large dataset to analyze confluence for term rewrite systems. Our results focus on improving the state-of-the-art automatic confluence prover CSI: When equipped with our invented strategies, it surpasses its human-designed strategies both on the augmented dataset and on the original human-created benchmark dataset Cops, proving/disproving the confluence of several term rewrite systems for which no automated proofs were known before.
• Abstract（参考訳）: 用語の書き換えは、ソフトウェアの検証とコンパイラの最適化において重要な役割を担います。 様々なシステム特性を証明するために数十の高度パラメータ化技術が開発され、自動項書き換えツールは広範なパラメータ空間で機能する。 この複雑さは、パラメータ選択のための人間の能力を超え、自動戦略発明の研究を動機付けている。 本稿では,用語書き換えシステムの重要な特性である合流性に着目し,機械学習を適用して学習誘導型自動合流証明器を開発する。 さらに,項書き換えシステムにおけるコンバレンスを分析するために,大規模データセットをランダムに生成する。 我々の発明した戦略を取り入れた場合、その人間設計戦略を、拡張データセットとオリジナルの人為的ベンチマークデータセットCopsの両方で超越し、自動証明がない複数の項書き換えシステムの合流性を証明/証明します。

関連論文リスト

• Boosting CNN-based Handwriting Recognition Systems with Learnable Relaxation Labeling [48.78361527873024]
  本稿では,2つの異なる手法の強みを組み込んだ手書き文字認識手法を提案する。 本稿では,アルゴリズムの収束を加速し,システム全体の性能を向上させるスペーシフィケーション手法を提案する。
  論文  参考訳（メタデータ） (2024-09-09T15:12:28Z)
• Advancing Cyber Incident Timeline Analysis Through Rule Based AI and Large Language Models [0.0]
  本稿では,ルールベース人工知能(R-BAI)アルゴリズムとLarge Language Models(LLM)を組み合わせた新しいフレームワークGenDFIRを紹介する。
  論文  参考訳（メタデータ） (2024-09-04T09:46:33Z)
• Inference Optimization of Foundation Models on AI Accelerators [68.24450520773688]
  トランスフォーマーアーキテクチャを備えた大規模言語モデル(LLM)を含む強力な基礎モデルは、ジェネレーティブAIの新たな時代を支えている。 モデルパラメータの数が数十億に達すると、実際のシナリオにおける推論コストと高いレイテンシーが排除される。 このチュートリアルでは、AIアクセラレータを用いた補完推論最適化テクニックに関する包括的な議論を行っている。
  論文  参考訳（メタデータ） (2024-07-12T09:24:34Z)
• "I understand why I got this grade": Automatic Short Answer Grading with Feedback [36.74896284581596]
  本稿では,5.8kの学生回答と参照回答と自動短解答(ASAG)タスクに対する質問のデータセットを提案する。 EngSAFデータセットは、複数のエンジニアリングドメインのさまざまな主題、質問、回答パターンをカバーするために、慎重にキュレートされている。
  論文  参考訳（メタデータ） (2024-06-30T15:42:18Z)
• Automatic AI Model Selection for Wireless Systems: Online Learning via Digital Twinning [50.332027356848094]
  AIベースのアプリケーションは、スケジューリングや電力制御などの機能を実行するために、インテリジェントコントローラにデプロイされる。 コンテキストとAIモデルのパラメータのマッピングは、ゼロショット方式で理想的に行われる。 本稿では,AMSマッピングのオンライン最適化のための一般的な手法を紹介する。
  論文  参考訳（メタデータ） (2024-06-22T11:17:50Z)
• Thread Detection and Response Generation using Transformers with Prompt Optimisation [5.335657953493376]
  本稿では,スレッドを識別し,その重要度に基づいて応答生成を優先するエンドツーエンドモデルを開発する。 モデルは最大10倍の速度向上を実現し、既存のモデルに比べて一貫性のある結果を生成する。
  論文  参考訳（メタデータ） (2024-03-09T14:50:20Z)
• Toward Educator-focused Automated Scoring Systems for Reading and Writing [0.0]
  本稿では,データとラベルの可用性,信頼性と拡張性,ドメインスコアリング,プロンプトとソースの多様性,伝達学習といった課題に対処する。 モデルトレーニングコストを増大させることなく、エッセイの長さを重要な特徴として保持する技術を採用している。
  論文  参考訳（メタデータ） (2021-12-22T15:44:30Z)
• Sensitivity analysis in differentially private machine learning using hybrid automatic differentiation [54.88777449903538]
  感性分析のための新しいテクスチブリド自動識別システム(AD)を導入する。 これにより、ニューラルネットワークをプライベートデータ上でトレーニングするなど、任意の微分可能な関数合成の感度をモデル化できる。 当社のアプローチは,データ処理の設定において,プライバシ損失に関する原則的推論を可能にする。
  論文  参考訳（メタデータ） (2021-07-09T07:19:23Z)
• On Learning Text Style Transfer with Direct Rewards [101.97136885111037]
  平行コーパスの欠如により、テキストスタイルの転送タスクの教師付きモデルを直接訓練することは不可能である。 我々は、当初、微調整されたニューラルマシン翻訳モデルに使用されていた意味的類似度指標を活用している。 我々のモデルは、強いベースラインに対する自動評価と人的評価の両方において大きな利益をもたらす。
  論文  参考訳（メタデータ） (2020-10-24T04:30:02Z)
• Recent Developments Combining Ensemble Smoother and Deep Generative Networks for Facies History Matching [58.720142291102135]
  本研究は、ファシズムモデルのための連続パラメータ化を構築するためのオートエンコーダネットワークの利用に焦点を当てる。 本稿では,VAE,GAN,Wasserstein GAN,変分自動符号化GAN,サイクルGANの主成分分析(PCA),転送スタイルネットワークのPCA,スタイル損失のVAEの7種類の定式化をベンチマークする。
  論文  参考訳（メタデータ） (2020-05-08T21:32:42Z)

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

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