Commutativity and Kleisli laws of codensity monads of probability measures
本論文は、確率測度のコデシティモノイドの構成を用いて、Giry モノイドへのクライスリ法則の存在やその普遍性、およびマルコフ圏理論に関連するモノイダル性やアフィン性の条件を導き出し、特にラドンモノイドの自由代数のテンソル積をデイ合成積で記述し、Giry モノイドのモノイダル性が標準ボレル空間に限定される理由を明らかにする。
💻 Category
cs.LO
64 件の論文
Dependent Directed Wiring Diagrams for Composing Instantaneous Systems
この論文は、入出力が瞬間的に依存するメリー機械や在庫・フロー図を構成するための「依存付き有向配線図」のオペラドを導入し、その代数的構造とメリー機械への意味論的対応を確立するものである。
A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
本論文は、大規模プログラムの形式検証におけるスケーラビリティ課題を解決するため、静的解析と大規模言語モデル（LLM）を協調させ、潜在的なランタイムエラーに基づいて検証単位を優先的に選定・合成するモジュール型フレームワーク「Preguss」を提案し、千行を超える実世界プログラムにおいて人間の手間を最大 88.9% 削減する高い自動化を実現したことを示しています。
Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits
本論文は、量子ビットの抽象化とビットベクトル論理を用いることで、1,024 個の位相量子ビットを含む大規模な量子位相推定回路の機能的正当性を効率的に検証するスケーラブルな形式検証手法を提案しています。
A Simple Constructive Bound on Circuit Size Change Under Truth Table Perturbation
この論文は、真理値表の一点変更による回路サイズの増大がで抑えられることを明示的に示し、一般のハミング距離への拡張やにおける AIG 基底での厳密な検証を通じて、この境界がでタイトであることを確認したものである。
Declarative Scenario-based Testing with RoadLogic
本論文は、自律走行車のシナリオベーステストにおいて、宣言的な OpenSCENARIO 仕様を実行可能なシミュレーションに変換し、多様な行動バリエーションを体系的に生成するオープンソースツール「RoadLogic」を提案し、その有効性を示すものである。
d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries
この論文は、SMT 問題を事前計算された理論レマと組み合わせることで d-DNNF へ変換し、既存の命題論理推論器を用いて多項式時間で SMT クエリを処理する汎用的なフレームワークを初めて提案し、その有効性を実証したものです。
BemaGANv2: Discriminator Combination Strategies for GAN-based Vocoders in Long-Term Audio Generation
本論文は、AMP モジュールと新規の Multi-Envelope Discriminator を導入し、長尺音声生成における時間的整合性や周期性のモデル化を強化した GAN ベースのボコーダ「BemaGANv2」を提案し、各種識別器の組み合わせ戦略を客観的・主観的指標を用いて体系的に評価したものである。
FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
大規模言語モデルが数学オリンピックなどの競合問題では高い性能を示す一方で、現代の数学研究の深さや抽象度を反映する「FATE」という新たな代数学形式ベンチマークシリーズ（FATE-H および FATE-X）の導入により、最先端モデルが博士課程レベルの証明において極めて低い精度しか達成できず、自然言語での推論と形式化の間に大きなギャップが存在することが明らかになりました。
Classifying covering types in homotopy type theory
この論文は、ホモトピー型理論において被覆空間と基本群のガロア対応を形式化し、n 次元への一般化を提案するとともに、レンズ空間の被覆の分類やポアンカレのホモロジー球の構成を通じてその手法の有効性を示しています。
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
本論文は、Syntax Guided Synthesis 技術と TSL（Temporal Stream Logic の有限接頭辞解釈）を組み合わせることで、ブール値抽象化の限界を超え、データ変換と時制仕様を同時に学習し、より頑健かつ効率的にリアクティブプログラムを合成する手法を提案しています。
Three Fixed-Dimension Satisfiability Semantics for Quantum Logic: Implications and an Explicit Separator
この論文は、固定次元のヒルベルト空間における量子論理の 3 つの充足可能性意味論（標準的、大域的交換、局所的部分ブール）を比較し、標準的意味論では充足可能だが他の 2 つでは充足不可能な明示的な分離式「SEP-1」を構成することで、それらの充足可能性クラスが厳密に異なることを示しています。
Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
この論文は、複数の LLM ベースのコーディングエージェントが、証明タスクに対して動的に提案や報酬（バウンティ）を設定し、証明アシスタントと直接対話しながら分散的に協力して代数トポロジーの大規模な自動形式化を実現する、市場原理に基づく新しいアプローチを提案するものである。
Twitch: Learning Abstractions for Equational Theorem Proving
この論文は、失敗した証明や成功した証明から自動的に「抽象化（項パターン）」を学習するツール「Twitch」を提案し、これを等式定理証明器「Twee」に統合することで、TPTP の問題において 12 の難問を解決し、多くの問題で大幅な高速化を実現したことを報告しています。
LLM2SMT: Building an SMT Solver with Zero Human-Written Code
この論文は、人間のコードを一切書かずに LLM コーディングエージェントが QF_UF 形式の完全な SMT ソルバーを構築し、その性能が SMT-LIB ベンチマークで競合するレベルであることを示したケーススタディです。
Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
この論文は、大規模言語モデルを対話相手として専門家が自らのコミットメントを精査・明確化する「Elenchus」という対話システムを提案し、それを Hlobil と Brandom の非単調論理 NMMS にマッピングすることで、W3C の PROV-O Ontology の設計根拠を対話から形式化し、推論まで一貫して統合する手法を示しています。
Learning to Rank the Initial Branching Order of SAT Solvers
この論文は、グラフニューラルネットワークを用いて SAT ソルバの初期分岐順序を学習・予測する手法を提案し、ランダムおよび疑似産業ベンチマークで大幅な高速化を実現したが、動的ヒューリスティックが初期値を上書きしやすく予測が困難な複雑な産業インスタンスでは効果が限定的であることを示しています。
Sketch-Oriented Databases
この論文は、有限極限スケッチを用いてデータベースのパラダイムを形式化する「スケッチ指向データベース」という枠組みを提案し、グラフ特徴の統一的な表現や経路推論、そしてモジュール化とスケーラビリティを可能にする「スタッタリングスケッチ」の導入を通じて、データベース理論の一般化と拡張を示しています。
A method for the automated generation of proof exercises with comparable levels of proving complexity
この論文は、離散数学の証明問題の難易度を制御し、教育現場での自動化を可能にするため、入力された問題と証明規則に基づいて同等の証明複雑性を持つ証明問題を自動的に生成する手法を提案している。
Proceedings Eighth International Conference on Applied Category Theory
2025 年 6 月にフロリダ大学で開催された「第 8 回応用圏論国際会議（ACT2025）」の議事録は、コンピュータサイエンスから量子計算まで多岐にわたる分野からの寄稿を収録したものです。