计算机科学中的逻辑
查看 最近的 文章
显示 2025年07月11日， 星期五 新的列表
- [1] arXiv:2507.07208 (交叉列表自 math.LO) [中文pdf, pdf, 其他]
-
标题： 2-范畴论方法在具有计算公理的依赖类型理论语义中的应用标题： A 2-categorical approach to the semantics of dependent type theory with computation axioms评论： 64页，欢迎留言主题： 逻辑 (math.LO) ; 计算机科学中的逻辑 (cs.LO) ; 范畴论 (math.CT)
公理类型理论是一种没有计算规则的依赖类型理论。 通常表征这些规则的项等式判断被替换为计算公理，即由同伦类型定义的额外项判断。 本文致力于从高范畴论的角度提供其语义的有效描述：鉴于将可意类型形成器编码为一维范畴术语和性质的挑战，即使对于公理类型形成器来说这一挑战依然存在，我们采用理查德·加纳在依赖类型二维研究中的方法。 我们证明，公理理论的类型形成器可以编码为自然的二维范畴理论数据，通过称为显示映射二维范畴的二维范畴模型来呈现公理类型理论的语义。 在公理情况下，加纳为解释可意类型形成器所确定的二维范畴要求被放宽。 因此，我们获得了一个公理理论语义的表述，该表述推广了加纳对可意情况的表述。 我们的主要结果指出，在显示映射二维范畴中对公理理论的解释是定义良好的，并且具有合理性属性。 我们利用这一事实提供了一个语义证明，说明可意同伦类型的计算规则在公理类型理论中是不可接受的。 这是通过重新审视霍夫曼和斯特赖彻的群胚模型实现的，该模型认为公理同伦类型但不认为可意同伦类型。
Axiomatic type theory is a dependent type theory without computation rules. The term equality judgements that usually characterise these rules are replaced by computation axioms, i.e., additional term judgements that are typed by identity types. This paper is devoted to providing an effective description of its semantics, from a higher categorical perspective: given the challenge of encoding intensional type formers into 1-dimensional categorical terms and properties, a challenge that persists even for axiomatic type formers, we adopt Richard Garner's approach in the 2-dimensional study of dependent types. We prove that the type formers of axiomatic theories can be encoded into natural 2-dimensional category theoretic data, obtaining a presentation of the semantics of axiomatic type theory via 2-categorical models called display map 2-categories. In the axiomatic case, the 2-categorical requirements identified by Garner for interpreting intensional type formers are relaxed. Therefore, we obtain a presentation of the semantics of the axiomatic theory that generalises Garner's one for the intensional case. Our main result states that the interpretation of axiomatic theories within display map 2-categories is well-defined and enjoys the soundness property. We use this fact to provide a semantic proof that the computation rule of intensional identity types is not admissible in axiomatic type theory. This is achieved via a revisitation of Hofmann and Streicher's groupoid model that believes axiomatic identity types but does not believe intensional ones.
- [2] arXiv:2507.07217 (交叉列表自 cs.AI) [中文pdf, pdf, html, 其他]
-
标题： 神经符号特征提取用于识别供应链中的强迫劳动标题： Neurosymbolic Feature Extraction for Identifying Forced Labor in Supply Chains主题： 人工智能 (cs.AI) ; 机器学习 (cs.LG) ; 计算机科学中的逻辑 (cs.LO)
供应链网络是复杂的系统，分析起来具有挑战性; 当供应链中涉及非法活动时，如假冒零件、强迫劳动或人口贩卖，这个问题会更加严重。 虽然机器学习（ML）可以在像供应链这样的复杂系统中找到模式，但传统的ML技术需要大量的训练数据集。 然而，非法供应链的特点是数据非常稀疏，可用的数据往往（故意地）被破坏或不可靠，以隐藏活动的性质。 我们需要能够自动检测与这种非法活动相关的新的模式，即使是在复杂甚至时间序列数据上，而无需大量训练数据集。 我们探讨了神经符号方法，用于在供应链中识别非法活动的实例，并比较了从准确描述当局发现的非法活动的新闻文章中手动和自动特征提取的有效性。 我们提出了一种问题树方法，用于查询大型语言模型（LLM），以识别和量化文章的相关性。 这使得可以系统地评估人类和机器对供应链中与强迫劳动相关的新闻文章分类之间的差异。
Supply chain networks are complex systems that are challenging to analyze; this problem is exacerbated when there are illicit activities involved in the supply chain, such as counterfeit parts, forced labor, or human trafficking. While machine learning (ML) can find patterns in complex systems like supply chains, traditional ML techniques require large training data sets. However, illicit supply chains are characterized by very sparse data, and the data that is available is often (purposely) corrupted or unreliable in order to hide the nature of the activities. We need to be able to automatically detect new patterns that correlate with such illegal activity over complex, even temporal data, without requiring large training data sets. We explore neurosymbolic methods for identifying instances of illicit activity in supply chains and compare the effectiveness of manual and automated feature extraction from news articles accurately describing illicit activities uncovered by authorities. We propose a question tree approach for querying a large language model (LLM) to identify and quantify the relevance of articles. This enables a systematic evaluation of the differences between human and machine classification of news articles related to forced labor in supply chains.
- [3] arXiv:2507.07576 (交叉列表自 cs.AI) [中文pdf, pdf, html, 其他]
-
标题： 关于可信的基于规则的模型和解释标题： On Trustworthy Rule-Based Models and Explanations主题： 人工智能 (cs.AI) ; 机器学习 (cs.LG) ; 计算机科学中的逻辑 (cs.LO)
机器学习（ML）中感兴趣的任务之一是为ML模型做出的预测提供解释。 此外，在被认为高风险的领域中，解释的严谨性至关重要。 确实，错误的解释可能会误导人类决策者。 因此，即使可解释性被公认为一个难以捉摸的概念，所谓的可解释模型在ML和数据挖掘（DM）的高风险应用中被普遍使用。 规则基础的ML模型就是这种情况，它们包括决策树、图示、集合和列表。 本文将解释与规则基础ML模型中众所周知的不良特性联系起来，这些特性包括负重叠和多种形式的冗余。 本文开发了用于分析这些规则系统不良特性的算法，并得出结论，众所周知且广泛使用的规则基础ML模型学习工具将导致表现出一个或多个负面特性的规则集。
A task of interest in machine learning (ML) is that of ascribing explanations to the predictions made by ML models. Furthermore, in domains deemed high risk, the rigor of explanations is paramount. Indeed, incorrect explanations can and will mislead human decision makers. As a result, and even if interpretability is acknowledged as an elusive concept, so-called interpretable models are employed ubiquitously in high-risk uses of ML and data mining (DM). This is the case for rule-based ML models, which encompass decision trees, diagrams, sets and lists. This paper relates explanations with well-known undesired facets of rule-based ML models, which include negative overlap and several forms of redundancy. The paper develops algorithms for the analysis of these undesired facets of rule-based systems, and concludes that well-known and widely used tools for learning rule-based ML models will induce rule sets that exhibit one or more negative facets.
- [4] arXiv:2507.07942 (交叉列表自 cs.DM) [中文pdf, pdf, html, 其他]
-
标题： CSP非冗余性的重要性标题： The Richness of CSP Non-redundancy评论： 82页，5图主题： 离散数学 (cs.DM) ; 计算复杂性 (cs.CC) ; 计算机科学中的逻辑 (cs.LO) ; 组合数学 (math.CO)
在约束满足问题（CSP）领域，如果一个子句的满足由满足所有其他子句所隐含，则该子句被称为冗余的。 CSP$(P)$的一个实例被称为非冗余的，如果它不包含任何冗余子句。 谓词$P$的非冗余性（NRD）是作为变量数量$n$的函数，在CSP$(P)$的非冗余实例中子句的最大数量。 最近的研究进展表明，非冗余性与计算机科学和数学中的许多其他重要问题密切相关，包括稀疏化、核化、查询复杂性、通用代数和极值组合学。 鉴于非冗余性是这些重要问题的一个交汇点，本文的核心目标是更深入地理解非冗余性。 我们第一个主要结果表明，对于每个有理数$r \ge 1$，存在一个有限的CSP谓词$P$，使得$P$的非冗余性为$\Theta(n^r)$。 我们的第二个主要结果探讨了由Brakensiek和Guruswami [STOC 2025]首次提出的条件非冗余性概念。 我们通过将这些非冗余性问题与极值组合学中高环长图的结构相联系，对所有二元谓词（即对两个变量的约束）的条件非冗余性进行了完全分类。 受这些具体结果的启发，我们基于Carbonnel [CP 2022]的工作，发展了一个条件非冗余性的代数理论。 作为该代数理论的应用，我们重新审视了Mal'tsev嵌入的概念，这是目前用于证明一个谓词具有线性非冗余性的最一般技术。 例如，我们提供了第一个具有Mal'tsev嵌入的谓词示例，该示例不能归因于阿贝尔群的结构，而是归因于量子泡利群的结构。
In the field of constraint satisfaction problems (CSP), a clause is called redundant if its satisfaction is implied by satisfying all other clauses. An instance of CSP$(P)$ is called non-redundant if it does not contain any redundant clause. The non-redundancy (NRD) of a predicate $P$ is the maximum number of clauses in a non-redundant instance of CSP$(P)$, as a function of the number of variables $n$. Recent progress has shown that non-redundancy is crucially linked to many other important questions in computer science and mathematics including sparsification, kernelization, query complexity, universal algebra, and extremal combinatorics. Given that non-redundancy is a nexus for many of these important problems, the central goal of this paper is to more deeply understand non-redundancy. Our first main result shows that for every rational number $r \ge 1$, there exists a finite CSP predicate $P$ such that the non-redundancy of $P$ is $\Theta(n^r)$. Our second main result explores the concept of conditional non-redundancy first coined by Brakensiek and Guruswami [STOC 2025]. We completely classify the conditional non-redundancy of all binary predicates (i.e., constraints on two variables) by connecting these non-redundancy problems to the structure of high-girth graphs in extremal combinatorics. Inspired by these concrete results, we build off the work of Carbonnel [CP 2022] to develop an algebraic theory of conditional non-redundancy. As an application of this algebraic theory, we revisit the notion of Mal'tsev embeddings, which is the most general technique known to date for establishing that a predicate has linear non-redundancy. For example, we provide the first example of predicate with a Mal'tsev embedding that cannot be attributed to the structure of an Abelian group, but rather to the structure of the quantum Pauli group.
交叉提交 (展示 4 之 4 条目 )
- [5] arXiv:2407.17947 (替换) [中文pdf, pdf, 其他]
-
标题： 图同构的超临界尺寸-宽度树状解析权衡标题： Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism评论： 36页，2张图表，一篇被接受发表于MFCS 2025的论文的完整版本主题： 计算机科学中的逻辑 (cs.LO) ; 计算复杂性 (cs.CC)
我们研究图同构在树形解析演算中的反驳复杂性。 Torán 和 Wörz（TOCL 2023）表明，当且仅当两个图可以在（$k+1$）变量的一阶逻辑（FO$^{k+1}$）中被区分时，它们才存在宽度为$k$的解析反驳，因此也可以通过$k$维 Weisfeiler-Leman 算法的无计数变体来区分。 虽然 DAG 形式的宽度为$k$的解析反驳的大小最多为$n^k$，但树形反驳可能要大得多。 我们证明存在阶为n的图，其同构性可以在窄宽度$k$下被反驳，但只能在树状大小$2^{\Omega(n^{k/2})}$下被反驳。 这是一个超临界权衡，其中限制一个参数（窄宽度）会导致另一个参数（大小）超过其最坏情况。 该大小下界是公式大小的超指数级，并改进了Razborov（JACM 2016）的相关超临界宽度与树状大小权衡。 为了证明我们的结果，我们开发了FO$^k$的一种新的$k$-棋子EF游戏，以类似证明复杂性中的Prover-Delayer游戏的方式来推理树状反驳大小。 我们在Grohe、Lichter、Neuen和Schweitzer（FOCS 2023）引入的压缩CFI图的一个修改变体上分析了这个游戏。 利用Janett、Nordström和Pang（未发表的手稿）最近改进的鲁棒压缩CFI构造，我们得到了关于宽度$k$的类似界限（而不是更强但不常见的窄宽度），并使结果更加鲁棒。
We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Tor\'an and W\"orz (TOCL 2023) showed that there is a resolution refutation of narrow width $k$ for two graphs if and only if they can be distinguished in ($k+1$)-variable first-order logic (FO$^{k+1}$) and hence by a count-free variant of the $k$-dimensional Weisfeiler-Leman algorithm. While DAG-like narrow width $k$ resolution refutations have size at most $n^k$, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width $k$ but only in tree-like size $2^{\Omega(n^{k/2})}$. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical width versus tree-like size trade-off by Razborov (JACM 2016). To prove our result, we develop a new variant of the $k$-pebble EF-game for FO$^k$ to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on a modified variant of the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer (FOCS 2023). Using a recent improved robust compressed CFI construction of Janett, Nordstr\"om, and Pang (unpublished manuscript), we obtain a similar bound for width $k$ (instead of the stronger but less common narrow width) and make the result more robust.
- [6] arXiv:2408.16102 (替换) [中文pdf, pdf, 其他]
-
标题： 超越单子和双积：直觉逻辑中并行性的统一解释标题： Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic评论： 15页加附录主题： 计算机科学中的逻辑 (cs.LO) ; 范畴论 (math.CT)
传统上，对lambda演算中并行性和代数结构的建模方法通常依赖于单子——如Moggi的框架——或者依赖于丰富的范畴结构，如双积——如在线性逻辑中使用。 在本工作中，我们提出了一种最小的替代方案，在直觉命题逻辑的框架内捕捉并行性和加权并行性（线性组合），而无需使用单子或假设双积的存在。 我们引入了两种lambda演算：一种是并行lambda演算和一种代数lambda演算，它们都扩展了完整的命题直觉逻辑。 它们的语义是在两个范畴中给出的：${\mathbf{Mag}_{\mathbf{Set}}}$，其对象是幕群，箭头是$\mathbf{Set}$中的函数；以及${\mathbf{AMag}^{\mathcal{S}}_{\mathbf{Set}}}$，其对象是作用幕群。 解决的关键技术挑战是在存在并行和代数运算符的情况下解释析取。 由于在我们的最小设置中通常的余积结构不可用，我们提出了一种基于不相交并集和笛卡尔积的并集的新集合论解释。 这使得可以为这两种演算构建声音且充分的模型。 我们的结果为在直觉逻辑中建模并行性和代数效应提供了一个统一且结构轻量的框架，为超越传统的单子或线性逻辑方法提供了新的途径。
Traditional approaches to modelling parallelism and algebraic structure in lambda calculi often rely on monads -- as in Moggi's framework -- or on rich categorical structures such as biproducts -- as used in linear logic. In this work, we propose a minimal alternative that captures both parallelism and weighted parallelism (linear combinations) within the setting of intuitionistic propositional logic, without resorting to monads or assuming the existence of biproducts. We introduce two lambda calculi: a parallel lambda calculus and an algebraic lambda calculus, both extending full propositional intuitionistic logic. Their semantics are given in two categories: ${\mathbf{Mag}_{\mathbf{Set}}}$, whose objects are magmas and arrows are functions in $\mathbf{Set}$; and ${\mathbf{AMag}^{\mathcal{S}}_{\mathbf{Set}}}$, whose objects are action magmas. The key technical challenge addressed is the interpretation of disjunction in the presence of parallel and algebraic operators. Since the usual coproduct structure is unavailable in our minimal setting, we propose a novel set-theoretic interpretation based on the union of the disjoint union and the Cartesian product. This allows for the construction of sound and adequate models for both calculi. Our results offer a unified and structurally lightweight framework for modelling parallelism and algebraic effects in intuitionistic logic, opening the way to alternatives beyond the traditional monadic or linear logic approaches.
- [7] arXiv:2503.04512 (替换) [中文pdf, pdf, 其他]
-
标题： 并发概率程序的误差界模块化推理（扩展版）标题： Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal主题： 计算机科学中的逻辑 (cs.LO) ; 编程语言 (cs.PL)
我们提出Coneris，这是第一个高阶并发分离逻辑，用于推理具有高阶状态的高阶并发概率程序的错误概率界限。 为了支持对并发（非概率）程序模块进行模块化推理，最先进的程序逻辑通过逻辑原子性的概念在逻辑内部内化了线性化的经典概念。 Coneris将这一思想扩展到概率并发程序模块。 因此，Coneris通过在逻辑中捕获一种新的随机逻辑原子性概念，支持对概率并发模块进行模块化推理。 为此，Coneris利用预采样磁带和一种新的概率更新模态来描述在线性化点状态如何被概率地改变。 我们通过较小的合成示例和较大的案例研究来展示这种方法。 所有呈现的结果，包括元理论，都已在Rocq证明助手和Iris分离逻辑框架中形式化。
We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules, state-of-the-art program logics internalize the classic notion of linearizability within the logic through the concept of logical atomicity. Coneris extends this idea to probabilistic concurrent program modules. Thus Coneris supports modular reasoning about probabilistic concurrent modules by capturing a novel notion of randomized logical atomicity within the logic. To do so, Coneris utilizes presampling tapes and a novel probabilistic update modality to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies. All of the presented results, including the meta-theory, have been mechanized in the Rocq proof assistant and the Iris separation logic framework
- [8] arXiv:2506.18439 (替换) [中文pdf, pdf, html, 其他]
-
标题： 量子下推系统的模型检测计算复杂性标题： Computational Complexity of Model-Checking Quantum Pushdown Systems评论： [v5] 语法错误已修复；欢迎提出评论。arXiv管理员注：与arXiv:1405.4806、arXiv:2209.10517有大量文本重叠。主题： 计算机科学中的逻辑 (cs.LO) ; 计算复杂性 (cs.CC)
在本文中，我们从计算复杂性的角度研究模型检测量子下推系统的問題。 我们得出了以下同样重要且有趣的新的结果： 我们首先将{\it 概率下推系统}和{\it 马尔可夫链}的概念扩展到它们的量子对应物，并研究是否有必要定义{\it 概率计算树逻辑}的量子对应物来描述{\it 量子马尔可夫链}的概率和分支时间性质。 我们研究其模型检测问题，并表明对{\it 无状态量子下推系统 (qBPA)}与{\it 概率计算树逻辑（PCTL）}的模型检测通常是不可判定的，即不存在对{\it 无状态量子下推系统}与{\it 概率计算树逻辑}进行模型检测的算法。 我们接着研究在何种情况下存在对{\it 无状态量子下推系统}的模型检测算法，并表明对{\it 无状态量子下推系统}与{\it 有界概率计算树逻辑}（bPCTL）的模型检测问题是可判定的，进一步表明该问题属于$NP$-hard。 我们的归约首次是从{\it 有界邮递员问题 对应问题}进行的，这是一个著名的$NP$-完全问题。
In this paper, we study the problem of model-checking quantum pushdown systems from a computational complexity point of view. We arrive at the following equally important, interesting new results: We first extend the notions of the {\it probabilistic pushdown systems} and {\it Markov chains} to their quantum analogues and investigate the question of whether it is necessary to define a quantum analogue of {\it probabilistic computational tree logic} to describe the probabilistic and branching-time properties of the {\it quantum Markov chain}. We study its model-checking question and show that model-checking of {\it stateless quantum pushdown systems (qBPA)} against {\it probabilistic computational tree logic (PCTL)} is generally undecidable, i.e., there exists no algorithm for model-checking {\it stateless quantum pushdown systems} against {\it probabilistic computational tree logic}. We then study in which case there exists an algorithm for model-checking {\it stateless quantum pushdown systems} and show that the problem of model-checking {\it stateless quantum pushdown systems} against {\it bounded probabilistic computational tree logic} (bPCTL) is decidable, and further show that this problem is in $NP$-hard. Our reduction is from the {\it bounded Post Correspondence Problem} for the first time, a well-known $NP$-complete problem.
- [9] arXiv:2501.05765 (替换) [中文pdf, pdf, html, 其他]
-
标题： AI伦理形式验证的规范时间逻辑标题： Deontic Temporal Logic for Formal Verification of AI Ethics主题： 人工智能 (cs.AI) ; 计算机科学中的逻辑 (cs.LO)
确保在人工智能（AI）系统日益普遍和影响力扩大的情况下保持伦理行为是全球关注的重大问题。 在AI伦理中使用形式化方法可能是指定和验证AI系统伦理行为的关键方法。 本文提出了一种基于义务逻辑的形式化方法，用于定义和评估AI系统的伦理行为，重点在于系统级规范，为实现这一重要目标做出贡献。 它引入了公理和定理来捕捉与公平性和可解释性相关的伦理要求。 该形式化方法结合了时间算子，以推理AI系统随时间变化的伦理行为。 作者通过评估现实世界中的COMPAS和贷款预测AI系统的伦理来验证这种形式化方法的有效性。 使用义务逻辑公式对COMPAS和贷款预测系统的各种伦理属性进行编码，从而可以使用自动定理证明器验证这些系统是否满足定义的属性。 形式化验证表明，这两个系统未能满足与公平性和非歧视相关的某些关键伦理属性，这证明了所提出的形式化方法在识别现实世界AI应用中潜在伦理问题方面的有效性。
Ensuring ethical behavior in Artificial Intelligence (AI) systems amidst their increasing ubiquity and influence is a major concern the world over. The use of formal methods in AI ethics is a possible crucial approach for specifying and verifying the ethical behavior of AI systems. This paper proposes a formalization based on deontic logic to define and evaluate the ethical behavior of AI systems, focusing on system-level specifications, contributing to this important goal. It introduces axioms and theorems to capture ethical requirements related to fairness and explainability. The formalization incorporates temporal operators to reason about the ethical behavior of AI systems over time. The authors evaluate the effectiveness of this formalization by assessing the ethics of the real-world COMPAS and loan prediction AI systems. Various ethical properties of the COMPAS and loan prediction systems are encoded using deontic logical formulas, allowing the use of an automated theorem prover to verify whether these systems satisfy the defined properties. The formal verification reveals that both systems fail to fulfill certain key ethical properties related to fairness and non-discrimination, demonstrating the effectiveness of the proposed formalization in identifying potential ethical issues in real-world AI applications.