論文の概要: The Imandra Automated Reasoning System (system description)
- arxiv url: http://arxiv.org/abs/2004.10263v1
- Date: Tue, 21 Apr 2020 19:57:34 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-11 07:41:43.438850
- Title: The Imandra Automated Reasoning System (system description)
- Title（参考訳）: イマンドラ自動推論システム(システム記述)
- Authors: Grant Olney Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken,
Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, and Nicola Mometto
- Abstract要約: イマンドラ(Imandra)は、現代の計算論理学の定理証明器である。
SMTのような意思決定手順とACL2のような帰納的プロバーとのギャップを埋める。
Imandraには、大規模産業アプリケーションをサポートする新機能がある。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We describe Imandra, a modern computational logic theorem prover designed to
bridge the gap between decision procedures such as SMT, semi-automatic
inductive provers of the Boyer-Moore family like ACL2, and interactive proof
assistants for typed higher-order logics. Imandra's logic is computational,
based on a pure subset of OCaml in which all functions are terminating, with
restrictions on types and higher-order functions that allow conjectures to be
translated into multi-sorted first-order logic with theories, including
arithmetic and datatypes. Imandra has novel features supporting large-scale
industrial applications, including a seamless integration of bounded and
unbounded verification, first-class computable counterexamples, efficiently
executable models and a cloud-native architecture supporting live multiuser
collaboration.
The core reasoning mechanisms of Imandra are (i) a semi-complete procedure
for finding models of formulas in the logic mentioned above, centered around
the lazy expansion of recursive functions, and (ii) an inductive waterfall and
simplifier which "lifts" many Boyer-Moore ideas to our typed higher-order
setting.
These mechanisms are tightly integrated and subject to many forms of user
control. Imandra's user interfaces include an interactive toplevel, Jupyter
notebooks and asynchronous document-based verification (in the spirit of
Isabelle's Prover IDE) with VS Code.
- Abstract（参考訳）: Imandraは、SMTのような決定手順、ACL2のようなBoier-Mooreファミリーの半自動帰納的プロデューサ、そして型付き高階論理の対話的証明アシスタントのギャップを埋めるために設計された、現代的な計算論理定理証明器である。
イマンドラの論理は計算であり、すべての関数が終端するocamlの純粋部分集合に基づいており、型や高階関数に制限があり、予想を算術やデータ型を含む理論を持つ多列一階述語論理に翻訳できる。
imandraには、境界付きおよび非境界型検証のシームレスな統合、ファーストクラスの計算可能なカウンター例、効率的な実行可能モデル、ライブマルチユーザコラボレーションをサポートするクラウドネイティブアーキテクチャなど、大規模な産業アプリケーションをサポートする新しい機能がある。
イマンドラの核となる推論機構は
一 上記の論理式において、再帰関数の遅延展開を中心とした式モデルを見つけるための半完全手順、及び
(ii)多くのボイヤームーアのアイデアを型づけされた高階設定に「リフト」する帰納的ウォーターフォールと単純化。
これらのメカニズムは密に統合され、ユーザー制御の多くの形態に適用される。
Imandraのユーザインターフェースには、インタラクティブなトップレベル、Jupyterノートブック、VS Codeによる非同期ドキュメントベースの検証(IsabelleのProver IDEの精神)が含まれている。
関連論文リスト
- A Semantic Parsing Algorithm to Solve Linear Ordering Problems [2.23890712706409]
線形順序付け問題を意味論的に解析するアルゴリズムを開発した。
提案手法は,複数の前提文と候補文を入力として扱う。
次に、制約論理プログラミングを用いて、注文に関する提案された文の真相を推測する。
論文 参考訳（メタデータ） (2025-02-12T13:58:42Z) - Effective Instruction Parsing Plugin for Complex Logical Query Answering on Knowledge Graphs [51.33342412699939]
知識グラフクエリ埋め込み(KGQE)は、不完全なKGに対する複雑な推論のために、低次元KG空間に一階論理(FOL)クエリを埋め込むことを目的としている。
近年の研究では、FOLクエリの論理的セマンティクスをよりよく捉えるために、さまざまな外部情報(エンティティタイプや関係コンテキストなど)を統合している。
コードのようなクエリ命令から遅延クエリパターンをキャプチャする効果的なクエリ命令解析(QIPP)を提案する。
論文 参考訳（メタデータ） (2024-10-27T03:18:52Z) - Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
大規模言語モデル(LLM)に基づくKG上の複雑な推論スキーマを提案する。
任意の一階論理クエリを二分木分解により拡張し、LLMの推論能力を刺激する。
広く使われているデータセットに対する実験では、LACTは高度な手法よりも大幅に改善されている(平均+5.5% MRRスコア)。
論文 参考訳（メタデータ） (2024-05-02T18:12:08Z) - Assessing Logical Reasoning Capabilities of Encoder-Only Transformer Models [0.13194391758295113]
本稿では,エンコーダのみのトランスフォーマー言語モデル (LM) が論理規則に従ってどの程度理にかなっているかを検討する。
様々なデータセットの論理的妥当性を決定するために,エンコーダのみのLMを適度に訓練できることを示す。
これらのデータセット上で微調整されたモデルをクロスプロブすることで、LMはそれらの仮定的論理的推論能力の伝達が困難であることを示す。
論文 参考訳（メタデータ） (2023-12-18T21:42:34Z) - Sorted LLaMA: Unlocking the Potential of Intermediate Layers of Large
Language Models for Dynamic Inference [32.62084449979531]
SortedNet を Sorted Fine-Tuning (SoFT) に置き換えることで生成 NLP タスクに拡張する。
我々のアプローチはモデル効率を向上し、推論中に様々なシナリオに対する複数のモデルの必要性を排除します。
以上の結果から,SFT+ICT(Early-Exit)と標準ファインチューニング(SFT+ICT)と比較して,サブモデルの優れた性能を示す。
論文 参考訳（メタデータ） (2023-09-16T11:58:34Z) - Query Structure Modeling for Inductive Logical Reasoning Over Knowledge
Graphs [67.043747188954]
KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。
線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。
2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
論文 参考訳（メタデータ） (2023-05-23T01:25:29Z) - Join-Chain Network: A Logical Reasoning View of the Multi-head Attention
in Transformer [59.73454783958702]
本稿では,多くの結合演算子を連結して出力論理式をモデル化するシンボリック推論アーキテクチャを提案する。
特に,このような結合鎖のアンサンブルが'ツリー構造'の1次論理式であるFOETの広い部分集合を表現できることを実証する。
変圧器における多頭部自己保持モジュールは,確率的述語空間における結合作用素の結合境界を実装する特別なニューラル演算子として理解することができる。
論文 参考訳（メタデータ） (2022-10-06T07:39:58Z) - ORCHARD: A Benchmark For Measuring Systematic Generalization of
Multi-Hierarchical Reasoning [8.004425059996963]
本稿では,Transformer と LSTM のモデルが体系的一般化において驚くほど失敗することを示す。
また、階層間の参照の増加に伴い、Transformerはランダムにしか動作しないことを示す。
論文 参考訳（メタデータ） (2021-11-28T03:11:37Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳（メタデータ） (2021-07-15T04:47:35Z) - Text Modular Networks: Learning to Decompose Tasks in the Language of
Existing Models [61.480085460269514]
本稿では,既存のモデルで解けるより単純なモデルに分解することで,複雑なタスクを解くための解釈可能なシステムを構築するためのフレームワークを提案する。
我々はこのフレームワークを用いて、ニューラルネットワークのファクトイド単一スパンQAモデルとシンボリック電卓で答えられるサブクエストに分解することで、マルチホップ推論問題に答えられるシステムであるModularQAを構築する。
論文 参考訳（メタデータ） (2020-09-01T23:45:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。