-
A Democratic Platform for Engaging with Disabled Community in Generative AI Development
Authors:
Deepak Giri,
Erin Brady
Abstract:
Artificial Intelligence (AI) systems, especially generative AI technologies are becoming more relevant in our society. Tools like ChatGPT are being used by members of the disabled community e.g., Autistic people may use it to help compose emails. The growing impact and popularity of generative AI tools have prompted us to examine their relevance within the disabled community. The design and develo…
▽ More
Artificial Intelligence (AI) systems, especially generative AI technologies are becoming more relevant in our society. Tools like ChatGPT are being used by members of the disabled community e.g., Autistic people may use it to help compose emails. The growing impact and popularity of generative AI tools have prompted us to examine their relevance within the disabled community. The design and development phases often neglect this marginalized group, leading to inaccurate predictions and unfair discrimination directed towards them. This could result from bias in data sets, algorithms, and systems at various phases of creation and implementation. This workshop paper proposes a platform to involve the disabled community while building generative AI systems. With this platform, our aim is to gain insight into the factors that contribute to bias in the outputs generated by generative AI when used by the disabled community. Furthermore, we expect to comprehend which algorithmic factors are the main contributors to the output's incorrectness or irrelevancy. The proposed platform calls on both disabled and non-disabled people from various geographical and cultural backgrounds to collaborate asynchronously and remotely in a democratic approach to decision-making.
△ Less
Submitted 26 September, 2023;
originally announced September 2023.
-
Frex: dependently-typed algebraic simplification
Authors:
Guillaume Allais,
Edwin Brady,
Nathan Corbyn,
Ohad Kammar,
Jeremy Yallop
Abstract:
We present an extensible, mathematically-structured algebraic simplification library design. We structure the library using universal algebraic concepts: a free algebra -- fral -- and a free extension -- frex -- of an algebra by a set of variables. The library's dependently-typed API guarantees simplification modules, even user-defined ones, are terminating, sound, and complete with respect to a w…
▽ More
We present an extensible, mathematically-structured algebraic simplification library design. We structure the library using universal algebraic concepts: a free algebra -- fral -- and a free extension -- frex -- of an algebra by a set of variables. The library's dependently-typed API guarantees simplification modules, even user-defined ones, are terminating, sound, and complete with respect to a well-specified class of equations. Completeness offers intangible benefits in practice -- our main contribution is the novel design. Cleanly separating between the interface and implementation of simplification modules provides two new modularity axes. First, simplification modules share thousands of lines of infrastructure code dealing with term-representation, pretty-printing, certification, and macros/reflection. Second, new simplification modules can reuse existing ones. We demonstrate this design by develo** simplification modules for monoid varieties: ordinary, commutative, and involutive. We implemented this design in the new Idris2 dependently-typed programming language, and in Agda.
△ Less
Submitted 27 June, 2023;
originally announced June 2023.
-
Exploring outlooks towards generative AI-based assistive technologies for people with Autism
Authors:
Deepak Giri,
Erin Brady
Abstract:
The last few years have significantly increased global interest in generative artificial intelligence. Deepfakes, which are synthetically created videos, emerged as an application of generative artificial intelligence. Fake news and pornographic content have been the two most prevalent negative use cases of deepfakes in the digital ecosystem. Deepfakes have some advantageous applications that expe…
▽ More
The last few years have significantly increased global interest in generative artificial intelligence. Deepfakes, which are synthetically created videos, emerged as an application of generative artificial intelligence. Fake news and pornographic content have been the two most prevalent negative use cases of deepfakes in the digital ecosystem. Deepfakes have some advantageous applications that experts in the subject have thought of in the areas of filmmaking, teaching, etc. Research on the potential of deepfakes among people with disabilities is, however, scarce or nonexistent. This workshop paper explores the potential of deepfakes as an assistive technology. We examined Reddit conversations regarding Nvdia's new videoconferencing feature which allows participants to maintain eye contact during online meetings. Through manual web scra** and qualitative coding, we found 162 relevant comments discussing the relevance and appropriateness of the technology for people with Autism. The themes identified from the qualitative codes indicate a number of concerns for technology among the autistic community. We suggest that develo** generative AI-based assistive solutions will have ramifications for human-computer interaction (HCI), and present open questions that should be investigated further in this space.
△ Less
Submitted 16 May, 2023;
originally announced May 2023.
-
Type Theory as a Language Workbench
Authors:
Jan de Muijnck-Hughes,
Guillaume Allais,
Edwin Brady
Abstract:
Language Workbenches offer language designers an expressive environment in which to create their DSLs. Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes!
We have d…
▽ More
Language Workbenches offer language designers an expressive environment in which to create their DSLs. Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes!
We have developed an exemplar DSL called Velo that showcases not only dependently typed techniques to realise and manipulate IRs, but that dependently typed languages make fine language workbenches. Velo is a simple verified language with well-typed holes and comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compiler passes. Specifically, we describe our design choices for well-typed IRs design that includes support for well-typed holes, how CSE is achieved in a well-typed setting, and how the mechanised type-soundness proof for Velo is the source of the evaluator.
△ Less
Submitted 30 January, 2023;
originally announced January 2023.
-
Model-assisted deep learning of rare extreme events from partial observations
Authors:
Anna Asch,
Ethan Brady,
Hugo Gallardo,
John Hood,
Bryan Chu,
Mohammad Farazmand
Abstract:
To predict rare extreme events using deep neural networks, one encounters the so-called small data problem because even long-term observations often contain few extreme events. Here, we investigate a model-assisted framework where the training data is obtained from numerical simulations, as opposed to observations, with adequate samples from extreme events. However, to ensure the trained networks…
▽ More
To predict rare extreme events using deep neural networks, one encounters the so-called small data problem because even long-term observations often contain few extreme events. Here, we investigate a model-assisted framework where the training data is obtained from numerical simulations, as opposed to observations, with adequate samples from extreme events. However, to ensure the trained networks are applicable in practice, the training is not performed on the full simulation data; instead we only use a small subset of observable quantities which can be measured in practice. We investigate the feasibility of this model-assisted framework on three different dynamical systems (Rossler attractor, FitzHugh-Nagumo model, and a turbulent fluid flow) and three different deep neural network architectures (feedforward, long short-term memory, and reservoir computing). In each case, we study the prediction accuracy, robustness to noise, reproducibility under repeated training, and sensitivity to the type of input data. In particular, we find long short-term memory networks to be most robust to noise and to yield relatively accurate predictions, while requiring minimal fine-tuning of the hyperparameters.
△ Less
Submitted 22 March, 2022; v1 submitted 4 November, 2021;
originally announced November 2021.
-
Idris 2: Quantitative Type Theory in Practice
Authors:
Edwin Brady
Abstract:
Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent program…
▽ More
Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. As yet, however, there has not been a full-scale programming language with which to experiment with these ideas. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types. In this paper, we introduce Idris 2, and describe how QTT has influenced its design. We give examples of the benefits of QTT in practice including: expressing which data is erased at run time, at the type level; and, resource tracking in the type system leading to type-safe concurrent programming with session types.
△ Less
Submitted 1 April, 2021;
originally announced April 2021.
-
Value-Dependent Session Design in a Dependently Typed Language
Authors:
Jan de Muijnck-Hughes,
Edwin Brady,
Wim Vanderbauwhede
Abstract:
Session Types offer a ty** discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care must be taken that values introduced in the description are used by roles that know about the value.
We present Sessions, a Resource Dependent E…
▽ More
Session Types offer a ty** discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care must be taken that values introduced in the description are used by roles that know about the value.
We present Sessions, a Resource Dependent EDSL for describing global session descriptions in the dependently typed language Idris. As we construct session descriptions the values parameterising the EDSLs' type keeps track of roles and messages they have encountered. We can use this knowledge to ensure that message values are only used by those who know the value. Sessions supports protocol descriptions that are computable, composable, higher-order, and value-dependent. We demonstrate Sessions expressiveness by describing the TCP Handshake, a multi-modal server providing echo and basic arithmetic operations, and a Higher-Order protocol that supports an authentication interaction step.
△ Less
Submitted 2 April, 2019;
originally announced April 2019.
-
Sequential decision problems, dependent types and generic solutions
Authors:
Nicola Botta,
Patrik Jansson,
Cezar Ionescu,
David R. Christiansen,
Edwin Brady
Abstract:
We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or…
▽ More
We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or combinations thereof). This level of genericity is achievable in a programming language with dependent types (we have used both Idris and Agda). Dependent types are also the means that allow us to obtain a formalization and computer-checked proof of the central component of our implementation: Bellman's principle of optimality and the associated backwards induction algorithm. The formalization clarifies certain aspects of backwards induction and, by making explicit notions such as viability and reachability, can serve as a starting point for a theory of controllability of monadic dynamical systems, commonly encountered in, e.g., climate impact research.
△ Less
Submitted 22 March, 2017; v1 submitted 23 October, 2016;
originally announced October 2016.
-
HackAttack: Game-Theoretic Analysis of Realistic Cyber Conflicts
Authors:
Erik M. Ferragut,
Andrew C. Brady,
Ethan J. Brady,
Jacob M. Ferragut,
Nathan M. Ferragut,
Max C. Wildgruber
Abstract:
Game theory is appropriate for studying cyber conflict because it allows for an intelligent and goal-driven adversary. Applications of game theory have led to a number of results regarding optimal attack and defense strategies. However, the overwhelming majority of applications explore overly simplistic games, often ones in which each participant's actions are visible to every other participant. T…
▽ More
Game theory is appropriate for studying cyber conflict because it allows for an intelligent and goal-driven adversary. Applications of game theory have led to a number of results regarding optimal attack and defense strategies. However, the overwhelming majority of applications explore overly simplistic games, often ones in which each participant's actions are visible to every other participant. These simplifications strip away the fundamental properties of real cyber conflicts: probabilistic alerting, hidden actions, unknown opponent capabilities.
In this paper, we demonstrate that it is possible to analyze a more realistic game, one in which different resources have different weaknesses, players have different exploits, and moves occur in secrecy, but they can be detected. Certainly, more advanced and complex games are possible, but the game presented here is more realistic than any other game we know of in the scientific literature. While optimal strategies can be found for simpler games using calculus, case-by-case analysis, or, for stochastic games, Q-learning, our more complex game is more naturally analyzed using the same methods used to study other complex games, such as checkers and chess. We define a simple evaluation function and ploy multi-step searches to create strategies. We show that such scenarios can be analyzed, and find that in cases of extreme uncertainty, it is often better to ignore one's opponent's possible moves. Furthermore, we show that a simple evaluation function in a complex game can lead to interesting and nuanced strategies.
△ Less
Submitted 13 November, 2015;
originally announced November 2015.
