論文の概要: 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アプリケーションの開発と検証を行う。
関連論文リスト
- TituLLMs: A Family of Bangla LLMs with Comprehensive Benchmarking [6.070192392563392]
1B と 3B のパラメータサイズで最初の大容量バングラ LLM である TituLLMs を提示する。
TituLLMsをトレーニングするために、約37億トークンの事前トレーニングデータセットを収集しました。
我々はLlama-3.2トークンを言語や文化固有の知識に組み込むように拡張した。
論文 参考訳(メタデータ) (2025-02-16T16:22:23Z) - Small Models, Big Impact: Efficient Corpus and Graph-Based Adaptation of Small Multilingual Language Models for Low-Resource Languages [10.418542753869433]
低リソース言語(LRL)は、限られたデータのために自然言語処理(NLP)において重大な課題に直面している。
現在の最先端の大規模言語モデル(LLM)は、まだLRLと競合している。
mBERTやXLM-Rのような小さなマルチリンガルモデル(mLM)は、トレーニングデータサイズに適合する能力が向上するため、より有望である。
論文 参考訳(メタデータ) (2025-02-14T13:10:39Z) - Adaptive Self-improvement LLM Agentic System for ML Library Development [8.766639641127412]
大規模言語モデル(LLM)は一般的なコーディング能力を示している。
LLMはこのタスクを完了するには、限られたデータによる複雑な推論が必要である。
オープンおよびクローズドソースのLLMを用いてASPLコードを生成する適応型自己改善エージェントシステムを提案する。
論文 参考訳(メタデータ) (2025-02-04T17:57:17Z) - 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) - An empirical study of LLaMA3 quantization: from LLMs to MLLMs [54.91212829143966]
LLaMAファミリーは、最も強力なオープンソースの大規模言語モデル(LLM)の1つである。
LLaMA3モデルは、15T以上のデータに対する超大規模事前トレーニングによって、様々な領域で優れたパフォーマンスを実現している。
我々は,LLaMA3の1-8ビットおよび様々なデータセット上で,LLaMA3の学習後量子化とLoRA微調整(LoRA-FT)の10種類の既存手法を評価し,LLaMA3の低ビット量子化性能を明らかにする。
論文 参考訳(メタデータ) (2024-04-22T10:03:03Z) - 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) - LLM-Pruner: On the Structural Pruning of Large Language Models [65.02607075556742]
大規模言語モデル(LLM)は、言語理解と生成において顕著な能力を示している。
タスク非依存であり、元のトレーニングデータセットへの依存を最小限に抑えるという2つの制約の範囲内でLLMの圧縮に取り組む。
LLM-Prunerという名前のこの手法は、非臨界結合構造を選択的に除去する構造プルーニングを採用する。
論文 参考訳(メタデータ) (2023-05-19T12:10:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。