論文の概要: Machine-Learned Premise Selection for Lean

• arxiv url: http://arxiv.org/abs/2304.00994v2
• Date: Wed, 14 Jun 2023 10:06:52 GMT
• ステータス: 処理完了
• システム内更新日: 2023-06-17 01:25:26.241403
• Title: Machine-Learned Premise Selection for Lean
• Title（参考訳）: リーンのための機械学習型前提選択
• Authors: Bartosz Piotrowski, Ramon Fern\'andez Mir, Edward Ayers
• Abstract要約: 我々は、ユーザーが証明した定理の適切な前提を提案する、リーン証明アシスタントのための機械学習ベースのツールを紹介します。 ツールの設計原則は,(1)証明アシスタントとの緊密な統合,(2)使いやすさとインストール,(3)軽量で迅速なアプローチである。
• 参考スコア（独自算出の注目度）: 0.8354034992258483
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce a machine-learning-based tool for the Lean proof assistant that suggests relevant premises for theorems being proved by a user. The design principles for the tool are (1) tight integration with the proof assistant, (2) ease of use and installation, (3) a lightweight and fast approach. For this purpose, we designed a custom version of the random forest model, trained in an online fashion. It is implemented directly in Lean, which was possible thanks to the rich and efficient metaprogramming features of Lean 4. The random forest is trained on data extracted from mathlib -- Lean's mathematics library. We experiment with various options for producing training features and labels. The advice from a trained model is accessible to the user via the suggest_premises tactic which can be called in an editor while constructing a proof interactively.
• Abstract（参考訳）: ユーザによって証明される定理の前提となる前提を示唆する,リーン証明アシスタントのための機械学習ベースのツールを紹介する。 ツールの設計原則は,(1)証明アシスタントとの緊密な統合,(2)使いやすさとインストール,(3)軽量で迅速なアプローチである。 この目的のために、オンラインで訓練されたランダム森林モデルのカスタムバージョンを設計した。 これはLean 4.0のリッチで効率的なメタプログラミング機能のおかげで可能になった。 ランダムな森は、リーンの数学ライブラリであるMathlibから抽出されたデータに基づいて訓練されている。 トレーニング機能やラベルを作成するための様々なオプションを試す。 トレーニングされたモデルからのアドバイスは、対話的に証明を構築しながら、エディターで呼び出すことができるsuggested_premises tacticを介してユーザに提供する。

関連論文リスト

• SPaR: Self-Play with Tree-Search Refinement to Improve Instruction-Following in Large Language Models [88.29990536278167]
  SPaRは、木探索の自己制限を統合したセルフプレイフレームワークで、気を散らさずに有効かつ同等の選好ペアを得る。 実験により,SPaRで誘導された3回の反復で訓練されたLLaMA3-8Bモデルが,一般機能を失うことなくIFEvalベンチマークでGPT-4-Turboを上回った。
  論文  参考訳（メタデータ） (2024-12-16T09:47:43Z)
• OMuleT: Orchestrating Multiple Tools for Practicable Conversational Recommendation [16.19266229218955]
  現実的な会話推薦システム(CRS)の設計、評価、実装のための体系的な取り組みを提案する。 本システムの目的は,ユーザが自由形式のテキストを入力してレコメンデーションをリクエストし,関連する,多様な項目のリストを受信できるようにすることである。 そこで本研究では,大規模言語モデル(LLM)に10以上のツールを組み,内部知識ベースと実運用で使用されるAPIコールへのアクセスを可能にする,新たなアプローチを提案する。
  論文  参考訳（メタデータ） (2024-11-28T19:53:39Z)
• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• CodeGen2: Lessons for Training LLMs on Programming and Natural Languages [116.74407069443895]
  我々はエンコーダとデコーダベースのモデルを単一のプレフィックスLMに統一する。 学習方法は,「フリーランチ」仮説の主張を考察する。 データ配信においては,混合分布と多言語学習がモデル性能に及ぼす影響について検討した。
  論文  参考訳（メタデータ） (2023-05-03T17:55:25Z)
• AdapterHub Playground: Simple and Flexible Few-Shot Learning with Adapters [34.86139827292556]
  事前訓練された言語モデルのオープンアクセスの普及は、最先端自然言語処理(NLP)研究の民主化につながった。 これにより、NLP以外の人たちでも、そのようなモデルを使用して、特定のユースケースに適応することが可能になります。 本研究では,一行のコードを書かずに事前学習したモデルを活用できるツールを提供することで,このギャップを克服することを目指している。
  論文  参考訳（メタデータ） (2021-08-18T11:56:01Z)
• A Simple yet Brisk and Efficient Active Learning Platform for Text Classification [4.2024137750169945]
  能動的学習を利用して非構造化データからモデルを直接構築する,フルマネージドな機械学習サービスを提案する。 弊社のアプローチでは,OpenAIのGPT2のような最先端のテキスト表現と,アクティブラーニングワークフローの迅速な実装を活用している。 公開および実生活の保険データセットに関する実験は、我々の単純かつ高速な分類アルゴリズムの選択が、現在進行中のタスクに理想的な理由を実証的に示している。
  論文  参考訳（メタデータ） (2021-01-31T10:44:04Z)
• SLADE: A Self-Training Framework For Distance Metric Learning [75.54078592084217]
  我々は、追加のラベルのないデータを活用することで、検索性能を向上させるための自己学習フレームワークSLADEを提案する。 まず、ラベル付きデータに基づいて教師モデルをトレーニングし、ラベルなしデータに対して擬似ラベルを生成する。 次に、最終機能埋め込みを生成するために、ラベルと擬似ラベルの両方で学生モデルをトレーニングします。
  論文  参考訳（メタデータ） (2020-11-20T08:26:10Z)
• Fast Few-Shot Classification by Few-Iteration Meta-Learning [173.32497326674775]
  数ショット分類のための高速な最適化に基づくメタラーニング手法を提案する。 我々の戦略はメタ学習において学習すべき基礎学習者の目的の重要な側面を可能にする。 我々は、我々のアプローチの速度と効果を実証し、総合的な実験分析を行う。
  論文  参考訳（メタデータ） (2020-10-01T15:59:31Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。