skip to main content


Title: Weighted Transducers for Robustness Verification
Automata theory provides us with fundamental notions such as languages, membership, emptiness and inclusion that in turn allow us to specify and verify properties of reactive systems in a useful manner. However, these notions all yield "yes"/"no" answers that sometimes fall short of being satisfactory answers when the models being analyzed are imperfect, and the observations made are prone to errors. To address this issue, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so robustly. We present notions of robustness that place a metric on words, thus providing a natural notion of distance between words. Such a metric naturally leads to a topological neighborhood of words and languages, leading to quantitative and robust versions of the membership, emptiness and inclusion problems. More generally, we consider weighted transducers to model the cost of errors. Such a transducer models neighborhoods of words by providing the cost of rewriting a word into another. The main contribution of this work is to study robustness verification problems in the context of weighted transducers. We provide algorithms for solving the robust and quantitative versions of the membership and inclusion problems while providing useful motivating case studies including approximate pattern matching problems to detect clinically relevant events in a large type-1 diabetes dataset.  more » « less
Award ID(s):
1836900
NSF-PAR ID:
10193725
Author(s) / Creator(s):
; ; ; ;
Date Published:
Journal Name:
Leibniz international proceedings in informatics
Volume:
171
ISSN:
1868-8969
Page Range / eLocation ID:
17:1--17:21
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Jovanovic, Jelena ; Chounta, Irene-Angelica ; Uhomoibhi, James ; McLaren, Bruce (Ed.)
    Computer-supported education studies can perform two important roles. They can allow researchers to gather important data about student learning processes, and they can help students learn more efficiently and effectively by providing automatic immediate feedback on what the students have done so far. The evaluation of student work required for both of these roles can be relatively easy in domains like math, where there are clear right answers. When text is involved, however, automated evaluations become more difficult. Natural Language Processing (NLP) can provide quick evaluations of student texts. However, traditional neural network approaches require a large amount of data to train models with enough accuracy to be useful in analyzing student responses. Typically, educational studies collect data but often only in small amounts and with a narrow focus on a particular topic. BERT-based neural network models have revolutionized NLP because they are pre-trained on very large corpora, developing a robust, contextualized understanding of the language. Then they can be “fine-tuned” on a much smaller set of data for a particular task. However, these models still need a certain base level of training data to be reasonably accurate, and that base level can exceed that provided by educational applications, which might contain only a few dozen examples. In other areas of artificial intelligence, such as computer vision, model performance on small data sets has been improved by “data augmentation” — adding scaled and rotated versions of the original images to the training set. This has been attempted on textual data; however, augmenting text is much more difficult than simply scaling or rotating images. The newly generated sentences may not be semantically similar to the original sentence, resulting in an improperly trained model. In this paper, we examine a self-augmentation method that is straightforward and shows great improvements in performance with different BERT-based models in two different languages and on two different tasks that have small data sets. We also identify the limitations of the self-augmentation procedure. 
    more » « less
  2. Bouajjani, A ; Holík, L. ; Wu, Z. (Ed.)
    This paper presents an optimization based framework to automate system repair against omega-regular properties. In the proposed formalization of optimal repair, the systems are represented as Kripke structures, the properties as omega-regular languages, and the repair space as repair machines—weighted omega-regular transducers equipped with Büchi conditions—that rewrite strings and associate a cost sequence to these rewritings. To translate the resulting cost-sequences to easily interpretable payoffs, we consider several aggregator functions to map cost sequences to numbers—including limit superior, supremum, discounted-sum, and average-sum—to define quantitative cost semantics. The problem of optimal repair, then, is to determine whether traces from a given system can be rewritten to satisfy an omega-regular property when the allowed cost is bounded by a given threshold. We also consider the dual challenge of impair verification that assumes that the rewritings are resolved adversarially under some given cost restriction, and asks to decide if all traces of the system satisfy the specification irrespective of the rewritings. With a negative result to the impair verification problem, we study the problem of designing a minimal mask of the Kripke structure such that the resulting traces satisfy the specifications despite the threshold-bounded impairment. We dub this problem as the mask synthesis problem. This paper presents automata-theoretic solutions to repair synthesis, impair verification, and mask synthesis problem for limit superior, supremum, discounted-sum, and average-sum cost semantics. 
    more » « less
  3. Bilinguals occasionally produce language intrusion errors (inadvertent translations of the intended word), especially when attempting to produce function word targets, and often when reading aloud mixed-language paragraphs. We investigate whether these errors are due to a failure of attention during speech planning, or failure of monitoring speech output by classifying errors based on whether and when they were corrected, and investigating eye movement behaviour surrounding them. Prior research on this topic has primarily tested alphabetic languages (e.g., Spanish–English bilinguals) in which part of speech is confounded with word length, which is related to word skipping (i.e., decreased attention). Therefore, we tested 29 Chinese–English bilinguals whose languages differ in orthography, visually cueing language membership, and for whom part of speech (in Chinese) is less confounded with word length. Despite the strong orthographic cue, Chinese–English bilinguals produced intrusion errors with similar effects as previously reported (e.g., especially with function word targets written in the dominant language). Gaze durations did differ by whether errors were made and corrected or not, but these patterns were similar for function and content words and therefore cannot explain part of speech effects. However, bilinguals regressed to words produced as errors more often than to correctly produced words, but regressions facilitated correction of errors only for content, not for function words. These data suggest that the vulnerability of function words to language intrusion errors primarily reflects automatic retrieval and failures of speech monitoring mechanisms from stopping function versus content word errors after they are planned for production.

     
    more » « less
  4. Abstract

    Machine learning (ML) has been applied to space weather problems with increasing frequency in recent years, driven by an influx of in-situ measurements and a desire to improve modeling and forecasting capabilities throughout the field. Space weather originates from solar perturbations and is comprised of the resulting complex variations they cause within the numerous systems between the Sun and Earth. These systems are often tightly coupled and not well understood. This creates a need for skillful models with knowledge about the confidence of their predictions. One example of such a dynamical system highly impacted by space weather is the thermosphere, the neutral region of Earth’s upper atmosphere. Our inability to forecast it has severe repercussions in the context of satellite drag and computation of probability of collision between two space objects in low Earth orbit (LEO) for decision making in space operations. Even with (assumed) perfect forecast of model drivers, our incomplete knowledge of the system results in often inaccurate thermospheric neutral mass density predictions. Continuing efforts are being made to improve model accuracy, but density models rarely provide estimates of confidence in predictions. In this work, we propose two techniques to develop nonlinear ML regression models to predict thermospheric density while providing robust and reliable uncertainty estimates: Monte Carlo (MC) dropout and direct prediction of the probability distribution, both using the negative logarithm of predictive density (NLPD) loss function. We show the performance capabilities for models trained on both local and global datasets. We show that the NLPD loss provides similar results for both techniques but the direct probability distribution prediction method has a much lower computational cost. For the global model regressed on the Space Environment Technologies High Accuracy Satellite Drag Model (HASDM) density database, we achieve errors of approximately 11% on independent test data with well-calibrated uncertainty estimates. Using an in-situ CHAllenging Minisatellite Payload (CHAMP) density dataset, models developed using both techniques provide test error on the order of 13%. The CHAMP models—on validation and test data—are within 2% of perfect calibration for the twenty prediction intervals tested. We show that this model can also be used to obtain global density predictions with uncertainties at a given epoch.

     
    more » « less
  5. Introduction and Theoretical Frameworks Our study draws upon several theoretical foundations to investigate and explain the educational experiences of Black students majoring in ME, CpE, and EE: intersectionality, critical race theory, and community cultural wealth theory. Intersectionality explains how gender operates together with race, not independently, to produce multiple, overlapping forms of discrimination and social inequality (Crenshaw, 1989; Collins, 2013). Critical race theory recognizes the unique experiences of marginalized groups and strives to identify the micro- and macro-institutional sources of discrimination and prejudice (Delgado & Stefancic, 2001). Community cultural wealth integrates an asset-based perspective to our analysis of engineering education to assist in the identification of factors that contribute to the success of engineering students (Yosso, 2005). These three theoretical frameworks are buttressed by our use of Racial Identity Theory, which expands understanding about the significance and meaning associated with students’ sense of group membership. Sellers and colleagues (1997) introduced the Multidimensional Model of Racial Identity (MMRI), in which they indicated that racial identity refers to the “significance and meaning that African Americans place on race in defining themselves” (p. 19). The development of this model was based on the reality that individuals vary greatly in the extent to which they attach meaning to being a member of the Black racial group. Sellers et al. (1997) posited that there are four components of racial identity: 1. Racial salience: “the extent to which one’s race is a relevant part of one’s self-concept at a particular moment or in a particular situation” (p. 24). 2. Racial centrality: “the extent to which a person normatively defines himself or herself with regard to race” (p. 25). 3. Racial regard: “a person’s affective or evaluative judgment of his or her race in terms of positive-negative valence” (p. 26). This element consists of public regard and private regard. 4. Racial ideology: “composed of the individual’s beliefs, opinions and attitudes with respect to the way he or she feels that the members of the race should act” (p. 27). The resulting 56-item inventory, the Multidimensional Inventory of Black Identity (MIBI), provides a robust measure of Black identity that can be used across multiple contexts. Research Questions Our 3-year, mixed-method study of Black students in computer (CpE), electrical (EE) and mechanical engineering (ME) aims to identify institutional policies and practices that contribute to the retention and attrition of Black students in electrical, computer, and mechanical engineering. Our four study institutions include historically Black institutions as well as predominantly white institutions, all of which are in the top 15 nationally in the number of Black engineering graduates. We are using a transformative mixed-methods design to answer the following overarching research questions: 1. Why do Black men and women choose and persist in, or leave, EE, CpE, and ME? 2. What are the academic trajectories of Black men and women in EE, CpE, and ME? 3. In what way do these pathways vary by gender or institution? 4. What institutional policies and practices promote greater retention of Black engineering students? Methods This study of Black students in CpE, EE, and ME reports initial results from in-depth interviews at one HBCU and one PWI. We asked students about a variety of topics, including their sense of belonging on campus and in the major, experiences with discrimination, the impact of race on their experiences, and experiences with microaggressions. For this paper, we draw on two methodological approaches that allowed us to move beyond a traditional, linear approach to in-depth interviews, allowing for more diverse experiences and narratives to emerge. First, we used an identity circle to gain a better understanding of the relative importance to the participants of racial identity, as compared to other identities. The identity circle is a series of three concentric circles, surrounding an “inner core” representing one’s “core self.” Participants were asked to place various identities from a provided list that included demographic, family-related, and school-related identities on the identity circle to reflect the relative importance of the different identities to participants’ current engineering education experiences. Second, participants were asked to complete an 8-item survey which measured the “centrality” of racial identity as defined by Sellers et al. (1997). Following Enders’ (2018) reflection on the MMRI and Nigrescence Theory, we chose to use the measure of racial centrality as it is generally more stable across situations and best “describes the place race holds in the hierarchy of identities an individual possesses and answers the question ‘How important is race to me in my life?’” (p. 518). Participants completed the MIBI items at the end of the interview to allow us to learn more about the participants’ identification with their racial group, to avoid biasing their responses to the Identity Circle, and to avoid potentially creating a stereotype threat at the beginning of the interview. This paper focuses on the results of the MIBI survey and the identity circles to investigate whether these measures were correlated. Recognizing that Blackness (race) is not monolithic, we were interested in knowing the extent to which the participants considered their Black identity as central to their engineering education experiences. Combined with discussion about the identity circles, this approach allowed us to learn more about how other elements of identity may shape the participants’ educational experiences and outcomes and revealed possible differences in how participants may enact various points of their identity. Findings For this paper, we focus on the results for five HBCU students and 27 PWI students who completed the MIBI and identity circle. The overall MIBI average for HBCU students was 43 (out of a possible 56) and the overall MIBI scores ranged from 36-51; the overall MIBI average for the PWI students was 40; the overall MIBI scores for the PWI students ranged from 24-51. Twenty-one students placed race in the inner circle, indicating that race was central to their identity. Five placed race on the second, middle circle; three placed race on the third, outer circle. Three students did not place race on their identity circle. For our cross-case qualitative analysis, we will choose cases across the two institutions that represent low, medium and high MIBI scores and different ranges of centrality of race to identity, as expressed in the identity circles. Our final analysis will include descriptive quotes from these in-depth interviews to further elucidate the significance of race to the participants’ identities and engineering education experiences. The results will provide context for our larger study of a total of 60 Black students in engineering at our four study institutions. Theoretically, our study represents a new application of Racial Identity Theory and will provide a unique opportunity to apply the theories of intersectionality, critical race theory, and community cultural wealth theory. Methodologically, our findings provide insights into the utility of combining our two qualitative research tools, the MIBI centrality scale and the identity circle, to better understand the influence of race on the education experiences of Black students in engineering. 
    more » « less