論文の概要: 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を介してユーザに提供する。
関連論文リスト
- Efficient Tool Use with Chain-of-Abstraction Reasoning [65.18096363216574]
大規模言語モデル(LLM)は、現実世界の知識に対する推論の基礎となる必要がある。
マルチステップ推論問題におけるツールの実行には,微調整LDMエージェントの課題が残されている。
マルチステップ推論におけるツールの活用方法として, LLM の新しい手法を提案する。
論文 参考訳(メタデータ) (2024-01-30T21:53:30Z) - 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) - Verifiable and Provably Secure Machine Unlearning [37.353982787321385]
機械学習は、トレーニング後の機械学習モデルのトレーニングデータセットからポイントを取り除くことを目的としている。
本稿では,機械のアンラーニングシステムの保証を捉えるための,検証可能なアンラーニングの最初の暗号的定義を示す。
我々は、線形回帰、ロジスティック回帰、ニューラルネットワークの実現可能性を検証するために、3つの異なるアンラーニング手法のプロトコルを実装した。
論文 参考訳(メタデータ) (2022-10-17T14:19:52Z) - SHiFT: An Efficient, Flexible Search Engine for Transfer Learning [16.289623977712086]
トランスファーラーニングは、スクラッチからトレーニングモデルのデータと計算効率の代替品と見なすことができる。
本稿では,トランスファー学習のための第1のダウンストリームタスク認識,フレキシブル,効率的なモデル検索エンジンであるSHiFTを提案する。
論文 参考訳(メタデータ) (2022-04-04T13:16:46Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。