Formalism
Below you will find some articles related to our theoretical program, which is based on the "programs as proofs" equivalence. We would like to translate upcoming AI legislation into specifications within the "right" system of logic (or equivalently, the "right" programming language) and then eventually write AI programs as formal proofs of those specifications. Mathematicians are already beginning to use AI (specifically, neural networks) to help proving theorems in standard mathematics. We find ourselves in this surprising "virtuous" cycle: we use neural networks (the ultimate pattern recognizers, which we do not fully understand) to develop theorem provers for things we do understand (our mathematics), which we can then use to prove theorems about AI systems based on neural networks!
The Legislative Recipe: Syntax For Machine-Readable Legislation
By Megan Ma and Bryan Wilson/ December, 2021"Legal interpretation is a linguistic venture. In judicial opinions, for example, courts are often asked to interpret the text of statutes and legislation. As time has shown, this is not always as easy as it sounds. Matters can hinge on vague or inconsistent language and, under the surface, human biases can impact the decision-making of judges. This raises an important question: what if there was a method of extracting the meaning of statutes consistently? That is, what if it were possible to use machines to encode legislation in a mathematically precise form that would permit clearer responses to legal questions?"
How Close Are Computers to Automating Mathematical Reasoning?
By VentureBeat/ July 14, 2021"A formidable open challenge in the field asks how much proof-making can actually be automated: Can a system generate an interesting conjecture and prove it in a way that people understand? A slew of recent advances from labs around the world suggests ways that artificial intelligence tools may answer that question"
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
By Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, Guillaume Lample/ Oct 21, 2022"The formalization of existing mathematical proofs is a notoriously difficult process. Despite decades of research on automation and proof assistants, writing formal proofs remains arduous and only accessible to a few experts. While previous studies to automate formalization focused on powerful search algorithms, no attempts were made to take advantage of available informal proofs.
In this work, we introduce Draft, Sketch, and Prove (DSP), a method that maps informal proofs to formal proof sketches, and uses the sketches to guide an automated prover by directing its search to easier sub-problems. We investigate two relevant setups where informal proofs are either written by humans or generated by a language model.
Our experiments and ablation studies show that large language models are able to produce well-structured formal sketches that follow the same reasoning steps as the informal proofs. Guiding an automated prover with these sketches enhances its performance from 20.9% to 39.3% on a collection of mathematical competition problems."
Are Formal Methods Applicable To Machine Learning And Artificial Intelligence?
By Moez Krichen, Alaeddine Mihoub, Mohammed Y. Alzahrani, Wilfried Yves, Hamilton Adoni, Tarik Nahhal/ May 10, 2022"Formal approaches can provide strict correctness guarantees for the development of both hardware and software systems. In this work, we examine state-of-the-art formal methods for the verification and validation of machine learning systems in particular. We first provide a brief summary of existing formal approaches in general.
After that, we report on formal methods developed for validating data preparation and training phases. Then, we go over the formal methods used for the verification of machine learning systems. At this level, we consider both partial and exhaustive techniques.
In addition, we review research works dedicated to the verification of support vector machines and decision tree ensembles. Finally, we propose several potential future directions for formal verification of machine learning systems."
AI Meets Formal Software Development
By Dieter Hutter, O. Sokolsky, Marc Shapiro/ 2013"This report documents the program and the outcomes of Dagstuhl Seminar 12271``AI meets Formal Software Development. This seminar brought together researchers from formal methods and AI.
The participants addressed the issue of how AI can aid the formal software development process, including modelling and proof. There was a pleasing number of participants from industry and this made it possible to ground the discussions on industrial-scale problems."
Formal Software Development
By Adrian Zidaritz/ Mar 3, 2011This is an overview of the Formal Software Development Program. It is written for software professionals and as such, it assumes some familiarity with symbolic manipulation.
In this overview we explain what a mathematical formal system is, show why formal systems are the foundation of software, give some concrete examples of formal software development and present the structure and the goals of the program.