Logic & Formal Reasoning
Guided Sketch-Based Program Induction by Search Gradients
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.
Le Nozze di Giustizia. Interactions between Artificial Intelligence, Law, Logic, Language and Computation with some case studies in Traffic Regulations and Health Care
Joosten, Joost J., García, Manuela Montoya
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.
Modelling Human Values for AI Reasoning
Osman, Nardine, d'Inverno, Mark
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
AI, Meet Human: Learning Paradigms for Hybrid Decision Making Systems
Punzi, Clara, Pellungrini, Roberto, Setzu, Mattia, Giannotti, Fosca, Pedreschi, Dino
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.
Opening the AI black box: program synthesis via mechanistic interpretability
Michaud, Eric J., Liao, Isaac, Lad, Vedang, Liu, Ziming, Mudide, Anish, Loughridge, Chloe, Guo, Zifan Carl, Kheirkhah, Tara Rezaei, Vukelić, Mateja, Tegmark, Max
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
Three Pathways to Neurosymbolic Reinforcement Learning with Interpretable Model and Policy Networks
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.
A Unified Framework for Probabilistic Verification of AI Systems via Weighted Model Integration
Morettin, Paolo, Passerini, Andrea, Sebastiani, Roberto
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.
Counterfactual Generation with Answer Set Programming
Dasgupta, Sopam, Shakerin, Farhad, Arias, Joaquín, Salazar, Elmer, Gupta, Gopal
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.
DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models
Shao, Zhihong, Wang, Peiyi, Zhu, Qihao, Xu, Runxin, Song, Junxiao, Zhang, Mingchuan, Li, Y. K., Wu, Y., Guo, Daya
Mathematical reasoning poses a significant challenge for language models due to its complex and structured nature. In this paper, we introduce DeepSeekMath 7B, which continues pre-training DeepSeek-Coder-Base-v1.5 7B with 120B math-related tokens sourced from Common Crawl, together with natural language and code data. DeepSeekMath 7B has achieved an impressive score of 51.7% on the competition-level MATH benchmark without relying on external toolkits and voting techniques, approaching the performance level of Gemini-Ultra and GPT-4. Self-consistency over 64 samples from DeepSeekMath 7B achieves 60.9% on MATH. The mathematical reasoning capability of DeepSeekMath is attributed to two key factors: First, we harness the significant potential of publicly available web data through a meticulously engineered data selection pipeline. Second, we introduce Group Relative Policy Optimization (GRPO), a variant of Proximal Policy Optimization (PPO), that enhances mathematical reasoning abilities while concurrently optimizing the memory usage of PPO.
Extended Version of: On the Structural Hardness of Answer Set Programming: Can Structure Efficiently Confine the Power of Disjunctions?
Hecher, Markus, Kiesel, Rafael
Answer Set Programming (ASP) is a generic problem modeling and solving framework with a strong focus on knowledge representation and a rapid growth of industrial applications. So far, the study of complexity resulted in characterizing hardness and determining their sources, fine-grained insights in the form of dichotomy-style results, as well as detailed parameterized complexity landscapes. Unfortunately, for the well-known parameter treewidth disjunctive programs require double-exponential runtime under reasonable complexity assumptions. This quickly becomes out of reach. We deal with the classification of structural parameters for disjunctive ASP on the program's rule structure (incidence graph). First, we provide a polynomial kernel to obtain single-exponential runtime in terms of vertex cover size, despite subset-minimization being not represented in the program's structure. Then we turn our attention to strictly better structural parameters between vertex cover size and treewidth. Here, we provide double-exponential lower bounds for the most prominent parameters in that range: treedepth, feedback vertex size, and cliquewidth. Based on this, we argue that unfortunately our options beyond vertex cover size are limited. Our results provide an in-depth hardness study, relying on a novel reduction from normal to disjunctive programs, trading the increase of complexity for an exponential parameter compression.