論文の概要: Binary intersection formalized
- arxiv url: http://arxiv.org/abs/2006.16711v1
- Date: Tue, 30 Jun 2020 12:08:33 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-15 05:55:32.694808
- Title: Binary intersection formalized
- Title(参考訳): バイナリ交差点の形式化
- Authors: \v{S}t\v{e}p\'an Holub and \v{S}t\v{e}p\'an Starosta
- Abstract要約: 我々は射の用語を使い、その結果をより短くより透明な方法で定式化することができる。
証明アシスタントのIsabelle/HOLで結果の形式化を行う。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We provide a reformulation and a formalization of the classical result by
Juhani Karhum\"aki characterizing intersections of two languages of the form
$\{x,y\}^*\cap \{u,v\}^*$. We use the terminology of morphisms which allows to
formulate the result in a shorter and more transparent way, and we formalize
the result in the proof assistant Isabelle/HOL.
- Abstract(参考訳): 我々は、Juhani Karhum\"akiによって古典的な結果の改定と形式化を提供し、$\{x,y\}^*\cap \{u,v\}^*$という形の2つの言語の交叉を特徴づける。
我々は、より短くより透明な方法で結果を定式化できる射の用語を使用し、証明アシスタントのIsabelle/HOLで結果を形式化する。
関連論文リスト
- Labeled Morphological Segmentation with Semi-Markov Models [127.69031138022534]
いくつかのタスクを統一する形態的処理の代替として,ラベル付き形態的セグメンテーションを提案する。
また、形態素タグセットの新しい階層も導入する。
形態素を明示的にモデル化する識別型形態素分割システムであるモデル名を開発した。
論文 参考訳(メタデータ) (2024-04-13T12:51:53Z) - On the Origins of Linear Representations in Large Language Models [51.88404605700344]
我々は,次のトークン予測の概念力学を定式化するために,単純な潜在変数モデルを導入する。
実験により、潜在変数モデルと一致するデータから学習すると線形表現が現れることが示された。
また、LLaMA-2大言語モデルを用いて、理論のいくつかの予測を検証した。
論文 参考訳(メタデータ) (2024-03-06T17:17:36Z) - Lexinvariant Language Models [84.2829117441298]
離散語彙記号から連続ベクトルへの写像であるトークン埋め込みは、任意の言語モデル(LM)の中心にある
我々は、語彙記号に不変であり、したがって実際に固定トークン埋め込みを必要としないテクスチトレキシン変種モデルについて研究する。
十分長い文脈を条件として,レキシン変項LMは標準言語モデルに匹敵する難易度が得られることを示す。
論文 参考訳(メタデータ) (2023-05-24T19:10:46Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳(メタデータ) (2022-05-25T09:53:30Z) - Diffeomorphisms of Scalar Quantum Fields via Generating Functions [0.0]
正規微分同相のスカラー場への応用について検討する。
木振幅の相互作用が結果として生じる理論でなくなるという新しい証明を与える。
論文 参考訳(メタデータ) (2020-07-24T04:24:59Z) - Constructing a Family Tree of Ten Indo-European Languages with
Delexicalized Cross-linguistic Transfer Patterns [57.86480614673034]
我々は,デレクシカル化転送を,解釈可能なツリー・ツー・ストリングパターンとツリー・ツー・ツリーパターンとして定式化する。
これにより、言語間移動を定量的に探索し、第二言語習得の問い合わせを拡張することができる。
論文 参考訳(メタデータ) (2020-07-17T15:56:54Z) - Lattice Representation Learning [6.427169570069738]
ユークリッド空間に埋め込まれた格子を利用する離散表現を学習するための理論とアルゴリズムを導入する。
格子表現は興味深い性質の組み合わせを持つ:a) 格子量子化を用いて明示的に計算できるが、導入したアイデアを使って効率的に学習することができる。
この記事では、トレーニングや推論時間に使用される式をリンクする新しい数学的結果や、2つの一般的なデータセットに対する実験的な検証など、最初の2つの特性を探索し、活用するための基盤の整備に焦点をあてる。
論文 参考訳(メタデータ) (2020-06-24T16:05:11Z) - The Structure of Sum-Over-Paths, its Consequences, and Completeness for
Clifford [0.0]
線形写像や量子作用素を象徴的に表現するために用いられる「Sum-Over-Path」(SOP)の形式は、ダガーコンパクトな PROP の構造を持つことを示す。
論文 参考訳(メタデータ) (2020-03-12T09:38:10Z) - A refinement of Reznick's Positivstellensatz with applications to
quantum information theory [72.8349503901712]
ヒルベルトの17番目の問題において、アルティンはいくつかの変数の任意の正定値が2つの平方和の商として書けることを示した。
レズニックはアルティンの結果の分母は常に変数の平方ノルムの$N$-次パワーとして選択できることを示した。
論文 参考訳(メタデータ) (2019-09-04T11:46:26Z) - A Simple Joint Model for Improved Contextual Neural Lemmatization [60.802451210656805]
本稿では,20言語で最先端の成果を得られる,単純結合型ニューラルモデルを提案する。
本論文では,トレーニングと復号化に加えて,本モデルについて述べる。
論文 参考訳(メタデータ) (2019-04-04T02:03:19Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。