28 件の論文
大規模言語モデルが数学オリンピックなどの競合問題では高い性能を示す一方で、現代の数学研究の深さや抽象度を反映する「FATE」という新たな代数学形式ベンチマークシリーズ（FATE-H および FATE-X）の導入により、最先端モデルが博士課程レベルの証明において極めて低い精度しか達成できず、自然言語での推論と形式化の間に大きなギャップが存在することが明らかになりました。
この論文は、-自動列の線形部分列の複雑性を研究し、自動機構築における状態数やランタイムの分析、Zantema と Bosma による最近の問いへの解答、および内部列の部分語複雑性との関係性を明らかにするものです。
本論文は、Syntax Guided Synthesis 技術と TSL（Temporal Stream Logic の有限接頭辞解釈）を組み合わせることで、ブール値抽象化の限界を超え、データ変換と時制仕様を同時に学習し、より頑健かつ効率的にリアクティブプログラムを合成する手法を提案しています。
この論文は、共有乱数を持たない分散環境における concurrent graph games において、閾値問題が NP 困難かつ実数存在論理に属し、ほぼ確実到達問題が NP 完全であることを示し、新しい論理 IRATL を提案するとともに、これらの問題に対するソルバーを実装・評価したものである。
この論文は、高次元オートマトン（HDA）の標準的な定式化に含まれる人工的なイベント順序の制約を、順序に依存しない区間 ipomset に基づく意味論によって解消し、ST トレースと hhp 双対性を ipomset 同型を通じて統一的に記述する新たな基礎を提供するものである。
この論文は、プッシュダウンオートマトンやワンカウンターオートマトンの計算における「ターン数」の決定可能性、非再帰的なトレードオフ、入力長に対する部分線形なターン数による無限の階層構造、およびその階層より緩やかに増加するターン数を必要とする言語の存在などを証明したものです。
この論文は、マルチエッジ NFA や特定の部分 DFA を用いた有限状態記述を導入し、決定性文脈自由木の同型判定問題が根付き・非根付きの両ケースにおいて NL 完全であることを示しています。
この論文は、 Walnut 定理証明器や ChatGPT 5 などのソフトウェアを活用して、整数の-表現に関する新たな性質を証明し、特に Kimberling による 2012 年の予想を解決したことを報告しています。
この論文は、形式言語理論における生成と認識の間の本質的な非対称性を、計算複雑性や曖昧さなど新たに特定された 6 つの次元から包括的に分析し、両者が拡張的には等価であるにもかかわらず操作的にどのように異なるかを明らかにしています。
この論文は、非負整数のアルファベット上の滑らかな言葉の複雑性に関するシングの予想について、偶数アルファベットで証明し、任意の二文字アルファベットで下界を示し、奇数アルファベットにおける既知の上界を改善する結果を報告しています。
本論文は、Scala 向けに Stainless 検証器を用いて実装・検証された「ZipLex」を提案し、正規表現と最長一致の性質に加え、トークン列の印刷との相互逆関数性（可逆性）を保証しつつ、従来の検証済み lexer が直面する二次時間計算量の問題を回避して線形時間での処理を実現したことを示しています。
この論文は、離散事象システムのモデルが未知である状況下で、与えられたデータセットから非ブロッキングなマーク付け制御器を設計可能かどうかを判定する「マーク付けデータ情報性」という新概念を提案し、その検証アルゴリズムや制約付きの拡張概念、および最大部分仕様を計算する手法を開発するものである。
この論文は、文法制約付きデコーディングにおいて、文法構造が到達可能性と計算コストに与える影響を理論的に解析し、構造的曖昧性コストの定量化、最適化の理論的限界、およびトランスフォーマーアーキテクチャにおける実用的な遅延バウンドを導出する。
この論文は、モア機械と状態空間モデル（SSM）の形式的な対応関係を確立し、自動機学習で得られた記号的な構造を SSM の初期化に活用することで、ランダム初期化に比べて 2〜5 倍の高速な収束と高精度な学習を実現する手法を提案しています。
本論文は、メトリック時相論理（MTL）仕様から離散・密時間両方の振る舞いに対してシーケンシャルネットワークを構築する手法を提案し、将来の時間的マーカーを用いた効率的なオンライン監視フレームワークを実現することで、既存手法よりも優れた性能と拡張性を示すものである。
本論文は、プッシュダウン型マルチエージェントシステムのモジュール検査問題について、ATL 指定では 2EXPTIME 完全、ATL* 指定では 4EXPTIME 完全であることを示し、特に後者が自然な決定問題として三重指数時間を超える複雑性を持つ稀有な例であることを明らかにしています。
この論文は、無限木に関するラムゼー型定理や類似の組合せ論的道具の研究を通じて、木代数の展開問題への応用を論じています。
この論文は、交通規則違反や衝突リスクなど多様な運転リスクを人間のようにバランスさせるため、線形時相論理（LTL）の仕様と占有測度に基づく線形計画法を組み合わせ、自律運転システムのリスク感知型制御方策を合成する手法を提案し、Carla シミュレーターによる検証でその有効性を示したものである。
この論文は、2017 年にクラーク・キンバリングが定義した 0 と 1 の列に関する彼の予想を Walnut 定理証明器を用いて証明し、その列と無限トリボナッチ語との関係、部分語の複雑さ、および臨界指数を決定するものである。
この論文は、有向サイクルにおける局所最適化問題の分散計算複雑性を完全分類し、決定論的およびランダム化 LOCAL モデルにおける 4 つの複雑性クラスを特定するだけでなく、任意の問題と近似率に対してその複雑性クラスを自動的に判定し、非同期最適の分散アルゴリズムを効率的に合成するメタアルゴリズムを提案しています。