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

• arxiv url: http://arxiv.org/abs/2304.00994v1
• Date: Fri, 17 Mar 2023 10:37:34 GMT
• ステータス: 処理完了
• システム内更新日: 2023-04-09 05:45:02.079431
• 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を介してユーザに提供する。

関連論文リスト

• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• ALICE: Combining Feature Selection and Inter-Rater Agreeability for Machine Learning Insights [0.0]
  本稿では,新たなPythonライブラリであるAutomated Learning for Insightful Comparison and Evaluation(ALICE)を提案する。 これは、ブラックボックス機械学習モデルに対する洞察を求めるために、従来の特徴選択と、ユーザフレンドリなシンプルな方法で、ラタ間適合性の概念を融合する。 このフレームワークは、MLにおける解釈可能性の主要な概念の概要に続いて提案されている。
  論文  参考訳（メタデータ） (2024-04-13T17:34:58Z)
• 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)
• Retrieval as Attention: End-to-end Learning of Retrieval and Reading within a Single Transformer [80.50327229467993]
  学習した1つのモデルが競合検索とQA性能の両方を達成可能であることを示す。 エンドツーエンド適応は、教師なし設定と教師なし設定の両方において、ドメイン外のデータセットのパフォーマンスを大幅に向上させることを示す。
  論文  参考訳（メタデータ） (2022-12-05T04:51:21Z)
• 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)

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

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