論文の概要: Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
- arxiv url: http://arxiv.org/abs/2609.07345v1
- Date: Mon, 07 Sep 2026 11:09:03 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-10 19:44:08.415677
- Title: Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
- Title（参考訳）: HOLにおけるモナディック二階述語論理--自動化された信心(拡張プレプリント)による深度と浅度
- Abstract要約: Isabelle/HOLでは、先行研究のディープ・アンド・シャロー埋め込み手法をモナディック二階述語論理に適用する。
3つの埋め込みが並行して開発され、深層埋め込み、最大浅層埋め込み、最小浅層埋め込みである。
中心的な貢献は、完全に機械化された2階下方へのローウェンハイム・スコレムの定理である。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In Isabelle/HOL, we apply the deep-and-shallow embedding methodology of our prior work to monadic second-order logic (MSO). Three embeddings are developed side by side: a deep embedding (an inductive datatype with an explicit satisfaction relation); a maximal-shallow embedding that translates the connectives and quantifiers directly into HOL, carrying the interpretation and both assignments as explicit arguments; and a minimal-shallow embedding -- a locale that fixes those parameters, collapsing the formula type to bool. The enabling new ingredient is a two-sorted substitution apparatus -- capture-avoiding substitution, renaming, and a substitution lemma per namespace -- in which each binder is transparent for the other; faithfulness of all three embeddings is mechanised and automated. Our central contribution is a fully mechanised two-sorted downward Loewenheim-Skolem theorem: the minimal embedding recovers deep validity relative to the (countable) assignment ranges, and this range-relative reading is shown to coincide with the general (Henkin-style) reading of MSO, whereas the standard reading is provably stronger, witnessed by comprehension. Both readings are nonetheless recovered from the minimal embedding, differing only in the admitted interpretations: all of them for the general reading, only the elementary substructures of the full model for the standard. We further exercise the embeddings on classical MSO landmarks: the Boolean-closure and graph schemata hold under the full second-order domain yet fail in the minimal embedding, making the dichotomy concrete, while reachability and 2-colorability are refuted throughout.
- Abstract（参考訳）: Isabelle/HOLでは、先行研究のディープ・アンド・シャロー埋め込み手法をモナディック二階述語論理(MSO)に適用する。
ディープ埋め込み(明示的な満足度関係を持つインダクティブデータ型)、接続子と量化子を直接HOLに変換して、解釈と両方の代入を明示的な引数として持参する最大シュロー埋め込み、そしてそれらのパラメータを修正するローカライズ -- 式型をブールに分解するローカライズである。
新規成分の有効化は、2種類の置換装置 -- 捕捉回避置換、改名、名前空間ごとの置換レムマ -- であり、各バインダーが他方に対して透明であり、3つの埋め込みの忠実性は機械化され、自動化される。
最小の埋め込みは(可算)代入範囲に対する深い妥当性を回復し、この範囲相対的な読影は、MSOの一般的な(ヘンキン型)読影と一致することが示され、標準読影は証明的に強く、理解によって観察される。
いずれの読影も最小限の埋め込みから復元され、認識された解釈でのみ異なる:これら全ては一般的な読影のためのものであり、標準の完全なモデルの基本的な部分構造のみである。
ブール閉包とグラフスキーマは、完全な2階のドメインの下に保持されるが、最小の埋め込みでは失敗し、二分法は具体化され、到達性と2色性は全会一致で否定される。
関連論文リスト
- Structuring Semantic Embeddings for Principle Evaluation: A Prototype-Guided Contrastive Learning Approach [58.15427952222424]
汎用的なテキスト埋め込みはそのようなタスクに広くデプロイされているが、意味的類似性は意味的に似ているがタスク固有の例を示すことができる。
本稿では,凍結したテキスト埋め込み上に構築された幾何正規化モジュールであるPGCL(Prototype-Guided Contrastive Learning)を紹介する。
論文 参考訳（メタデータ） (2026-08-15T13:19:25Z) - First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint) [0.08594140167290099]
Isabelle/HOLは、深層埋め込み、重量級最大浅層埋め込み、軽量の極小浅層埋め込みである。
中心的な技術的貢献は、(可算)下向きのルウェンハイム・スコレム定理の定数領域クリプケ意味論の下でのFMLの機械化である。
論文 参考訳（メタデータ） (2026-07-12T19:03:54Z) - Weave of Formal Thought [51.56484100374058]
WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。
本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。
Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
論文 参考訳（メタデータ） (2026-06-24T15:58:11Z) - LimiX-2M: Mitigating Low-Rank Collapse and Attention Bottlenecks in Tabular Foundation Models [56.999481798138625]
LimiX-2Mは2Mパラメータモデルであり、広く使われているベンチマークでTabPFN-v2とTabICLのベースラインを上回っている。
本稿では,強力なタブラル基礎モデル(TFM)のための統一トークン化・ルートフレームワークを提案する。
その結果、TFMにおける精度-効率トレードオフを改善するキーレバーとして、バリューアウェアトークン化とリードアウト整列ルーティングが強調された。
論文 参考訳（メタデータ） (2026-06-03T06:07:33Z) - TIDE: Every Layer Knows the Token Beneath the Context [21.609102126208608]
本稿では,標準トランスフォーマーを EmbeddingMemory で拡張する TIDE を提案する。
我々は、TIDEの利点を理論的かつ実証的に確立し、シングルトークンID注入に関連する問題に対処する。
論文 参考訳（メタデータ） (2026-05-07T13:16:18Z) - SAM-NER: Semantic Archetype Mediation for Zero-Shot Named Entity Recognition [50.82878172248818]
emphSemantic Archetype Mediationは中間的、領域不変なアーキタイプ空間を介してクロスドメイン転送を安定化する。
SAM-NERは、クロスドメイン設定でZS-NERベースラインを一貫して上回る。
論文 参考訳（メタデータ） (2026-05-05T12:54:17Z) - Cross-modal Full-mode Fine-grained Alignment for Text-to-Image Person Retrieval [54.90229711181207]
TIPR (Text-to-Image Person Retrieval) は、与えられたテキストクエリに基づいて、最も関連性の高い人物画像を取得することを目的としている。
TIPRの鍵となる課題は、テキストと視覚のモダリティの効果的なアライメントを達成することである。
FMFA, クロスモーダルフルモーデファインファインファインファインアライメントフレームワークを提案する。
論文 参考訳（メタデータ） (2025-09-17T07:12:05Z) - Latent Reasoning via Sentence Embedding Prediction [41.06552269338159]
本稿では,次の文の連続的な埋め込みを自動回帰予測することにより,事前訓練されたトークンレベルのLMを文空間内での操作に適応させるフレームワークを提案する。
以上の結果から,事前学習したLMは,遅延埋め込み空間内での抽象的構造的推論に効果的に移行できることが示唆された。
論文 参考訳（メタデータ） (2025-05-28T10:28:35Z) - Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。
QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
論文 参考訳（メタデータ） (2024-10-09T22:53:48Z) - Repetition Improves Language Model Embeddings [86.71985212601258]
「echo Embeddings」は、自動回帰言語モデルをアーキテクチャの変更や微調整を必要とせず、強力なテキスト埋め込みモデルに変換する。
我々のゼロショット埋め込みは、マスク付き言語モデリングトレーニングを施した双方向変換LMで得られたものとほぼ一致します。
論文 参考訳（メタデータ） (2024-02-23T17:25:10Z) - Reinforcing Semantic-Symmetry for Document Summarization [15.113768658584979]
文書要約は、長い文書を詳細な情報と正確な意味記述を備えた短いバージョンに凝縮する。
本稿では,文書要約のための新しいtextbfreinforcing stextbfemantic-textbfsymmetric Learning textbfmodelを提案する。
CNN/Daily MailとBigPatentの2つの大胆なベンチマークデータセットに対して、一連の実験が行われた。
論文 参考訳（メタデータ） (2021-12-14T17:41:37Z) - Out-of-Manifold Regularization in Contextual Embedding Space for Text
Classification [22.931314501371805]
空間の残りの部分を見つけ、正規化するための新しいアプローチを提案します。
実際に観察された単語から得られた2つの埋め込みに基づいて, アウトオブマニフォールド埋め込みを合成する。
判別器は、入力埋め込みがマニホールド内に位置するかどうかを検出するように訓練され、同時に、ジェネレーターは、容易にマニホールド外として識別できる新しい埋め込みを生成するように最適化される。
論文 参考訳（メタデータ） (2021-05-14T10:17:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。