Fugu-MT 論文翻訳(概要): Verified Scalable Parallel Computing with Why3

論文の概要: Verified Scalable Parallel Computing with Why3

arxiv url: http://arxiv.org/abs/2307.16592v1
Date: Mon, 31 Jul 2023 11:46:16 GMT
ステータス: 処理完了
システム内更新日: 2023-10-23 15:49:36.920038
Title: Verified Scalable Parallel Computing with Why3
Title（参考訳）: why3によるスケーラブル並列コンピューティングの検証
Authors: Olivia Proust (LMV), Fr\'ed\'eric Loulergue (LMV)
Abstract要約: B はマルチパラダイム言語 OCaml の純粋機能ライブラリである。本稿では,WhyML を用いた B プリミティブの形式化を提案し,B 標準ライブラリの大部分の正当性を規定し,証明する。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: BSML is a pure functional library for the multi-paradigm language OCaml. BSML embodies the principles of the Bulk Synchronous Parallel (BSP) model, a model of scalable parallel computing. We propose a formalization of BSML primitives with WhyML, the specification language of Why3 and specify and prove the correctness of most of the BSML standard library. Finally, we develop and verify the correctness of a small BSML application.
Abstract（参考訳）: BSMLは、マルチパラダイム言語OCamlのための純粋な機能ライブラリである。 BSMLはスケーラブル並列コンピューティングのモデルであるBulk Synchronous Parallel(BSP)モデルの原則を具現化している。本稿では、Why3の仕様言語であるWhyMLを用いてBSMLプリミティブの形式化を提案し、BSML標準ライブラリのほとんどを特定・証明する。最後に,小型BSMLアプリケーションの開発と検証を行う。

関連論文リスト

LLaVA-KD: A Framework of Distilling Multimodal Large Language Models [70.19607283302712]
本稿では,l-MLLMからs-MLLMへ知識を伝達する新しいフレームワークを提案する。具体的には,l-MLLMとs-MLLMの視覚的テキスト出力分布のばらつきを最小限に抑えるために,MDist(Multimodal Distillation)を導入する。また,S-MLLMの可能性を完全に活用するための3段階学習手法を提案する。
論文参考訳（メタデータ） (2024-10-21T17:41:28Z)
LBC: Language-Based-Classifier for Out-Of-Variable Generalization [14.033963471962823]
大規模言語モデル(LLM)は、応答生成のような自然言語処理タスクにおいて大きな成功を収めている。 LLMの事前学習された知識により、追加のトレーニングなしでテストに現れる新しい変数を解釈できることがわかった。本稿では,LBC(Language-Based-Classifier)を提案する。
論文参考訳（メタデータ） (2024-08-20T15:05:02Z)
Spectra: Surprising Effectiveness of Pretraining Ternary Language Models at Scale [16.865532646589987]
本稿では,従来の浮動小数点モデル(FloatLM)とその後量子化バージョン(QuantLM)の代替として,低ビット幅モデル,特に第三言語モデル(TriLM)の事前学習について検討する。我々は、FloatLMs、QuantLMs、TriLMsを含む複数のビット幅にまたがる最初のオープンなLLMスイートであるSpectra LLMスイートを、300Bトークンでトレーニングされた99Mから3.9Bのパラメータで紹介する。
論文参考訳（メタデータ） (2024-07-17T05:53:20Z)
Understanding and Mitigating Language Confusion in LLMs [76.96033035093204]
我々は,既存の英語および多言語プロンプトを用いた15の型的多様言語の評価を行った。 Llama Instruct と Mistral のモデルでは,言語的混乱の度合いが高いことがわかった。言語混乱は,数発のプロンプト,多言語SFT,選好調整によって部分的に緩和できることがわかった。
論文参考訳（メタデータ） (2024-06-28T17:03:51Z)
Verbalized Machine Learning: Revisiting Machine Learning with Language Models [63.10391314749408]
言語化機械学習(VML)の枠組みを紹介する。 VMLはパラメータ空間を人間の解釈可能な自然言語に制限する。我々は,VMLの有効性を実証的に検証し,VMLがより強力な解釈可能性を実現するためのステップストーンとして機能することを期待する。
論文参考訳（メタデータ） (2024-06-06T17:59:56Z)
TransMI: A Framework to Create Strong Baselines from Multilingual Pretrained Language Models for Transliterated Data [50.40191599304911]
そこで我々は,Transliterate Transliteration-Merge (TransMI)を提案する。結果は、モデルやタスクによって異なるが、3%から34%の改善が一貫したことを示している。
論文参考訳（メタデータ） (2024-05-16T09:08:09Z)
Making Large Language Models A Better Foundation For Dense Retrieval [19.38740248464456]
デンス検索では,クエリとドキュメント間の意味的関係を表現するために,識別テキストの埋め込みを学習する必要がある。意味理解におけるLLMの強い能力を考えると、大きな言語モデル(LLM)の使用の恩恵を受けるかもしれない。本稿では,LLaRA (LLM adapted for dense RetrievAl) を提案する。
論文参考訳（メタデータ） (2023-12-24T15:10:35Z)
ML-Bench: Evaluating Large Language Models and Agents for Machine Learning Tasks on Repository-Level Code [76.84199699772903]
ML-Benchは、既存のコードリポジトリを利用してタスクを実行する現実世界のプログラミングアプリケーションに根ざしたベンチマークである。 LLM(Large Language Model)とAIエージェントの両方を評価するために、事前に定義されたデプロイメント環境でLLMのテキスト-コード変換を評価するML-LLM-Benchと、Linuxサンドボックス環境でエンドツーエンドのタスク実行で自律エージェントをテストするML-Agent-Benchの2つの設定が採用されている。
論文参考訳（メタデータ） (2023-11-16T12:03:21Z)
Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation [11.663380583835288]
本稿では,単一GPU上でLoRAを用いたNL-FOL翻訳のためのモデルであるLogicLLaMAを紹介する。 LogicLLaMAは、自然言語を直接FOLルールに変換することができ、GPT-3.5より優れている。また、GPT-3.5で予測されるFOLルールの修正も可能で、GPT-4と同等の性能をコストのごく一部で達成できる。
論文参考訳（メタデータ） (2023-05-24T19:59:51Z)
LLM-Pruner: On the Structural Pruning of Large Language Models [65.02607075556742]
大規模言語モデル(LLM)は、言語理解と生成において顕著な能力を示している。タスク非依存であり、元のトレーニングデータセットへの依存を最小限に抑えるという2つの制約の範囲内でLLMの圧縮に取り組む。 LLM-Prunerという名前のこの手法は、非臨界結合構造を選択的に除去する構造プルーニングを採用する。
論文参考訳（メタデータ） (2023-05-19T12:10:53Z)

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