論文の概要: LLMSTEP: LLM proofstep suggestions in Lean
- arxiv url: http://arxiv.org/abs/2310.18457v1
- Date: Fri, 27 Oct 2023 20:10:56 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-31 18:34:46.661971
- Title: LLMSTEP: LLM proofstep suggestions in Lean
- Title(参考訳): LLMSTEP: リーンにおけるLLMの証明ステップの提案
- Authors: Sean Welleck and Rahul Saha
- Abstract要約: LLMSTEPはLean 4の戦術で、ユーザの証明状態を言語モデルをホストするサーバに送る。
言語モデルは提案を生成し、リーンでチェックされ、開発環境でユーザに表示される。
- 参考スコア(独自算出の注目度): 27.5626664686618
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present LLMSTEP, a tool for integrating a language model into the Lean
proof assistant. LLMSTEP is a Lean 4 tactic that sends a user's proof state to
a server hosting a language model. The language model generates suggestions,
which are checked in Lean and displayed to a user in their development
environment. We provide a baseline language model, along with code for
fine-tuning and evaluation to support further development. We provide server
implementations that run on CPU, a CUDA GPU, or a Google Colab notebook, as a
step towards fast, effective language model suggestions for any user.
- Abstract(参考訳): LLMSTEPは,言語モデルをリーン証明アシスタントに統合するためのツールである。
LLMSTEPはLean 4の戦術で、ユーザの証明状態を言語モデルをホストするサーバに送る。
言語モデルは提案を生成し、リーンでチェックされ、開発環境でユーザに表示される。
我々は、ベースライン言語モデルと、さらなる開発をサポートするための微調整と評価のためのコードを提供します。
CPU、CUDA GPU、またはGoogle Colabノートブックで動作するサーバ実装を、高速で効率的な言語モデル提案へのステップとして提供します。
関連論文リスト
- LEIA: Facilitating Cross-Lingual Knowledge Transfer in Language Models
with Entity-based Data Augmentation [25.967369103344588]
言語間で整列したウィキペディアのエンティティ名を利用する言語適応チューニング手法であるLEIAを紹介する。
この方法は、ターゲット言語コーパスを英語のエンティティ名で拡張し、左から右への言語モデリングを用いてモデルを訓練することを含む。
論文 参考訳(メタデータ) (2024-02-18T07:24:34Z) - If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code
Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
大型言語モデル(LLM)は、自然言語と形式言語(コード)の組み合わせに基づいて訓練される
コードは、標準構文、論理一貫性、抽象化、モジュール性を備えた高レベルの目標を実行可能なステップに変換する。
論文 参考訳(メタデータ) (2024-01-01T16:51:20Z) - Lenna: Language Enhanced Reasoning Detection Assistant [22.105472753701076]
大規模な言語モデルに埋め込まれた推論能力と世界知識は、画像認識タスクにおいて、はるかに少ない研究と活用がなされている。
MLLMの頑健なマルチモーダル特徴表現を利用した言語強化推論検出アシスタントLennaを提案する。
LennaはReasonDetで優れたパフォーマンスを示しており、トレーニングコストはかなり低い。
論文 参考訳(メタデータ) (2023-12-05T02:19:35Z) - Large Language Model Inference with Lexical Shortlisting [80.46235795566183]
大規模言語モデル(LLM)の推論は計算とメモリ集約であり、語彙的ショートリストに適応する。
Unicodeベースのスクリプトフィルタリングとコーパスベースの選択という,LLM推論時にサブ語彙をショートリスト化する2つのタスクについて検討する。
語彙的ショートリストは,一部のモデルのメモリ使用量を50%近く削減し,生成速度が25%向上することを示す。
論文 参考訳(メタデータ) (2023-11-16T09:35:50Z) - L2CEval: Evaluating Language-to-Code Generation Capabilities of Large
Language Models [102.00201523306986]
大規模言語モデル(LLM)の言語間コード生成能力を体系的に評価するL2CEvalを提案する。
モデルのサイズ、事前学習データ、命令チューニング、異なるプロンプトメソッドなど、それらのパフォーマンスに影響を与える可能性のある要因を分析する。
モデル性能の評価に加えて、モデルに対する信頼性校正を計測し、出力プログラムの人間による評価を行う。
論文 参考訳(メタデータ) (2023-09-29T17:57:00Z) - Domain Adaptive Code Completion via Language Models and Decoupled Domain
Databases [15.964849180459675]
$k$NM-LMは、ドメイン知識を微調整なしで言語モデルに統合する検索強化言語モデルである。
私たちのアプローチは、異なる言語モデルとドメインに自動的に適応できます。
論文 参考訳(メタデータ) (2023-08-18T05:25:55Z) - Soft Language Clustering for Multilingual Model Pre-training [57.18058739931463]
本稿では,インスタンスを条件付きで符号化するためのフレキシブルガイダンスとして,コンテキスト的にプロンプトを検索するXLM-Pを提案する。
我々のXLM-Pは、(1)言語間における言語不変および言語固有知識の軽量なモデリングを可能にし、(2)他の多言語事前学習手法との容易な統合を可能にする。
論文 参考訳(メタデータ) (2023-06-13T08:08:08Z) - InstructAlign: High-and-Low Resource Language Alignment via Continual
Crosslingual Instruction Tuning [66.31509106146605]
命令を調整した大規模言語モデル(LLM)は、様々なタスクや言語で顕著な能力を示している。
しかし、利用可能なデータが不足しているため、表現不足の言語に一般化する能力は限られている。
InstructAlignは、LLMが新しい未知の言語を学習済みの高リソース言語と整列できるようにするために、連続的なクロスリンガル命令チューニングを使用する。
論文 参考訳(メタデータ) (2023-05-23T02:51:34Z) - Prompting Is Programming: A Query Language for Large Language Models [5.8010446129208155]
我々はLMP(Language Model Programming)という新しいアイデアを提示する。
LMPは、純粋なテキストプロンプトからテキストプロンプトとスクリプティングの直感的な組み合わせまで、言語モデルを一般化する。
LMQLは、さまざまな最先端のプロンプトメソッドを直感的にキャプチャできることを示す。
論文 参考訳(メタデータ) (2022-12-12T18:09:09Z) - Generalizing Multimodal Pre-training into Multilingual via Language
Acquisition [54.69707237195554]
英語のVision-Language Pre-Trainingは、様々な下流タスクで大きな成功を収めた。
この成功を英語以外の言語に一般化するために、Multilingual Vision-Language Pre-Trainingを通じていくつかの取り組みがなされている。
単言語視覚言語事前学習モデルを多言語に容易に一般化できるtextbfMultitextbfLingual textbfAcquisition (MLA) フレームワークを提案する。
論文 参考訳(メタデータ) (2022-05-29T08:53:22Z) - Universal Sentence Representation Learning with Conditional Masked
Language Model [7.334766841801749]
文表現を効果的に学習するための条件付きマスク言語モデリング(M)を提案する。
我々の英語CMLMモデルは,SentEvalの最先端性能を実現する。
完全に教師なしの学習方法として、CMLMは幅広い言語やドメインに便利に拡張できます。
論文 参考訳(メタデータ) (2020-12-28T18:06:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。