Logically Sound Arguments for the Effectiveness of ML Safety Measures

• URL: http://arxiv.org/abs/2111.02649v1
• Date: Thu, 4 Nov 2021 06:09:34 GMT
• Title: Logically Sound Arguments for the Effectiveness of ML Safety Measures
• Abstract summary: We investigate the issues of achieving sufficient rigor in the arguments for the safety of machine learning functions. We sharpen the metric of imprecise pedestrian localization by associating it with the safety goal. We then propose a semi-formal assurance case for arguing the effectiveness of the post-processor.
• Score: 0.1657441317977376
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We investigate the issues of achieving sufficient rigor in the arguments for the safety of machine learning functions. By considering the known weaknesses of DNN-based 2D bounding box detection algorithms, we sharpen the metric of imprecise pedestrian localization by associating it with the safety goal. The sharpening leads to introducing a conservative post-processor after the standard non-max-suppression as a counter-measure. We then propose a semi-formal assurance case for arguing the effectiveness of the post-processor, which is further translated into formal proof obligations for demonstrating the soundness of the arguments. Applying theorem proving not only discovers the need to introduce missing claims and mathematical concepts but also reveals the limitation of Dempster-Shafer's rules used in semi-formal argumentation.

Related papers

• Autoformalizing Argumentative Material Inferences [26.35292656634472]
  We develop an autoformalization for argumentative material inference as guard completion.<n>GUARD yields significant improvements in verified-faithful.<n>We show that the symbolic soft critique and the explicit assumption layer account for most of these gains.
  arXiv  Detail & Related papers  (2026-09-15T11:05:26Z)
• Game Hopping in Lean [5.623680633781937]
  We present HOPSCOTCH, a Lean 4 framework for mechanizing sound, game-based cryptographic proofs.<n>Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm.<n>We illustrate the framework with formalized proofs of the IND-CCA security of encrypt-then-MAC, the security of ElGamal encryption from DDH, the implication from one-time secrecy to public-key IND-CPA security, and the GGM pseudorandom-function construction.
  arXiv  Detail & Related papers  (2026-08-06T16:52:16Z)
• Formal Verification of Probing Security via Conditional Independence [0.14323566945483493]
  Side-channel attacks are a major threat to the security of cryptosystems.<n>Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification.<n>We propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic.
  arXiv  Detail & Related papers  (2026-05-22T07:34:38Z)
• ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning [0.0]
  The large language models (LLMs) might produce a persuasive argument within mathematical and logical fields.<n>Lean and Coq have rigorous reliability by ensuring that syntactic and semantic statements only accept statements that can pass all the syntactic and semantic steps in the program.<n>This paper presents a hybrid pipeline where an LLM generates a typed proof sketch in a compact DSL and a lightweight trusted kernel expands the sketch into explicit proof obligations.
  arXiv  Detail & Related papers  (2026-04-07T19:33:54Z)
• Project Ariadne: A Structural Causal Framework for Auditing Faithfulness in LLM Agents [0.0]
  We introduce textbfProject Ariadne, a novel XAI framework to audit the causal integrity of agentic reasoning.<n>Unlike existing interpretability methods that rely on surface-level textual similarity, Project Ariadne performs textbfhard interventions ($do$-calculus) on intermediate reasoning nodes.<n>Our empirical evaluation of state-of-the-art models reveals a persistent textitFaithfulness Gap.
  arXiv  Detail & Related papers  (2026-01-05T18:05:29Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  Modern language models (LMs) exhibit strong deductive reasoning capabilities, yet standard evaluations emphasize correctness while overlooking a key aspect of human-like reasoning: efficiency.<n>We propose a framework for assessing LM reasoning efficiency through the lens of logic programming.
  arXiv  Detail & Related papers  (2025-10-29T15:30:31Z)
• Extending Prediction-Powered Inference through Conformal Prediction [2.7532313761753713]
  Many applications require strong properties besides valid inference, such as privacy, robustness or validity under continuous distribution shifts.<n>We resolve this issue by connecting prediction-powered inference with conformal prediction.<n>We instantiate our procedure for the inference of means, Z- and M-estimation, as well as e-values and e-value-based procedures.
  arXiv  Detail & Related papers  (2025-10-17T19:09:07Z)
• MPC in the Quantum Head (or: Superposition-Secure (Quantum) Zero-Knowledge) [19.71357898702801]
  We present a generalization of the MPC-in-the-head paradigm to the quantum setting.<n>We propose a new approach to build zero-knowledge protocols where security holds even against a verifier that can obtain a superposition of transcripts.
  arXiv  Detail & Related papers  (2025-06-28T17:43:32Z)
• Verification-Guided Falsification for Safe RL via Explainable Abstraction and Risk-Aware Exploration [8.246285288584625]
  We propose a hybrid framework that integrates explainability, model checking, and risk-guided falsification to achieve both rigor and coverage.<n>Our approach begins by constructing a human-interpretable abstraction of the RL policy using Comprehensible Abstract Policy Summarization (CAPS)<n>If no violation is detected, we cannot conclude satisfaction due to potential limitation in the abstraction and coverage of the offline dataset.
  arXiv  Detail & Related papers  (2025-06-04T00:54:01Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  We introduce a novel problem formulation called Abstract DNN-Verification, which verifies a hierarchical structure of unsafe outputs.<n>By leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the formal verification process.<n>Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches.
  arXiv  Detail & Related papers  (2025-05-08T13:29:46Z)
• NLP Verification: Towards a General Methodology for Certifying Robustness [9.897538432223714]
  We discuss the technical challenge of semantic generalisability of verified subspaces. We propose a general methodology to analyse the effect of the embedding gap. We propose the metric of falsifiability of semantic subspaces as another fundamental metric to be reported as part of the NLP verification pipeline.
  arXiv  Detail & Related papers  (2024-03-15T09:43:52Z)
• CASA: Causality-driven Argument Sufficiency Assessment [79.13496878681309]
  We propose CASA, a zero-shot causality-driven argument sufficiency assessment framework. PS measures how likely introducing the premise event would lead to the conclusion when both the premise and conclusion events are absent. Experiments on two logical fallacy detection datasets demonstrate that CASA accurately identifies insufficient arguments.
  arXiv  Detail & Related papers  (2024-01-10T16:21:18Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• Information-Theoretic Safe Exploration with Gaussian Processes [89.31922008981735]
  We consider a sequential decision making task where we are not allowed to evaluate parameters that violate an unknown (safety) constraint. Most current methods rely on a discretization of the domain and cannot be directly extended to the continuous case. We propose an information-theoretic safe exploration criterion that directly exploits the GP posterior to identify the most informative safe parameters to evaluate.
  arXiv  Detail & Related papers  (2022-12-09T15:23:58Z)
• Safe Exploration Method for Reinforcement Learning under Existence of Disturbance [1.1470070927586016]
  We deal with a safe exploration problem in reinforcement learning under the existence of disturbance. We propose a safe exploration method that uses partial prior knowledge of a controlled object and disturbance. We illustrate the validity and effectiveness of the proposed method through numerical simulations of an inverted pendulum and a four-bar parallel link robot manipulator.
  arXiv  Detail & Related papers  (2022-09-30T13:00:33Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)
• Quantifying Robustness to Adversarial Word Substitutions [24.164523751390053]
  Deep-learning-based NLP models are found to be vulnerable to word substitution perturbations. We propose a formal framework to evaluate word-level robustness. metric helps us figure out why state-of-the-art models like BERT can be easily fooled by a few word substitutions.
  arXiv  Detail & Related papers  (2022-01-11T08:18:39Z)
• Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Technical Report) [15.150938933215906]
  How comprehensible a proof is depends not only on the employed calculus, but also on the properties of the particular proof. We aim for general results that hold for wide classes of calculi and measures.
  arXiv  Detail & Related papers  (2021-04-27T12:34:13Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  We develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference. Our approach was able to verify and produce examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods.
  arXiv  Detail & Related papers  (2020-12-21T10:03:44Z)
• Semantic Security for Quantum Wiretap Channels [68.24747267214373]
  We consider the problem of semantic security via classical-quantum and quantum wiretap channels. We use explicit constructions to transform a non-secure code into a semantically secure code, achieving capacity by means of biregular irreducible functions.
  arXiv  Detail & Related papers  (2020-01-16T09:55:49Z)
• Quantum-secure message authentication via blind-unforgeability [74.7729810207187]
  We propose a natural definition of unforgeability against quantum adversaries called blind unforgeability. This notion defines a function to be predictable if there exists an adversary who can use "partially blinded" access to predict values. We show the suitability of blind unforgeability for supporting canonical constructions and reductions.
  arXiv  Detail & Related papers  (2018-03-10T05:31:38Z)

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.