Autoformalization is the task of translating natural language materials into machine-verifiable formalisations. Progress in autoformalization research is hindered by the lack of a sizeable dataset consisting of informal-formal pairs expressing the same essence. Existing methods tend to circumvent this challenge by manually curating small corpora or using few-shot learning with large language models. But these methods suffer from data scarcity and formal language acquisition difficulty. In this work, we create $\texttt{MMA}$, a large, flexible, multilingual, and multi-domain dataset of informal-formal pairs, by using a language model to translate in the reverse direction, that is, from formal mathematical statements into corresponding informal ones. Experiments show that language models fine-tuned on $\texttt{MMA}$ produce $16-18\%$ of statements acceptable with minimal corrections on the $\texttt{miniF2F}$ and $\texttt{ProofNet}$ benchmarks, up from $0\%$ with the base model. We demonstrate that fine-tuning on multilingual formal data results in more capable autoformalization models even when deployed on monolingual tasks.

We propose a new approach to formally describing the requirement for statistical inference and checking whether a program uses the statistical method appropriately. Specifically, we define belief Hoare logic (BHL) for formalizing and reasoning about the statistical beliefs acquired via hypothesis testing. This program logic is sound and relatively complete with respect to a Kripke model for hypothesis tests. We demonstrate by examples that BHL is useful for reasoning about practical issues in hypothesis testing. In our framework, we clarify the importance of prior beliefs in acquiring statistical beliefs through hypothesis testing, and discuss the whole picture of the justification of statistical inference inside and outside the program logic.

This paper explores the integration of neural networks with logic programming, addressing the longstanding challenges of combining the generalization and learning capabilities of neural networks with the precision of symbolic logic. Traditional attempts at this integration have been hampered by difficulties in initial data acquisition, the reliability of undertrained networks, and the complexity of reusing and augmenting trained models. To overcome these issues, we introduce the COOL (Constraint Object-Oriented Logic) programming language, an innovative approach that seamlessly combines logical reasoning with neural network technologies. COOL is engineered to autonomously handle data collection, mitigating the need for user-supplied initial data. It incorporates user prompts into the coding process to reduce the risks of undertraining and enhances the interaction among models throughout their lifecycle to promote the reuse and augmentation of networks. Furthermore, the foundational principles and algorithms in COOL's design and its compilation system could provide valuable insights for future developments in programming languages and neural network architectures.

As a result, many tasks that one would traditionally attribute to being done by a human being are being performed by machine learning (ML) and artificial intelligence (AI) based models. Hence it is not surprising to see machine learning models being deployed in areas where historically, due to the nature of the tasks, it would require the involvement of a human, e.g., getting a loan/ receiving a bail judgment. Unfortunately, many of these state-of-the-art machine learning or artificial intelligence-based systems are so complex that we are unable to understand why they made such a decision. This lack of clarity contributes to such models being viewed as a black box whose content/logic is unknown. A natural consequence of the increasing involvement of machine learning models in decisionmaking processes is that these decisions either directly or indirectly impact individuals.

Given the intractably large size of the space of proofs, any model that is capable of general deductive reasoning must generalize to proofs of greater complexity. Recent studies have shown that large language models (LLMs) possess some abstract deductive reasoning ability given chain-of-thought prompts. However, they have primarily been tested on proofs using modus ponens or of a specific size, and from the same distribution as the in-context examples. To measure the general deductive reasoning ability of LLMs, we test on a broad set of deduction rules and measure their ability to generalize to more complex proofs from simpler demonstrations from multiple angles: depth-, width-, and compositional generalization. To facilitate systematic exploration, we construct a new synthetic and programmable reasoning dataset that enables control over deduction rules and proof complexity. Our experiments on four LLMs of various sizes and training objectives show that they are able to generalize to compositional proofs. However, they have difficulty generalizing to longer proofs, and they require explicit demonstrations to produce hypothetical subproofs, specifically in proof by cases and proof by contradiction.

Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees. This monograph provides a survey of the current state of the art on applications of formal methods in the autonomous systems domain. We consider correct-by-construction synthesis under various formulations, including closed systems, reactive, and probabilistic settings. Beyond synthesizing systems in known environments, we address the concept of uncertainty and bound the behavior of systems that employ learning using formal methods. Further, we examine the synthesis of systems with monitoring, a mitigation technique for ensuring that once a system deviates from expected behavior, it knows a way of returning to normalcy. We also show how to overcome some limitations of formal methods themselves with learning. We conclude with future directions for formal methods in reinforcement learning, uncertainty, privacy, explainability of formal methods, and regulation and certification.

As transformers have gained prominence in natural language processing, some researchers have investigated theoretically what problems they can and cannot solve, by treating problems as formal languages. Exploring questions such as this will help to compare transformers with other models, and transformer variants with one another, for various tasks. Work in this subarea has made considerable progress in recent years. Here, we undertake a comprehensive survey of this work, documenting the diverse assumptions that underlie different results and providing a unified framework for harmonizing seemingly contradictory findings.

Core knowledge about physical objects -- e.g., their permanency, spatial transformations, and interactions -- is one of the most fundamental building blocks of biological intelligence across humans and non-human animals. While AI techniques in certain domains (e.g. vision, NLP) have advanced dramatically in recent years, no current AI systems can yet match human abilities in flexibly applying core knowledge to solve novel tasks. We propose a new AI approach to core knowledge that combines 1) visual representations of core knowledge inspired by human mental imagery abilities, especially as observed in studies of neurodivergent individuals; with 2) tree-search-based program synthesis for flexibly combining core knowledge to form new reasoning strategies on the fly. We demonstrate our system's performance on the very difficult Abstraction \& Reasoning Corpus (ARC) challenge, and we share experimental results from publicly available ARC items as well as from our 4th-place finish on the private test set during the 2022 global ARCathon challenge.

Modern Logics, as formulated notably by Frege, Russell and Tarski involved basic assumptions about Natural Languages in general and Indo-European Languages in particular, which are contested by Linguists. Based upon those assumptions, formal Languages were designed to overcome what Logicians claimed to be 'defects' of Natural Language. In this paper we show that those assumptions contradict basic principles of Arabic. More specifically: The Logicians ideas, that within Natural Language words refer to objects, 'ToBe'-constructions represent identity statements, Indefinite Descriptions must be replaced by existential quantifiers to form meaningful Sentences and Symbols can have no interpretation-independent meanings, are all falsified using undisputed principles of Arabic. The here presented falsification serves two purposes. First, it is used as a factual basis for the rejection of approaches adopting Semantic axioms of Mathematical Logics as Models for meaning of Arabic Syntax. Second, it shows a way to approach the important computational problem: Satisfiability (SAT). The described way is based upon the realization that parsing Arabic utilizes the existence of 'meaning-particles' within Syntax to efficiently recognize words, phrases and Sentences. Similar meaning-particles are shown to exist in 3CNF formulas, which, when properly handled within the machinery of 3SAT-Solvers, enable structural conditions to be imposed on formulas, sufficient alone to guarantee the efficient production of non-exponentially sized Free Binary Decision Diagrams (FBDDs). We show, why known exponential Lower Bounds on sizes of FBDDs do not contradict our results and reveal practical evidence, obtained for multiplication circuits, supporting our claims.

It is essential for users to understand what their AI systems can and can't do in order to use them safely. However, the problem of enabling users to assess AI systems with sequential decision-making (SDM) capabilities is relatively understudied. This paper presents a new approach for modeling the capabilities of black-box AI systems that can plan and act, along with the possible effects and requirements for executing those capabilities in stochastic settings. We present an active-learning approach that can effectively interact with a black-box SDM system and learn an interpretable probabilistic model describing its capabilities. Theoretical analysis of the approach identifies the conditions under which the learning process is guaranteed to converge to the correct model of the agent; empirical evaluations on different agents and simulated scenarios show that this approach is few-shot generalizable and can effectively describe the capabilities of arbitrary black-box SDM agents in a sample-efficient manner.