論文の概要: 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アプリケーションの開発と検証を行う。
関連論文リスト
- 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 for Code Generation in Repository-Level Machine Learning Tasks [76.85930757493409]
大規模言語モデル(LLM)は、コード生成ベンチマークの習熟度を示しているが、これらの結果を実用的な開発シナリオに変換することは依然として難しい。
ML-Benchは、レポジトリレベルのオープンソースライブラリを統合して機械学習タスクを完了させるLLMの機能を評価するために設計された、新しいベンチマークである。
以上の結果から, GPT-4は他のLSMよりも優れており, 課題の複雑さを浮き彫りにしたタスクは33.82%に過ぎなかった。
論文 参考訳(メタデータ) (2023-11-16T12:03:21Z) - Large Language Model-Aware In-Context Learning for Code Generation [75.68709482932903]
大規模言語モデル(LLM)は、コード生成において印象的なコンテキスト内学習(ICL)能力を示している。
コード生成のためのLAIL (LLM-Aware In-context Learning) という新しい学習ベース選択手法を提案する。
論文 参考訳(メタデータ) (2023-10-15T06:12:58Z) - 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) - Condensing Multilingual Knowledge with Lightweight Language-Specific
Modules [52.973832863842546]
本稿では,Language-Specific Matrix Synthesis (LMS)法を紹介する。
このアプローチは、2つのかなり小さな行列から低ランク行列を生成することでLSモジュールを構築する。
複数のLSモジュールからの多言語知識を、Fuse Distillation (FD) 技術を用いて単一の共有モジュールに格納する。
論文 参考訳(メタデータ) (2023-05-23T12:21:38Z) - LLM-Pruner: On the Structural Pruning of Large Language Models [65.02607075556742]
大規模言語モデル(LLM)は、言語理解と生成において顕著な能力を示している。
タスク非依存であり、元のトレーニングデータセットへの依存を最小限に抑えるという2つの制約の範囲内でLLMの圧縮に取り組む。
LLM-Prunerという名前のこの手法は、非臨界結合構造を選択的に除去する構造プルーニングを採用する。
論文 参考訳(メタデータ) (2023-05-19T12:10:53Z) - SpecInfer: Accelerating Generative Large Language Model Serving with Tree-based Speculative Inference and Verification [13.174386920965107]
SpecInferは、木に基づく投機的推測と検証を扱う生成的大規模言語モデル(LLM)を高速化するシステムである。
トークンツリーで表される全ての候補トークンシーケンスの正当性を、新しいツリーベースの並列復号機構を用いてLLMに対して並列に検証する。
論文 参考訳(メタデータ) (2023-05-16T20:12:59Z) - Why do Nearest Neighbor Language Models Work? [93.71050438413121]
言語モデル(LM)は、すでに見られる文脈の表現を逐次計算することで、テキストの確率を計算する。
Retrieval-augmented LMは、大規模なデータストアから取得した情報にアクセスすることによって、標準的なニューラルLMよりも改善されている。
論文 参考訳(メタデータ) (2023-01-07T11:12:36Z) - Improving Bilingual Lexicon Induction with Cross-Encoder Reranking [71.56677929420138]
BLICEr (BLI with Cross-Encoder Re rank) と呼ばれる新しい半教師付きポストホックリグレード法を提案する。
鍵となる考え方は、mPLMから言語間の語彙的知識を抽出し、元のCLWEと組み合わせることである。
BLICErは、多様な言語にまたがる2つの標準BLIベンチマークで、新しい結果を確立している。
論文 参考訳(メタデータ) (2022-10-30T21:26:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。