Assured Neuro Symbolic Learning and Reasoning (DARPA) [SRI funding: 5.4M]

Jul 27, 2022
DARPA ANSR

DARPA Project Page

Abstract: To successfully incorporate autonomous systems into their missions, military operators must have confidence that those systems will operate safely and perform as intended. DARPA is motivating new thinking and approaches to artificial intelligence development to enable high levels of trust in autonomous systems through the Assured Neuro Symbolic Learning and Reasoning (ANSR) program. ANSR seeks breakthrough innovations in the form of new, hybrid AI algorithms that integrate symbolic reasoning with data-driven learning to create robust, assured, and therefore trustworthy systems. ANSR defines a system as trustworthy, if it is: Robust to domain-informed and adversarial perturbations; Supported by an assurance framework that creates and analyzes heterogenous evidence towards safety and risk assessments; and Predictable with respect to some specification and models of fitness. Advances in assurance technologies, including formal and simulation-based approaches, have helped accelerate identification of failure modes and defects of machine learning (ML) algorithms. Unfortunately, the ability to repair defects in state-of-the-art ML remains limited to retraining, which is not guaranteed to eliminate defects or to improve the generalizability of ML algorithms. Further, while the runtime assurance architecture (e.g. monitoring and recovery) ensures operational safety, frequent invocations of fallback recovery, triggered by brittleness and generalizability of ML, compromises the ability to accomplish a mission. ANSR hypothesizes that several of the limitations in ML today are a consequence of the inability to incorporate contextual and background knowledge, and treating each data set as an independent, uncorrelated input. In the real world, observations are often correlated and a product of an underlying causal mechanism, which can be modeled and understood. ANSR also posits that hybrid AI algorithms capable of acquiring and integrating symbolic knowledge and performing symbolic reasoning at scale will deliver robust inference, generalize to new situations, and provide evidence for assurance and trust. SRI is developing TrinityNS - a novel neuro-symbolic AI framework to address ANSR challenges by combining foundation models, logic programming, and multimodal generative AI techniques.

Learning Formal Methods Foundation Models LLMs
Susmit Jha
Susmit Jha
Technical Director, NuSCI

My research interests include artificial intelligence, formal methods, machine learning and dynamical systems.

Related

Publications

Concept-based Analysis of Neural Networks via Vision-Language Models
The analysis of vision-based deep neural networks (DNNs) is highly desirable but it is very challenging due to the difficulty of expressing formal specifications for vision tasks and the lack of efficient verification procedures. In this paper, we propose to leverage emerging multimodal, vision-language, foundation models (VLMs) as a lens through which we can reason about vision models. VLMs have been trained on a large body of images accompanied by their textual description, and are thus implicitly aware of high-level, human-understandable concepts describing the images. We describe a logical specification language π™²πš˜πš—πšœπš™πšŽπšŒ designed to facilitate writing specifications in terms of these concepts. To define and formally check π™²πš˜πš—πšœπš™πšŽπšŒ specifications, we build a map between the internal representations of a given vision model and a VLM, leading to an efficient verification procedure of natural-language properties for vision models. We demonstrate our techniques on a ResNet-based classifier trained on the RIVAL-10 dataset using CLIP as the multimodal model.
PDF Cite Project
Direct Amortized Likelihood Ratio Estimation
We introduce a new amortized likelihood ratio estimator for likelihood-free simulation-based inference (SBI). Our estimator is simple to train and estimates the likelihood ratio using a single forward pass of the neural estimator. Our approach directly computes the likelihood ratio between two competing parameter sets which is different from the previous approach of comparing two neural network output values. We refer to our model as the direct neural ratio estimator (DNRE). As part of introducing the DNRE, we derive a corresponding Monte Carlo estimate of the posterior. We benchmark our new ratio estimator and compare to previous ratio estimators in the literature. We show that our new ratio estimator often outperforms these previous approaches. As a further contribution, we introduce a new derivative estimator for likelihood ratio estimators that enables us to compare likelihood-free Hamiltonian Monte Carlo (HMC) with random-walk Metropolis-Hastings (MH). We show that HMC is equally competitive, which has not been previously shown. Finally, we include a novel real-world application of SBI by using our neural ratio estimator to design a quadcopter.
PDF Cite Project
Counterexample Guided Inductive Synthesis Using Large Language Models and Satisfiability Solving
Generative large language models (LLMs) with instruct training such as GPT-4 can follow human-provided instruction prompts and generate human-like responses to these prompts. Apart from natural language responses, they have also been found to be effective at generating formal artifacts such as code, plans, and logical specifications from natural language prompts. Despite their remarkably improved accuracy, these models are still known to produce factually incorrect or contextually inappropriate results despite their syntactic coherence – a phenomenon often referred to as {\em hallucinations}. This limitation makes it difficult to use these models to synthesize formal artifacts that are used in safety-critical applications. Unlike tasks such as text summarization and question-answering, bugs in code, plan, and other formal artifacts produced by LLMs can be catastrophic. We posit that we can use the satisfiability modulo theory (SMT) solvers as deductive reasoning engines to analyze the generated solutions from the LLMs, produce counterexamples when the solutions are incorrect, and provide that feedback to the LLMs exploiting the dialog capability of instruct-trained LLMs. This interaction between inductive LLMs and deductive SMT solvers can iteratively steer the LLM to generate the correct response. In our experiments, we use planning over the domain of blocks as our synthesis task for evaluating our approach. We use GPT-4, GPT3.5 Turbo, Davinci, Curie, Babbage, and Ada as the LLMs and Z3 as the SMT solver. Our method allows the user to communicate the planning problem in natural language; even the formulation of queries to SMT solvers is automatically generated from natural language. Thus, the proposed technique can enable non-expert users to describe their problems in natural language, and the combination of LLMs and SMT solvers can produce provably correct solutions.
PDF Cite Project Project
Dehallucinating Large Language Models Using Formal Methods Guided Iterative Prompting
Large language models (LLMs) such as ChatGPT have been trained to generate human-like responses to natural language prompts. LLMs use a vast corpus of text data for training, and can generate coherent and contextually relevant responses to a wide range of questions and statements. Despite this remarkable progress, LLMs are prone to hallucinations making their application to safety-critical applications such as autonomous systems difficult. The hallucinations in LLMs refer to instances where the model generates responses that are not factually accurate or contextually appropriate. These hallucinations can occur due to a variety of factors, such as the model’s lack of real-world knowledge, the influence of biased or inaccurate training data, or the model’s tendency to generate responses based on statistical patterns rather than a true understanding of the input. While these hallucinations are a nuisance in tasks such as text summarization and question-answering, they can be catastrophic when LLMs are used in autonomy-relevant applications such as planning. In this paper, we focus on the application of LLMs in autonomous systems and sketch a novel self-monitoring and iterative prompting architecture that uses formal methods to detect these errors in the LLM response automatically. We exploit the dialog capability of LLMs to iteratively steer them to responses that are consistent with our correctness specification. We report preliminary experiments that show the promise of the proposed approach on tasks such as automated planning.
PDF Cite Project Project Project
Neural SDEs for Robust and Explainable Analysis of Electromagnetic Unintended Radiated Emissions
In this paper, we present a comprehensive evaluation of the robustness and explainability of ResNet-like models in the context of Unintended Radiated Emission (URE) classification and suggest a new approach leveraging Neural Stochastic Differential Equations (SDEs) to address identified limitations. We provide an empirical demonstration of the fragility of ResNet-like models to Gaussian noise perturbations, where the model performance deteriorates sharply and its F1-score drops to near insignificance at 0.008 with a Gaussian noise of only 0.5 standard deviation. We also highlight a concerning discrepancy where the explanations provided by ResNet-like models do not reflect the inherent periodicity in the input data, a crucial attribute in URE detection from stable devices.In response to these findings, we propose a novel application of Neural SDEs to build models for URE classification that are not only robust to noise but also provide more meaningful and intuitive explanations. Neural SDE models maintain a high F1-score of 0.93 even when exposed to Gaussian noise with a standard deviation of 0.5, demonstrating superior resilience to ResNet models. Neural SDE models successfully recover the time-invariant or periodic horizontal bands from the input data, a feature that was conspicuously missing in the explanations generated by ResNet-like models. This advancement presents a small but significant step in the development of robust and interpretable models for real-world URE applications where data is inherently noisy and assurance arguments demand interpretable machine learning predictions.
PDF Cite Project Project
Responsible Reasoning with Large Language Models and the Impact of Proper Nouns
Language models with billions of parameters have shown remarkable emergent properties, including the ability to reason on unstructured data. We show that open-science multi-lingual large language models can perform the task of spatial reasoning on two or more entities with significant accuracy. A responsible large language model would perform this spatial reasoning task with the same accuracy regardless of the choice of the names of the entities over which the spatial relationships are defined. However, we show that the accuracies of contemporary large language models are impacted by the choice of proper nouns even when the underlying task ought to be independent of the choice of proper nouns. In this context, we observe that the conditional log probabilities or beam scores of open-science multi-lingual large language model predictions are not well-calibrated, and the beam scores do not discriminate well between correct and wrong responses in this context.
PDF Cite Project Project