Safety Synthesis Sans Specification

• URL: http://arxiv.org/abs/2011.07630v2
• Date: Fri, 27 Nov 2020 13:25:02 GMT
• Title: Safety Synthesis Sans Specification
• Authors: Roderick Bloem and Hana Chockler and Masoud Ebrahimi and Dana Fisman and Heinz Riener
• Abstract summary: We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that its time and query complexity is with respect to the rank of the target language, its incompatibility measure, and the maximal length of a given counterexample.
• Score: 5.874782446136914
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that its time and query complexity is polynomial with respect to the rank of the target language, its incompatibility measure, and the maximal length of a given counterexample. We report on experiments conducted with a prototype implementation.

Related papers

• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  We introduce a novel approach for traversing the problem space using task decompositions. We use the Large Language Models to plan a solution, soft-formalise the query into facts and predicates using a logic programming code. Our method allows us to compute the faithfulness of the reasoning process w.r.t. the generated code and analyse the steps of the multi-hop search without relying on external solvers.
  arXiv  Detail & Related papers  (2024-10-14T19:39:11Z)
• Optimal level set estimation for non-parametric tournament and crowdsourcing problems [49.75262185577198]
  Motivated by crowdsourcing, we consider a problem where we partially observe the correctness of the answers of $n$ experts on $d$ questions. In this paper, we assume that the matrix $M$ containing the probability that expert $i$ answers correctly to question $j$ is bi-isotonic up to a permutation of it rows and columns. We construct an efficient-time algorithm that turns out to be minimax optimal for this classification problem.
  arXiv  Detail & Related papers  (2024-08-27T18:28:31Z)
• $\texttt{LM}^\texttt{2}$: A Simple Society of Language Models Solves Complex Reasoning [22.810441504080703]
  Large Language Models (LLMS) often lose track of complex, multi-step reasoning. This paper proposes LM2 to address these challenges. LM2 modularizes the decomposition, solution, and verification into three different language models.
  arXiv  Detail & Related papers  (2024-04-02T19:23:10Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• Frontier Language Models are not Robust to Adversarial Arithmetic, or "What do I need to say so you agree 2+2=5? [88.59136033348378]
  We study the problem of adversarial arithmetic, which provides a simple yet challenging testbed for language model alignment. This problem is comprised of arithmetic questions posed in natural language, with an arbitrary adversarial string inserted before the question is complete. We show that models can be partially hardened against these attacks via reinforcement learning and via agentic constitutional loops.
  arXiv  Detail & Related papers  (2023-11-08T19:07:10Z)
• Robust Approximation Algorithms for Non-monotone $k$-Submodular Maximization under a Knapsack Constraint [0.0]
  Two deterministic approximation algorithms are presented for the problem of non-monotone $k$-submodular complexity under a knapsack constraint. Our algorithms provide constant approximation ratios within only $O(nk)$ query complexity for the non-monotone objective.
  arXiv  Detail & Related papers  (2023-09-21T12:42:52Z)
• Efficiently Learning One-Hidden-Layer ReLU Networks via Schur Polynomials [50.90125395570797]
  We study the problem of PAC learning a linear combination of $k$ ReLU activations under the standard Gaussian distribution on $mathbbRd$ with respect to the square loss. Our main result is an efficient algorithm for this learning task with sample and computational complexity $(dk/epsilon)O(k)$, whereepsilon>0$ is the target accuracy.
  arXiv  Detail & Related papers  (2023-07-24T14:37:22Z)
• Efficient Quantum State Synthesis with One Query [0.0]
  We present a time analogue quantum algorithm making a single query (in superposition) to a classical oracle. We prove that every $n$-qubit state can be constructed to within 0.01 error by an $On/n)$-size circuit over an appropriate finite gate set.
  arXiv  Detail & Related papers  (2023-06-02T17:49:35Z)
• There is no Accuracy-Interpretability Tradeoff in Reinforcement Learning for Mazes [64.05903267230467]
  Interpretability is an essential building block for trustworthiness in reinforcement learning systems. We show that in certain cases, one can achieve policy interpretability while maintaining its optimality.
  arXiv  Detail & Related papers  (2022-06-09T04:23:26Z)
• Quantum search-to-decision reductions and the state synthesis problem [0.4248594146171025]
  We show that a quantum algorithm makes queries to a classical decision oracle to output a desired quantum state. We also show that there exists a quantum-time algorithm that can generate a witness for a $mathsfQMA$ problem up to inverse precision. We also explore the more general $textitstate synthesis problem$, in which the goal is to efficiently synthesize a target state.
  arXiv  Detail & Related papers  (2021-11-04T16:52:58Z)
• Learning Languages with Decidable Hypotheses [1.2728819383164875]
  In language learning in the limit, the most common type of hypothesis is to give an enumerator for a language. This so-called $W$-index allows for naming arbitrary computably enumerable languages. We use a different system which allows for naming arbitrary decidable languages, namely programs for characteristic functions (called $C$-indices)
  arXiv  Detail & Related papers  (2020-10-15T09:27:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.