Fugu-MT 論文翻訳(概要): LLMSTEP: LLM proofstep suggestions in Lean

論文の概要: 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ノートブックで動作するサーバ実装を、高速で効率的な言語モデル提案へのステップとして提供します。

関連論文リスト

Multilingual Prompts in LLM-Based Recommenders: Performance Across Languages [0.0]
この研究は、非英語のプロンプトがレコメンデーションパフォーマンスに与える影響を探求する。 ML1M、LastFM、Amazon-Beautyの3つの実世界のデータセットの評価は、非英語プロンプトの使用が一般的にパフォーマンスを低下させることを示した。多言語プロンプトによるリトレーニングにより、言語間のバランスの取れたパフォーマンスが向上したが、英語のパフォーマンスはわずかに低下した。
論文参考訳（メタデータ） (2024-09-11T20:31:42Z)
Show, Don't Tell: Aligning Language Models with Demonstrated Feedback [54.10302745921713]
Demonstration ITerated Task Optimization (DITTO)は、言語モデルの出力とユーザの実証された振る舞いを直接調整する。我々は,DITTOがニュース記事やメール,ブログ記事などのドメイン間できめ細かいスタイルやタスクアライメントを学習する能力を評価する。
論文参考訳（メタデータ） (2024-06-02T23:13:56Z)
CMULAB: An Open-Source Framework for Training and Deployment of Natural Language Processing Models [59.91221728187576]
本稿では,NLPモデルのモデル展開と連続的なヒューマン・イン・ザ・ループの微調整を簡単にするオープンソースフレームワークであるCMU言語バックエンドを紹介する。 CMULABは、マルチ言語モデルのパワーを活用して、音声認識、OCR、翻訳、構文解析などの既存のツールを新しい言語に迅速に適応し、拡張することができる。
論文参考訳（メタデータ） (2024-04-03T02:21:46Z)
LEIA: Facilitating Cross-lingual Knowledge Transfer in Language Models with Entity-based Data Augmentation [21.980770995466134]
言語間で整列したウィキペディアのエンティティ名を利用する言語適応チューニング手法である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)
L2CEval: Evaluating Language-to-Code Generation Capabilities of Large Language Models [102.00201523306986]
大規模言語モデル(LLM)の言語間コード生成能力を体系的に評価するL2CEvalを提案する。モデルのサイズ、事前学習データ、命令チューニング、異なるプロンプトメソッドなど、それらのパフォーマンスに影響を与える可能性のある要因を分析する。モデル性能の評価に加えて、モデルに対する信頼性校正を計測し、出力プログラムの人間による評価を行う。
論文参考訳（メタデータ） (2023-09-29T17:57:00Z)
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)

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