Fugu-MT 論文翻訳(概要): Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint

論文の概要: Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint

arxiv url: http://arxiv.org/abs/2305.15382v1
Date: Wed, 24 May 2023 17:40:54 GMT
ステータス: 処理完了
システム内更新日: 2023-05-25 13:51:25.068126
Title: Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
Title（参考訳）: 依存型高階論理の定理証明-拡張プレプリント
Authors: Colin Rothgang and Florian Rabe and Christoph Benzm\"uller
Abstract要約: 高階論理 HOL は、型付きデータ構造を表現および推論するための非常に単純な構文と意味論を提供します。依存型理論はそのようなリッチな型システムを提供するが、HOLとはかなり概念的な違いがある。本稿では,HOLのスタイルと概念的枠組みを維持した,依存型拡張DHOLを提案する。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.
Abstract（参考訳）: 高階論理holは、型付きデータ構造の表現と推論に非常にシンプルな構文と意味論を提供する。しかし型システムは、型が用語に依存する可能性のある高度な機能を持っていない。依存型理論はそのようなリッチな型システムを提供するが、HOLとはかなり概念的な違いがある。本稿では,HOLのスタイルと概念的枠組みを保持するHOLの拡張DHOLを提案する。さらに、DHOLからHOLへの変換を構築し、それをHOL定理証明器にプリプロセッサとして実装し、DHOLの定理証明器を得る。

関連論文リスト

Experiments with Choice in Dependently-Typed Higher-Order Logic [3.072340427031969]
ヒルベルトの不定選択作用素 $epsilon$ により DHOL 項構造を拡張する。選択項のHOL選択への変換を定義し、既存のDHOLからHOLへの変換を拡張する。選択を必要とするHOL問題に対する拡張翻訳の評価を行った。
論文参考訳（メタデータ） (2024-10-11T14:49:45Z)
SAIL: Self-Improving Efficient Online Alignment of Large Language Models [56.59644677997827]
人間のフィードバックからの強化学習は、大きな言語モデルを人間の好みに合わせるための重要な方法である。近年の文献では、オンラインRLHF法の設計に焦点が当てられているが、統一された概念的定式化はいまだに欠けている。提案手法は,計算オーバーヘッドを最小限に抑えたオープンソースデータセットのアライメント性能を著しく向上させる。
論文参考訳（メタデータ） (2024-06-21T18:05:35Z)
Beyond Prototypes: Semantic Anchor Regularization for Better Representation Learning [82.29761875805369]
表現学習の最終的な目標の1つは、クラス内のコンパクトさとクラス間の十分な分離性を達成することである。本稿では,機能セントロイドとして機能する事前定義されたクラスアンカーを用いて,特徴学習を一方向ガイドする新しい視点を提案する。提案したSemantic Anchor Regularization (SAR) は,既存モデルのプラグアンドプレイ方式で使用することができる。
論文参考訳（メタデータ） (2023-12-19T05:52:38Z)
Interpretability at Scale: Identifying Causal Mechanisms in Alpaca [62.65877150123775]
本研究では、Boundless DASを用いて、命令に従う間、大規模言語モデルにおける解釈可能な因果構造を効率的に探索する。私たちの発見は、成長し、最も広くデプロイされている言語モデルの内部構造を忠実に理解するための第一歩です。
論文参考訳（メタデータ） (2023-05-15T17:15:40Z)
METGEN: A Module-Based Entailment Tree Generation Framework for Answer Explanation [59.33241627273023]
複数のモジュールと推論コントローラを備えたモジュールベースのEntailment Tree GENフレームワークMETGENを提案する。質問に対して、METGENは、別々のモジュールで単一ステップのエンタテインメントを実行し、コントローラで推論フローを選択することで、エンタテインメントツリーを反復的に生成することができる。実験の結果,METGENは従来の最先端モデルよりも9%のパラメータで優れていた。
論文参考訳（メタデータ） (2022-05-05T12:06:02Z)
A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems [0.0]
本稿では,プログラムとプログラムが組み込まれている型システムの両方を表現可能な,確率的プログラミングのための形式メタ言語を提案する。我々は、我々のアプローチを形式化するために、立方体型理論と依存型メタグラフの枠組みを描いている。
論文参考訳（メタデータ） (2022-03-30T01:07:37Z)
Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs [2.28438857884398]
我々は、型チェックがプログラムの仮説空間の大部分を掃引することができることを示した。我々は合成節とプログラム全体の多形型を推測することができる。
論文参考訳（メタデータ） (2021-02-18T13:40:16Z)
Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文参考訳（メタデータ） (2020-09-07T19:50:10Z)
Plausible Reasoning about EL-Ontologies using Concept Interpolation [27.314325986689752]
本稿では,モデル理論の明確な意味論に基づく帰納的機構を提案する。我々は、カテゴリーベース誘導の認知モデルと密接に関連している強力なコモンセンス推論機構である推論に焦点を当てた。
論文参考訳（メタデータ） (2020-06-25T14:19:41Z)
Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
論文参考訳（メタデータ） (2020-05-05T12:10:21Z)
The Imandra Automated Reasoning System (system description) [0.0]
イマンドラ(Imandra)は、現代の計算論理学の定理証明器である。 SMTのような意思決定手順とACL2のような帰納的プロバーとのギャップを埋める。 Imandraには、大規模産業アプリケーションをサポートする新機能がある。
論文参考訳（メタデータ） (2020-04-21T19:57:34Z)

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