Formal mathematics is the discipline of translating mathematics into a programming language in which any statement can be unequivocally checked by a computer. Mathematicians and computer scientists have spent decades of painstaking formalization efforts developing languages such as Coq, HOL, and Lean. Machine learning research has converged on these formal math corpora and given rise to an assortment of methodologies to aid in interactive and automated theorem proving. However, these papers have primarily focused on one method, for one proof task, in one language. This paper introduces EvoGPT-f: a novel evolutionary framework for the first systematic quantitative analysis of the differential machine learnability of five formal math corpora (Lean 3, Lean 4, Coq, HOL 4, HOL Light) using four tokenization methods (character, word-level, Byte Pair Encoding and StarCoder tokenizer). This paper does not put to rest the question of the "best" or "easiest" language to learn. Rather, this framework and preliminary findings begin to illuminate the differential machine learnability of these languages, offering a foundation to forge more systematic quantitative and qualitative comparative research across communities.

Expert demonstrations have proven an easy way to indirectly specify complex tasks. Recent algorithms even support extracting unambiguous formal specifications, e.g. deterministic finite automata (DFA), from demonstrations. Unfortunately, these techniques are generally not sample efficient. In this work, we introduce $L^*LM$, an algorithm for learning DFAs from both demonstrations and natural language. Due to the expressivity of natural language, we observe a significant improvement in the data efficiency of learning DFAs from expert demonstrations. Technically, $L^*LM$ leverages large language models to answer membership queries about the underlying task. This is then combined with recent techniques for transforming learning from demonstrations into a sequence of labeled example learning problems. In our experiments, we observe the two modalities complement each other, yielding a powerful few-shot learner.

Many tasks can be easily solved using machine learning techniques. However, some tasks cannot readily be solved using statistical models, requiring a symbolic approach instead. Program induction is one of the ways that such tasks can be solved by means of capturing an interpretable and generalizable algorithm through training. However, contemporary approaches to program induction are not sophisticated enough to readily be applied to various types of tasks as they tend to be formulated as a single, all-encompassing model, usually parameterized by neural networks. In an attempt to make program induction a viable solution for many scenarios, we propose a framework for learning parameterized programs via search gradients using evolution strategies. This formulation departs from traditional program induction as it allows for the programmer to impart task-specific code to the program 'sketch', while also enjoying the benefits of accelerated learning through end-to-end gradient-based optimization.

An important aim of this paper is to convey some basics of mathematical logic to the legal community working with Artificial Intelligence. After analysing what AI is, we decide to delimit ourselves to rule-based AI leaving Neural Networks and Machine Learning aside. Rule based AI allows for Formal methods which are described in a rudimentary form. We will then see how mathematical logic interacts with legal rule-based AI practice. We shall see how mathematical logic imposes limitations and complications to AI applications. We classify the limitations and interactions between mathematical logic and legal AI in three categories: logical, computational and mathematical. The examples to showcase the interactions will largely come from European traffic regulations. The paper closes off with some reflections on how and where AI could be used and on basic mechanisms that shape society.

In academia, a growing body of research investigates the role of human values in designing ethical AI [12, 31, 74, 90]. Indeed, one of our leading AI research luminaries, Stuart Russell, believes the overarching goal of AI should change from "intelligence" to "intelligence provably aligned with human values" [74]. This call to arms gave birth to the value alignment problem. This challenge of engineering values into AI in response to the value alignment problem has resulted in a range of research areas: how human values can be learnt [43, 44, 45, 91]; how individual values can be aggregated to the level of groups [41]; how arguments that explicitly reference values can be made [7]; how decision making can be value-driven [14, 17, 21]; how online institutions can ensure value-aligned behaviours in hybrid communities [56, 57]; and how norms are selected or synthesised to maximise value-alignment [55, 80, 83]. Yet despite these efforts, no formal model of values exists today that provides a concrete foundational platform from which data structures and algorithms can be designed to build AI architectures that address the valuealignment problem. In response, we propose such a model built on the following guiding principles: 1) we employ a formal language to be precise about modelling values and related concepts [23, 47]; 2) we construct the formal components of this model to provide the foundations for the data structures and algorithmic design that will enable value-based reasoning; 3) we design the model to be agnostic on any specific implementation of values, though we do provide example implementation scenarios to illustrate the model's ubiquity and practical applicability; 4) we set out the model to subsume and relate to established concepts in AI research as much as possible; 5) we provide illustrative examples of building data structures and algorithms enabling value-based reasoning taken from our ongoing research applied to real-world use cases; 6) we ensure the model draws upon the wealth of work from within social psychology and explicitly demonstrate the grounding of our model within this research; and

Everyday we increasingly rely on machine learning models to automate and support high-stake tasks and decisions. This growing presence means that humans are now constantly interacting with machine learning-based systems, training and using models everyday. Several different techniques in computer science literature account for the human interaction with machine learning systems, but their classification is sparse and the goals varied. This survey proposes a taxonomy of Hybrid Decision Making Systems, providing both a conceptual and technical framework for understanding how current computer science literature models interaction between humans and machines.

We present MIPS, a novel method for program synthesis based on automated mechanistic interpretability The goal of the present paper is to take a modest first step in of neural networks trained to perform this direction by presenting and testing MIPS (Mechanistic-the desired task, auto-distilling the learned algorithm Interpretability-based Program Synthesis), a fully automated into Python code. We test MIPS on a benchmark method that can distill simple learned algorithms of 62 algorithmic tasks that can be learned from neural networks into Python code. The rest of this by an RNN and find it highly complementary to paper is organized as follows. After reviewing prior work in GPT-4: MIPS solves 32 of them, including 13 Section II, we present our method in Section III, test it on a that are not solved by GPT-4 (which also solves benchmark in Section IV and summarize our conclusions in 30). MIPS uses an integer autoencoder to convert Section V. the RNN into a finite state machine, then applies Boolean or integer symbolic regression to capture

Neurosymbolic AI combines the interpretability, parsimony, and explicit reasoning of classical symbolic approaches with the statistical learning of data-driven neural approaches. Models and policies that are simultaneously differentiable and interpretable may be key enablers of this marriage. This paper demonstrates three pathways to implementing such models and policies in a real-world reinforcement learning setting. Specifically, we study a broad class of neural networks that build interpretable semantics directly into their architecture. We reveal and highlight both the potential and the essential difficulties of combining logic, simulation, and learning. One lesson is that learning benefits from continuity and differentiability, but classical logic is discrete and non-differentiable. The relaxation to real-valued, differentiable representations presents a trade-off; the more learnable, the less interpretable. Another lesson is that using logic in the context of a numerical simulation involves a non-trivial mapping from raw (e.g., real-valued time series) simulation data to logical predicates. Some open questions this note exposes include: What are the limits of rule-based controllers, and how learnable are they? Do the differentiable interpretable approaches discussed here scale to large, complex, uncertain systems? Can we truly achieve interpretability? We highlight these and other themes across the three approaches.

However, the complexity and versatility of modern AI systems calls for a unified framework to assess their trustworthiness, which cannot The probabilistic formal verification (PFV) of be captured by a single evaluation metric or formal property. AI systems is in its infancy. So far, approaches This papers aims to introduce such a framework. We have been limited to ad-hoc algorithms for specific show how by leveraging the Weighted Model Integration classes of models and/or properties. We propose (WMI) [Belle et al., 2015] formalism, it is possible to devise a unifying framework for the PFV of AI systems a unified formulation for the probabilistic verification of based on Weighted Model Integration (WMI), combinatorial AI systems. Broadly speaking, WMI is the which allows to frame the problem in very general task of computing probabilities of arbitrary combinations terms. Crucially, this reduction enables the verification of logical and algebraic constraints given a structured joint of many properties of interest, like fairness, distribution over both continuous and discrete variables.

Machine learning models that automate decision-making are increasingly being used in consequential areas such as loan approvals, pretrial bail approval, hiring, and many more. Unfortunately, most of these models are black-boxes, i.e., they are unable to reveal how they reach these prediction decisions. A need for transparency demands justification for such predictions. An affected individual might also desire explanations to understand why a decision was made. Ethical and legal considerations may further require informing the individual of changes in the input attribute that could be made to produce a desirable outcome. This paper focuses on the latter problem of automatically generating counterfactual explanations. We propose a framework Counterfactual Generation with s(CASP) (CFGS) that utilizes answer set programming (ASP) and the s(CASP) goal-directed ASP system to automatically generate counterfactual explanations from rules generated by rule-based machine learning (RBML) algorithms. In our framework, we show how counterfactual explanations are computed and justified by imagining worlds where some or all factual assumptions are altered/changed. More importantly, we show how we can navigate between these worlds, namely, go from our original world/scenario where we obtain an undesired outcome to the imagined world/scenario where we obtain a desired/favourable outcome.