論文の概要: Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)

• arxiv url: http://arxiv.org/abs/2004.10667v3
• Date: Tue, 26 May 2020 07:46:04 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-11 06:20:28.553680
• Title: Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
• Title（参考訳）: Isabelle/HOLにおける証明法勧告のための簡易データセット(データセット記述)
• Authors: Yutaka Nagashima
• Abstract要約: そこで本研究では,400k以上の証明手法を応用したデータと,100以上の特徴を抽出したデータを含む,簡単なデータセットを提案する。 我々の単純なデータフォーマットにより、機械学習の実践者は、論理学の専門知識を必要とせずに、機械学習ツールを使ってIsabelle/HOLの証明メソッドを予測できます。
• 参考スコア（独自算出の注目度）: 6.85316573653194
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from achieving a large scale success in this field. In this data description, we present a simple dataset that contains data on over 400k proof method applications along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic. Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL without requiring domain expertise in logic.
• Abstract（参考訳）: 近年,対話型定理証明器のユーザを支援するために機械学習を応用する研究者が増えている。 しかし、基礎となる論理の表現的な性質と証明文書の難解な構造は、しばしば形式論理学の専門知識を持たない機械学習の実践者にとって、この分野での大規模な成功を妨げている。 このデータ記述では,400k以上の証明法アプリケーションと100以上の抽出された特徴を含む単純なデータセットを,形式論理の知識を必要とせずに容易に処理可能な形式として提示する。 我々の単純なデータフォーマットにより、機械学習の実践者は、論理学の専門知識を必要とせずに、機械学習ツールを使ってIsabelle/HOLの証明メソッドを予測できます。

関連論文リスト

• Topological Methods in Machine Learning: A Tutorial for Practitioners [4.297070083645049]
  トポロジカル機械学習(TML)は、代数的トポロジの技法を利用して複雑なデータ構造を分析する分野である。 このチュートリアルは、2つの重要なTMLテクニック、永続的ホモロジーとMapperアルゴリズムの包括的な紹介を提供する。 アクセシビリティを高めるために、私たちはデータ中心のアプローチを採用し、読者はこれらのテクニックを関連するタスクに適用したハンズオン体験を得ることができる。
  論文  参考訳（メタデータ） (2024-09-04T17:44:52Z)
• Can LLMs Separate Instructions From Data? And What Do We Even Mean By That? [60.50127555651554]
  大規模言語モデル(LLM)は、多くの実用的なアプリケーションにおいて印象的な結果を示すが、基本的な安全性機能は欠如している。 これにより、間接的なプロンプトインジェクションのような操作に脆弱になり、一般に安全クリティカルなタスクには適さない。 モデル出力から計算可能な命令データ分離の形式的尺度と経験的変量を導入する。
  論文  参考訳（メタデータ） (2024-03-11T15:48:56Z)
• MLFMF: Data Sets for Machine Learning for Mathematical Formalization [0.18416014644193068]
  MLFMF(MLFMF)は、証明アシスタントを用いた数学の形式化を支援するために使用されるベンチマークシステムのためのデータセットの集合である。 各データセットは、AgdaやLeanの証明アシスタントで書かれた形式化された数学のライブラリから導かれる。 合計25万ドル以上のエントリーがあり、これは現在、機械学習可能な形式における公式な数学的知識のコレクションとして最大である。
  論文  参考訳（メタデータ） (2023-10-24T17:00:00Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。 まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。 我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
  論文  参考訳（メタデータ） (2023-05-22T06:11:15Z)
• Rethinking Complex Queries on Knowledge Graphs with Neural Link Predictors [58.340159346749964]
  本稿では,証明可能な推論能力を備えた複雑なクエリを用いたエンドツーエンド学習を支援するニューラルシンボリック手法を提案する。 これまでに検討されていない10種類の新しいクエリを含む新しいデータセットを開発する。 提案手法は,新しいデータセットにおいて先行手法を著しく上回り,既存データセットにおける先行手法を同時に上回っている。
  論文  参考訳（メタデータ） (2023-04-14T11:35:35Z)
• On Exams with the Isabelle Proof Assistant [0.0]
  本稿では,Isabelle証明アシスタントを用いた自動推論のコースにおいて,学生の学習結果をテストするためのアプローチを提案する。 このアプローチにより、様々な論理的証明システムにおける形式的証明の一般的な理解と、イザベル/HOLの高階論理における証明の理解の両方をテストすることができる。
  論文  参考訳（メタデータ） (2023-03-10T11:37:09Z)
• Explaining Classifiers Trained on Raw Hierarchical Multiple-Instance Data [0.0]
  多くのデータソースは、構造化されたデータ交換フォーマット(例えば、XMLフォーマットの複数のセキュリティログ)の自然な形式を持っています。 階層型インスタンス学習(HMIL)のような既存の手法では、そのようなデータを生の形式で学習することができる。 これらのモデルをサブセット選択問題として扱うことにより、計算効率のよいアルゴリズムを用いて、解釈可能な説明が好ましい性質でどのように生成できるかを実証する。 我々は,グラフニューラルネットワークから導入した説明手法と比較して,桁違いの高速化と高品質な説明を行う。
  論文  参考訳（メタデータ） (2022-08-04T14:48:37Z)
• Questions Are All You Need to Train a Dense Passage Retriever [123.13872383489172]
  ARTは、ラベル付きトレーニングデータを必要としない高密度検索モデルをトレーニングするための、新しいコーパスレベルのオートエンコーディングアプローチである。 そこで,(1) 入力質問を用いて証拠文書の集合を検索し,(2) 文書を用いて元の質問を再構築する確率を計算する。
  論文  参考訳（メタデータ） (2022-06-21T18:16:31Z)
• Proving Theorems using Incremental Learning and Hindsight Experience Replay [45.277067974919106]
  等式のない一階述語論理のドメイン固有プローバを学習するための一般的な漸進学習アルゴリズムを提案する。 我々は、証明が見つからない場合でも学べるように、後見経験の再生を定理証明に適用する。 我々は、この方法で訓練されたプローバーがTPTPデータセットの最先端の伝統的なプローバーにマッチし、時には超えることを示した。
  論文  参考訳（メタデータ） (2021-12-20T16:40:26Z)
• Combining Feature and Instance Attribution to Detect Artifacts [62.63504976810927]
  トレーニングデータアーティファクトの識別を容易にする手法を提案する。 提案手法は,トレーニングデータのアーティファクトの発見に有効であることを示す。 我々は,これらの手法が実際にNLP研究者にとって有用かどうかを評価するために,小規模なユーザスタディを実施している。
  論文  参考訳（メタデータ） (2021-07-01T09:26:13Z)

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

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