This grant funds a project by computer scientist Jeannette Wing, Director of the Columbia University Data Science Institute and Professor of Computer Science, to adapt "formal methods” (the representation of computer science systems as mathematical objects) to AI systems.  Once the AI system, the input data, and the desired trust property are formally specified, the AI system can then be analyzed using mathematics, allowing a skilled analyst to rigorously prove or disprove statements about the system being represented. The technique holds obvious appeal for those concerned about the trustworthiness of AI systems, since a formal methods analysis has the potential to reveal how an AI system would or would not behave in novel situations.  Grant funds will support Wing’s attempts to extend formal methods theory to AI systems, including how to formally specify properties of AI systems like fairness, privacy, and robustness.  A particular focus of Wing’s work will be to better formally understand the relationships among such properties, in order to identify and generalize their commonalities and differences.  Wing will also work on trying to use formal methods to characterize, with respect to these trust properties, the relationship between AI systems and the datasets used for training and testing them.