論文の概要: The Tactician's Web of Large-Scale Formal Knowledge

• arxiv url: http://arxiv.org/abs/2401.02950v1
• Date: Fri, 5 Jan 2024 18:52:35 GMT
• ステータス: 処理完了
• システム内更新日: 2024-01-08 14:28:46.397857
• Title: The Tactician's Web of Large-Scale Formal Knowledge
• Title（参考訳）: 戦術家による大規模形式知識のWeb
• Authors: Lasse Blaauwbroek
• Abstract要約: Tactician's Webは、強く相互接続され、マシンチェックされ、正式な数学的知識を提供するプラットフォームである。 Coq証明アシスタント上に構築されたこのプラットフォームは、さまざまな形式理論を含むデータセットをエクスポートする。 証明エージェントは、同じリッチなデータ表現を通じてCoqと相互作用し、定理のセットで自動的にベンチマークすることができる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Tactician's Web is a platform offering a large web of strongly interconnected, machine-checked, formal mathematical knowledge conveniently packaged for machine learning, analytics, and proof engineering. Built on top of the Coq proof assistant, the platform exports a dataset containing a wide variety of formal theories, presented as a web of definitions, theorems, proof terms, tactics, and proof states. Theories are encoded both as a semantic graph (rendered below) and as human-readable text, each with a unique set of advantages and disadvantages. Proving agents may interact with Coq through the same rich data representation and can be automatically benchmarked on a set of theorems. Tight integration with Coq provides the unique possibility to make agents available to proof engineers as practical tools.
• Abstract（参考訳）: Tactician's Webは、強力な相互接続、マシンチェック、フォーマルな数学的知識を備えた大規模なWebを提供するプラットフォームで、機械学習、分析、証明エンジニアリングに便利にパッケージされている。 coq proof assistant上に構築されたこのプラットフォームは、定義、定理、証明項、戦術、証明状態のwebとして提示される、さまざまな形式理論を含むデータセットをエクスポートする。 理論は、意味グラフ(下記参照)と人間の読みやすいテキストの両方で符号化され、それぞれに独自の利点と欠点がある。 証明エージェントは同じリッチデータ表現を通じてCoqと相互作用し、定理のセットで自動的にベンチマークすることができる。 Coqとの密接な統合は、実証エンジニアを実用的なツールとして利用できるようにするユニークな可能性を提供する。

関連論文リスト

• Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code [0.0]
  Coqの証明アシスタントは、数学的アサーションとソフトウェアの正確性を検証するための厳格なアプローチで際立っている。 人工知能と機械学習の進歩にもかかわらず、Coq構文と意味論の特殊性は大規模言語モデル(LLM)に固有の課題をもたらす。 このデータセットは、10,000以上のCoqソースファイルのコレクションから派生したもので、幅広い命題、証明、定義を含んでいる。
  論文  参考訳（メタデータ） (2024-03-19T10:53:40Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。 応用例としては、メタ理論的性質の形式的解析と検証がある。
  論文  参考訳（メタデータ） (2023-12-08T09:32:26Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
  オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。 本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
  論文  参考訳（メタデータ） (2023-01-05T17:56:00Z)
• Mapping the Internet: Modelling Entity Interactions in Complex Heterogeneous Networks [0.0]
  サンプル表現、モデル定義、トレーニングのための汎用性のある統一フレームワークHMill'を提案します。 フレームワークに実装されたモデルによって実現されたすべての関数の集合に対する普遍近似定理の拡張を示す。 このフレームワークを使ってサイバーセキュリティドメインから3つの異なる問題を解決する。
  論文  参考訳（メタデータ） (2021-04-19T21:32:44Z)
• Formalising Concepts as Grounded Abstractions [68.24080871981869]
  このレポートは、表現学習が生データから概念を誘導する方法を示しています。 このレポートの主な技術的目標は、表現学習のテクニックが概念空間の格子理論的定式化とどのように結婚できるかを示すことである。
  論文  参考訳（メタデータ） (2021-01-13T15:22:01Z)
• Self-Supervised Hyperboloid Representations from Logical Queries over Knowledge Graphs [18.92547855877845]
  知識グラフ(kgs)は、web検索、eコマース、ソーシャルネットワーク、生物学といった現実世界のアプリケーションにおいて、情報ストレージのためのユビキタスな構造である。 表現学習を,翻訳,交叉,結合問合せをkgs上で利用する自己教師付き論理問合せ推論問題として定式化する。 我々は,KG上の正の1次存在条件を用いて,その実体と関係をポインカーボール内のハイパーボロイドとして学習する,新しい自己教師型動的推論フレームワークであるHyperboloid Embeddings (HypE)を提案する。
  論文  参考訳（メタデータ） (2020-12-23T23:19:00Z)
• Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge [0.0]
  Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。 Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。 現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
  論文  参考訳（メタデータ） (2020-12-20T18:15:12Z)
• A Graph Representation of Semi-structured Data for Web Question Answering [96.46484690047491]
  本稿では、半構造化データとそれらの関係の構成要素の体系的分類に基づいて、Webテーブルとリストのグラフ表現を提案する。 本手法は,最先端のベースラインに対してF1スコアを3.90ポイント向上させる。
  論文  参考訳（メタデータ） (2020-10-14T04:01:54Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• CSNE: Conditional Signed Network Embedding [77.54225346953069]
  署名されたネットワークは、友人/フォアや信頼/不信のようなエンティティ間の正と負の関係を符号化する。 サイン予測のための既存の埋め込み手法は、一般に最適化関数におけるステータスやバランス理論の異なる概念を強制する。 条件付き符号付きネットワーク埋め込み(CSNE)を導入する。 我々の確率論的アプローチは、きめ細かな詳細とは別途、ネットワーク内の記号に関する構造情報をモデル化する。
  論文  参考訳（メタデータ） (2020-05-19T19:14:52Z)

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

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