論文の概要: Isabelle Formalisation of Original Representation Theorems

• arxiv url: http://arxiv.org/abs/2306.10558v1
• Date: Sun, 18 Jun 2023 13:43:21 GMT
• ステータス: 処理完了
• システム内更新日: 2023-06-21 19:54:20.916144
• Title: Isabelle Formalisation of Original Representation Theorems
• Title（参考訳）: 原表現定理のイザベル形式化
• Authors: Marco B. Caminati
• Abstract要約: 明らかに無関係な数学的対象をリンクする新しい定理は、巨大なデータベース上のクロスサイトデータマイニングによって発見された。 そのような定理の起源と新しさを考えると、それらの形式的検証は特に望ましい。 本稿では、Isabelle/HOL定義と定理による検証を行い、そのプロセスで見られる技術的課題を明らかにする。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: In a recent paper, new theorems linking apparently unrelated mathematical objects (event structures from concurrency theory and full graphs arising in computational biology) were discovered by cross-site data mining on huge databases, and building on existing Isabelle-verified event structures enumeration algorithms. Given the origin and newness of such theorems, their formal verification is particularly desirable. This paper presents such a verification via Isabelle/HOL definitions and theorems, and exposes the technical challenges found in the process. The introduced formalisation completes the verification of Isabelle-verified event structure enumeration algorithms into a fully verified framework to link event structures to full graphs.
• Abstract（参考訳）: 最近の論文では、巨大なデータベース上のクロスサイトデータマイニングと、既存のイザベルで検証されたイベント構造列挙アルゴリズムに基づいて、明らかに無関係な数学的対象(並行性理論と計算生物学における全グラフからのイベント構造)をリンクする新たな定理が発見された。 そのような定理の起源と新しさを考えると、それらの形式的検証は特に望ましい。 本稿では,Isabelle/HOL定義と定理による検証を行い,そのプロセスにおける技術的課題を明らかにする。 導入された形式化は、Isabelleで検証されたイベント構造列挙アルゴリズムの完全な検証フレームワークへの検証を完了し、イベント構造を完全なグラフにリンクする。

関連論文リスト

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Compositional Structures in Neural Embedding and Interaction Decompositions [101.40245125955306]
  ニューラルネットワークにおけるベクトル埋め込みにおける線形代数構造間の基本的な対応について述べる。 相互作用分解」の観点から構成構造の特徴づけを導入する。 モデルの表現の中にそのような構造が存在するためには、必要かつ十分な条件を確立する。
  論文  参考訳（メタデータ） (2024-07-12T02:39:50Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)
• Counterfactual Explanations for Graph Classification Through the Lenses of Density [19.53018353016675]
  グラフ分類器のインスタンスレベルの反実例記述を生成するための一般密度に基づく反実例探索フレームワークを定義する。 この一般的なフレームワークでは,三角形の開きあるいは閉きによる反実数グラフの探索法と,最大傾きによって駆動される方法の2つの具体的インスタンス化を示す。 提案手法の有効性を7つの脳ネットワークデータセットで評価し, 広く利用されている指標に基づいて生成した偽事実を比較検討した。
  論文  参考訳（メタデータ） (2023-07-27T13:28:18Z)
• The Generative Programs Framework [0.0]
  任意の量的物理理論は、生成プログラムの形式で表すことができると論じる。 これらのグラフは「存在論的優先関係の符号化」と解釈でき、存在論的優先関係は因果関係の適切な一般化である。
  論文  参考訳（メタデータ） (2023-07-21T00:57:05Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。 線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。 2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
  論文  参考訳（メタデータ） (2023-05-23T01:25:29Z)
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics [7.607254619341369]
  本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。 ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。 テキスト内学習による文の自動書式化のベースライン結果について報告する。
  論文  参考訳（メタデータ） (2023-02-24T03:28:46Z)
• Self-organization Preserved Graph Structure Learning with Principle of Relevant Information [72.83485174169027]
  PRI-GSLは、自己組織化を特定し、隠された構造を明らかにするグラフ構造学習フレームワークである。 PRI-GSLは、フォン・ノイマンエントロピーと量子ジェンセン=シャノンの発散によって定量化された最も関連性が最も低い冗長な情報を含む構造を学ぶ。
  論文  参考訳（メタデータ） (2022-12-30T16:02:02Z)
• Generalization Guarantee of Training Graph Convolutional Networks with Graph Topology Sampling [83.77955213766896]
  グラフ畳み込みネットワーク(GCN)は近年,グラフ構造化データの学習において大きな成功を収めている。 スケーラビリティ問題に対処するため、Gsの学習におけるメモリと計算コストを削減するため、グラフトポロジサンプリングが提案されている。 本稿では,3層GCNのトレーニング(最大)におけるグラフトポロジサンプリングの最初の理論的正当性について述べる。
  論文  参考訳（メタデータ） (2022-07-07T21:25:55Z)
• Structural Causal Models Are (Solvable by) Credal Networks [70.45873402967297]
  因果推論は、干潟網の更新のための標準的なアルゴリズムによって得ることができる。 この貢献は, 干潟ネットワークによる構造因果モデルを表現するための体系的なアプローチと見なされるべきである。 実験により, 実規模問題における因果推論には, クレーダルネットワークの近似アルゴリズムがすぐに利用できることがわかった。
  論文  参考訳（メタデータ） (2020-08-02T11:19:36Z)

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

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