Finding Connections via Satisfiability Solving
この論文は、第一階述語論理の証明探索をさらに自動化するため、順序ベースの飽和と目標のサブゴールへの還元を組み合わせ、証明探索の構造そのものを符号化するSAT/SMTソルバに基づく新しい接続計算手法（upCoP）を提案・実装し、その理論的性質と実用性を検証するものである。
💻 Category
cs.LO
64 件の論文
Commutation Groups and State-Independent Contextuality
この論文は、パーレス・メリンのマジックスクエアに代表される状態非依存文脈性（量子非古典性）を研究するための「可換群」という代数的構造を導入し、文字列書き換え系や一般化されたパウリ群のユニタリ表現を用いて、文脈性の有無を特徴づける一般論を構築したものである。
Online Monitoring of Metric Temporal Logic using Sequential Networks
本論文は、メトリック時相論理（MTL）仕様から離散・密時間両方の振る舞いに対してシーケンシャルネットワークを構築する手法を提案し、将来の時間的マーカーを用いた効率的なオンライン監視フレームワークを実現することで、既存手法よりも優れた性能と拡張性を示すものである。
Module checking of pushdown multi-agent systems
本論文は、プッシュダウン型マルチエージェントシステムのモジュール検査問題について、ATL 指定では 2EXPTIME 完全、ATL* 指定では 4EXPTIME 完全であることを示し、特に後者が自然な決定問題として三重指数時間を超える複雑性を持つ稀有な例であることを明らかにしています。
The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness
本論文は、ステップ重複再帰関数における直接構成的測度の限界を Lean 4 で機械検証し、依存対や部分項基準に基づく射影的手法がその障壁を回避して終止性を証明できることを、TTT2 や CeTA による外部検証と組み合わせて実証しています。
MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
この論文は、グラフニューラルネットワークによる機能表現と設計統計データを組み合わせてプロパティを効率的にクラスタリングするハイブリッド手法を提案し、多プロパティ検証における有界モデル検査の性能向上を実現することを示しています。
Fusions of One-Variable First-Order Modal Logics
本論文は、等号を含まない一変数第一階述語モダリティ論理の独立融合において、Kripke 完全性と決定可能性が保存される一方、等号や非剛定数を含む場合はディオファントス方程式の符号化によりこれらが保存されないことを示し、有限モデル性は局所の場合にのみ保存されることを明らかにするとともに、S5 モダリティを共有する命題モダリティ論理の融合として一般化された保存条件を提示している。
Complete Diagrammatic Axiomatisations of Relative Entropy
本論文は、確率行列の圏を量的に拡張する視点から、Kronecker 積と直接和という 2 つのモノイダル構造に対して、相対エントロピー（KL 発散および任意次数のレニイ発散）の完全な公理系を、量的モノイダル代数の枠組みと図式言語を用いて定式化したものである。
Modal Fragments
本論文は、ポストの格子に基づく命題論理の断片の体系的研究を踏まえ、任意のモダラル式で定義される一般枠組みと、ブール関数と選択されたモダラル演算子で構成される「単純なモダラル断片」の二つの研究動向を統合し、表現力と計算複雑性、および学習可能性に関する知見を整理して未解決問題を指摘するものである。
The Complexity of the Constructive Master Modality
この論文は、基本的な構成主義的モダリティ論理とその無謬性拡張を拡張した論理とを導入し、それらがの断片との翻訳を通じて EXPTIME 完全であり指数関数的な有限モデル性を持つことを示すとともに、やの埋め込みを通じてその妥当性問題が EXPTIME に属することを証明し、Afshari らの予想を解決したものである。
Constraint Learning for Non-confluent Proof Search
本論文は、完全性を維持しつつ非連結な表計算（特に接続表計算）におけるバックトラッキングを削減するため、制約学習を適用し、実用的な削減効果を得るための制約学習言語を反復的に改良する手法を提案するものである。
On Solving String Equations via Powers and Parikh Images
この論文は、文字列のべき演算、一般化されたパラキ画像、および等式分解という 3 つの手法を組み合わせ、ニールセン変換の拡張として文字列方程式を解決する新しいアプローチを提案しています。
NL2GDS: LLM-aided interface for Open Source Chip Design
本論文は、大規模言語モデルを活用して自然言語から RTL コードおよび GDSII レイアウトを自動生成するオープンソースの ASIC 設計フレームワーク「NL2GDS」を提案し、ベンチマーク評価において面積、遅延、消費電力の大幅な削減を実現したことを示しています。
Reversible Computation with Stacks and "Reversible Management of Failures"
この論文は、計算モデルを全単射として解釈可能にするための新しい言語「SCORE」を提案し、証明支援系を用いてスタック操作が全単射であることを検証することで、計算複雑性の研究に寄与する reversible 計算モデルの構築を示しています。
Ohana trees, linear approximation and multi-types for the I-calculus: No variable gets left behind or forgotten!
本論文は、I-計算において変数の消去を禁止する制約下で、意味のない部分木や無限枝に隠れた自由変数を追跡する「Ohana 木」を導入し、これに基づくプログラム近似理論、テイラー展開との可換性定理、および変数追跡機能を備えた非空有限多重集合を用いた非冪等型システムによるモデルを構築する。
LeanTutor: Towards a Verified AI Mathematical Proof Tutor
この論文は、自然言語での円滑な対話と定理証明器による厳密な検証を両立させるため、LLM と定理証明器の長所を組み合わせた検証可能な AI 数学証明チューター「LeanTutor」のプロトタイプと、その評価用データセット「PeanoBench」を提案するものである。
The Geometry of Reasoning: Flowing Logics in Representation Space
本論文は、大規模言語モデルの推論を表現空間における幾何学的な「流れ」としてモデル化する新たな枠組みを提案し、次トークン予測のみの学習でも論理的な不変性が高次幾何学として内面化されることを実証することで、「確率的オウム」説に挑戦し、モデルやアーキテクチャに依存しない普遍的な表現法則の存在を示唆するものである。
Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
LLM の証明戦略を抽出して Rocq の定理に形式化し、CoqHammer の証明成功率を 13.41% 向上させる「Strat2Rocq」という手法を提案し、その有効性を示した。
SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification
本論文は、既存のテストベースの評価手法が見落としがちな生成 SQL と正解 SQL の差異を特定するために、形式検証エンジンを用いて両者を区別するデータベースを探索する新たな評価パイプライン「SpotIt」を提案し、BIRD データセットを用いた実験によりその有効性を示しています。
Formal that "Floats" High: Formal Verification of Floating Point Arithmetic
本論文は、抽象化の隔たりを排除し直接 RTL 間モデル検査を行うスケーラブルな手法を提案し、分割統治戦略と CEX 誘導による改良に加え、LLM 駆動の自動生成と人間による精査を組み合わせたアジェンティック AI により、浮動小数点演算の形式検証の効率性と網羅性を大幅に向上させることを示しています。