Fugu-MT 論文翻訳(概要): MoXIchecker: An Extensible Model Checker for MoXI

論文の概要: MoXIchecker: An Extensible Model Checker for MoXI

arxiv url: http://arxiv.org/abs/2407.15551v1
Date: Mon, 22 Jul 2024 11:26:04 GMT
ステータス: 処理完了
システム内更新日: 2024-07-23 15:11:26.826817
Title: MoXIchecker: An Extensible Model Checker for MoXI
Title（参考訳）: MoXI Checker: MoXI用の拡張可能なモデルチェッカー
Authors: Salih Ates, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee,
Abstract要約: MoXIは2024年に導入された新しい中間検証言語である。我々はMoXI検証タスクを直接解決する最初のモデルチェッカーであるMoXIcheckerを紹介する。
参考スコア（独自算出の注目度）: 3.9444967852633566
License: http://creativecommons.org/licenses/by/4.0/
Abstract: MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB 2 language with constructs to define state-transition systems. The tool suite of MoXI provides a translator from MoXI to Btor2, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for Btor2 to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in Btor2. We present MoXIchecker, the first model checker that solves MoXI verification tasks directly. Instead of translating MoXI to lower-level languages, MoXIchecker uses the solver-agnostic library PySMT for SMT solvers as backend for its verification algorithms. MoXIchecker is extensible because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the MoXI tool suite.
Abstract（参考訳）: MoXIは2024年に導入された新しい中間検証言語で、SMT-LIB 2言語を拡張して状態遷移システムを定義することで、シンボリックモデルチェックの標準化とオープンソース実装を促進する。 MoXIのツールスイートは、ハードウェア検証のための低レベル中間言語であるMoXIからBtor2へのトランスレータと、Btor2用の成熟ハードウェアモデルチェッカーを起動して、翻訳された検証タスクを分析する翻訳ベースモデルチェッカーを提供する。このような翻訳ベースのモデルチェッカーの拡張性は、整数や実算術のようなより複雑な理論は、Btor2の固定長のビットベクトルで正確に表現できないため制限される。我々はMoXI検証タスクを直接解決する最初のモデルチェッカーであるMoXIcheckerを紹介する。 MoXI を低レベル言語に翻訳する代わりに、MoXIchecker はその検証アルゴリズムのバックエンドとして SMT のソルバ非依存ライブラリ PySMT を使用している。 MoXIcheckerは、低レベル言語に制限されず、より複雑な理論を含む検証タスクに対応し、新しいアルゴリズムの実装を容易にするため拡張可能であり、PySMTのAPIを使用することで解決者に依存しない。評価において、MoXIcheckerは整数や実算術を使うタスクを一意に解決し、MoXIツールスイートから翻訳ベースのモデルチェッカーと同等のパフォーマンスを達成した。

関連論文リスト

Towards Zero-Shot Multimodal Machine Translation [64.9141931372384]
本稿では,マルチモーダル機械翻訳システムの学習において,完全教師付きデータの必要性を回避する手法を提案する。我々の手法はZeroMMTと呼ばれ、2つの目的の混合で学習することで、強いテキストのみの機械翻訳(MT)モデルを適応させることである。本手法が完全に教師付きトレーニングデータを持たない言語に一般化されることを証明するため,CoMMuTE評価データセットをアラビア語,ロシア語,中国語の3言語に拡張した。
論文参考訳（メタデータ） (2024-07-18T15:20:31Z)
LexMatcher: Dictionary-centric Data Collection for LLM-based Machine Translation [67.24113079928668]
本稿では、バイリンガル辞書に見られる感覚のカバレッジによって駆動されるデータキュレーション手法であるLexMatcherを提案する。我々の手法は、WMT2022テストセットの確立されたベースラインよりも優れています。
論文参考訳（メタデータ） (2024-06-03T15:30:36Z)
MambaByte: Token-free Selective State Space Model [71.90159903595514]
マンババイト(英: MambaByte)は、マンバSSMがバイト配列で自己回帰的に訓練したトークンレス適応である。 MambaByteは、言語モデリングタスクにおいて、最先端のサブワードトランスフォーマーよりも優れています。
論文参考訳（メタデータ） (2024-01-24T18:53:53Z)
CLIPTrans: Transferring Visual Knowledge with Pre-trained Models for Multimodal Machine Translation [31.911593690549633]
マルチモーダル機械翻訳(MMT)システムは、視覚的知識でニューラルネットワーク翻訳(NMT)を強化する。注釈付き多言語視覚言語データが不足しているため、従来の作業は、強力なMTTモデルをゼロからトレーニングする際の課題に直面していた。独立に訓練されたマルチモーダルM-CLIPと多言語mBARTを適応させるCLIPTransを提案する。
論文参考訳（メタデータ） (2023-08-29T11:29:43Z)
Sequential Monte Carlo Steering of Large Language Models using Probabilistic Programs [46.721838623748816]
本研究では,大規模言語モデルの出力に対する構文的制約と意味的制約を強制する新しい推論時手法を提案する。主要なアイデアは、言語生成タスクを離散確率列モデルのクラスにおける後部推論問題として指定することである。ビームサーチと同様の計算コストのために、SMCは多様なタスクを解決するためにLSMを操ることができる。
論文参考訳（メタデータ） (2023-06-05T17:55:05Z)
Active Learning for Neural Machine Translation [0.0]
NMTツールキットのJoey NMTにActive Learningと呼ばれるテクニックを組み込んで、低リソース言語翻訳の十分な精度と堅牢な予測を行った。この研究は、トランスフォーマーベースのNMTシステム、ベースラインモデル(BM)、フルトレーニングモデル(FTM)、アクティブラーニング最小信頼ベースモデル(ALLCM)、アクティブラーニングマージンサンプリングベースモデル(ALMSM)を用いて、英語をヒンディー語に翻訳する。
論文参考訳（メタデータ） (2022-12-30T17:04:01Z)
AutoMoE: Heterogeneous Mixture-of-Experts with Adaptive Computation for Efficient Neural Machine Translation [104.0979785739202]
ニューラルネットワーク翻訳(NMT)タスクにおいて、Mixture-of-Expert(MoE)モデルが最先端のパフォーマンスを得た。既存のMoEモデルは、ネットワーク全体に同じサイズの専門家が一様に配置される均質な設計を主に考慮している。計算制約下での不均一なMoEを設計するためのフレームワークであるAutoMoEを開発した。
論文参考訳（メタデータ） (2022-10-14T05:32:17Z)
Checks and Strategies for Enabling Code-Switched Machine Translation [22.67264032644644]
コードスイッチングは多言語話者の間で共通する現象であり、単一の会話の文脈内で2つ以上の言語間の交替が発生する。この研究は、コードスイッチされたテキストを処理する多言語ニューラルネットワーク翻訳(NMT)モデルの能力について検討する。
論文参考訳（メタデータ） (2022-10-11T02:25:21Z)
Language Models are Good Translators [63.528370845657896]
単一言語モデル(LM4MT)は,強力なエンコーダデコーダNMTモデルと同等の性能が得られることを示す。ピボットベースおよびゼロショット変換タスクの実験により、LM4MTはエンコーダ・デコーダのNMTモデルよりも大きなマージンで優れていることが示された。
論文参考訳（メタデータ） (2021-06-25T13:30:29Z)
Investigating Code-Mixed Modern Standard Arabic-Egyptian to English Machine Translation [6.021269454707625]
コード混在の現代標準アラビア語とエジプト・アラビア語(MSAEA)を英語に調査する。我々は、(i)標準のエンドツーエンドシーケンス・ツー・シーケンス(S2S)変換器と(ii)事前訓練されたS2S言語モデル(LM)を用いて、異なる条件下でモデルを開発する。我々は、スクラッチから訓練されたS2Sモデルと様々なアラビア方言のデータに基づいて微調整されたLMを用いて、MSA-EN並列データのみを用いて、合理的な性能を得ることができる。
論文参考訳（メタデータ） (2021-05-28T03:38:35Z)
Pre-training Multilingual Neural Machine Translation by Leveraging Alignment Information [72.2412707779571]
mRASPは、汎用多言語ニューラルマシン翻訳モデルを事前訓練するためのアプローチである。我々は,低,中,豊かな資源を含む多種多様な環境における42の翻訳方向の実験を行い,エキゾチックな言語対への変換を行った。
論文参考訳（メタデータ） (2020-10-07T03:57:54Z)

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

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