Logic in Computer Science
New submissions
[ showing up to 2000 entries per page: fewer | more ]
New submissions for Mon, 20 May 24
- [1] arXiv:2405.10611 [pdf, ps, other]
-
Title: A Certified Proof Checker for Deep Neural Network VerificationAuthors: Remi Desmartin, Omri Isac, Ekaterina Komendantskaya, Kathrin Stark, Grant Passmore, Guy KatzSubjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Programming Languages (cs.PL)
Recent advances in the verification of deep neural networks (DNNs) have opened the way for broader usage of DNN verification technology in many application areas, including safety-critical ones. DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and imprecisions; this in turn has raised the question of trust in DNN verifiers. One prominent attempt to address this issue is enhancing DNN verifiers with the capability of producing proofs of their results that are subject to independent algorithmic certification (proof checking). Formulations of proof production and proof checking already exist on top of the state-of-the-art Marabou DNN verifier. The native implementation of the proof checking algorithm for Marabou was done in C++ and itself raised the question of trust in the code (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou proof checking algorithm in Imandra -- an industrial functional programming language and prover -- that allows us to obtain an implementation with formal guarantees, including proofs of mathematical results underlying the algorithm, such as the use of the Farkas lemma.
- [2] arXiv:2405.10887 [pdf, ps, other]
-
Title: Preservation theorems on sparse classes revisitedComments: 16 pagesSubjects: Logic in Computer Science (cs.LO); Logic (math.LO)
We revisit the work studying homomorphism preservation for first-order logic in sparse classes of structures initiated in [Atserias et al., JACM 2006] and [Dawar, JCSS 2010]. These established that first-order logic has the homomorphism preservation property in any sparse class that is monotone and addable. It turns out that the assumption of addability is not strong enough for the proofs given. We demonstrate this by constructing classes of graphs of bounded treewidth which are monotone and addable but fail to have homomorphism preservation. We also show that homomorphism preservation fails on the class of planar graphs. On the other hand, the proofs of homomorphism preservation can be recovered by replacing addability by a stronger condition of amalgamation over bottlenecks. This is analogous to a similar condition formulated for extension preservation in [Ateserias et al., SiCOMP 2008].
- [3] arXiv:2405.10894 [pdf, other]
-
Title: Labelled Well Quasi Ordered Classes of Bounded Linear Clique WidthAuthors: Aliaume LopezComments: 24 pagesSubjects: Logic in Computer Science (cs.LO)
We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is well-quasi-ordered by the induced subgraph relation in the presence of a labelling of the vertices, where the class is given by an $\mathsf{MSO}$-transduction from finite words. This study leverages tools from automata theory, and the proof scheme allows to derive a weak version of the Pouzet conjecture for classes of bounded linear clique-width. We also provide an automata based characterization of which classes of $\mathsf{NLC}$ graphs are labelled-well-quasi-ordered by the induced subgraph relation, where we recover the results of Daligault Rao and Thomass\'e by encoding the models into trees with the gap embedding relation of Dershowitz and Tzameret.
- [4] arXiv:2405.10912 [pdf, other]
-
Title: Synthesis of Temporal CausalityComments: 36th International Conference on Computer Aided Verification (CAV 2024)Subjects: Logic in Computer Science (cs.LO)
We present an automata-based algorithm to synthesize omega-regular causes for omega-regular effects on executions of a reactive system, such as counterexamples uncovered by a model checker. Our theory is a generalization of temporal causality, which has recently been proposed as a framework for drawing causal relationships between trace properties on a given trace. So far, algorithms exist only for verifying a single causal relationship and, as an extension, cause synthesis through enumeration, which is complete only for a small fragment of effect properties. This work presents the first complete cause-synthesis algorithm for the class of omega-regular effects. We show that in this case, causes are guaranteed to be omega-regular themselves and can be computed as, e.g., nondeterministic B\"uchi automata. We demonstrate the practical feasibility of this algorithm with a prototype tool and evaluate its performance for cause synthesis and cause checking.
Cross-lists for Mon, 20 May 24
- [5] arXiv:2309.07806 (cross-list from cs.FL) [pdf, other]
-
Title: Feasability of Learning Weighted Automata on a SemiringSubjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
Since the seminal work by Angluin, active learning of automata, by membership and equivalence queries, has been extensively studied and several generalisations have been developed to learn various extensions of automata. For weighted automata, restricted cases have been tackled in the literature and in this paper we chart the boundaries of the Angluin approach (using a class of hypothesis automata constructed from membership and equivalence queries) applied to learning weighted automata over a general semiring. We show precisely the theoretical limitations of this approach and classify functions with respect to how guessable they are (corresponding to the existence and abundance of solutions of certain systems of equations). We provide a syntactic description of the boundary condition for a correct hypothesis of the prescribed form to exist. Of course, from an algorithmic standpoint, knowing that (many) solutions exist need not translate into an effective algorithm to find one; we conclude with a discussion of some known conditions (and variants thereof) that suffice to ensure this, illustrating the ideas over several familiar semirings (including the natural numbers) and pose some open questions for future research.
- [6] arXiv:2405.10924 (cross-list from cs.LG) [pdf, other]
-
Title: Boosting Few-Pixel Robustness Verification via Covering Verification DesignsSubjects: Machine Learning (cs.LG); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Proving local robustness is crucial to increase the reliability of neural networks. While many verifiers prove robustness in $L_\infty$ $\epsilon$-balls, very little work deals with robustness verification in $L_0$ $\epsilon$-balls, capturing robustness to few pixel attacks. This verification introduces a combinatorial challenge, because the space of pixels to perturb is discrete and of exponential size. A previous work relies on covering designs to identify sets for defining $L_\infty$ neighborhoods, which if proven robust imply that the $L_0$ $\epsilon$-ball is robust. However, the number of neighborhoods to verify remains very high, leading to a high analysis time. We propose covering verification designs, a combinatorial design that tailors effective but analysis-incompatible coverings to $L_0$ robustness verification. The challenge is that computing a covering verification design introduces a high time and memory overhead, which is intensified in our setting, where multiple candidate coverings are required to identify how to reduce the overall analysis time. We introduce CoVerD, an $L_0$ robustness verifier that selects between different candidate coverings without constructing them, but by predicting their block size distribution. This prediction relies on a theorem providing closed-form expressions for the mean and variance of this distribution. CoVerD constructs the chosen covering verification design on-the-fly, while keeping the memory consumption minimal and enabling to parallelize the analysis. The experimental results show that CoVerD reduces the verification time on average by up to 5.1x compared to prior work and that it scales to larger $L_0$ $\epsilon$-balls.
Replacements for Mon, 20 May 24
- [7] arXiv:2301.05084 (replaced) [pdf, other]
-
Title: Local consistency as a reduction between constraint satisfaction problemsSubjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC)
- [8] arXiv:2310.08779 (replaced) [pdf, ps, other]
-
Title: A Completeness Theorem for Probabilistic Regular ExpressionsComments: Accepted for publication at LICS. Full version of the paper containing omitted proofsSubjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)
- [9] arXiv:2310.09542 (replaced) [pdf, other]
-
Title: The Treewidth Boundedness Problem for an Inductive Separation Logic of RelationsSubjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)
- [10] arXiv:2312.03579 (replaced) [pdf, ps, other]
-
Title: The Implication Problem for Functional Dependencies and Variants of Marginal Distribution EquivalencesAuthors: Minna HirvonenComments: 23 pages, improved version after reviewer comments, results unchangedSubjects: Logic in Computer Science (cs.LO)
- [11] arXiv:2404.16061 (replaced) [pdf, ps, other]
-
Title: Dynamic Many Valued Logic Systems in Theoretical EconomicsAuthors: Daniel LuSubjects: Logic in Computer Science (cs.LO); Theoretical Economics (econ.TH)
- [12] arXiv:2309.09231 (replaced) [pdf, ps, other]
-
Title: ATM: a Logic for Quantitative Security Properties on Attack TreesSubjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO)
[ showing up to 2000 entries per page: fewer | more ]
Disable MathJax (What is MathJax?)
Links to: arXiv, form interface, find, cs, recent, 2405, contact, help (Access key information)