MFAI: Logic and the Theory of Neural Language Models

About This Grant

Large language models (LLMs) are advancing the state of the art in nearly all areas of artificial intelligence, yet they remain poorly understood. At a time when new abilities as well as new limitations of LLMs are continually coming to light, a clear understanding of what they can and cannot do (that is, their expressivity) is becoming increasingly important. Furthermore, differentiating between the tasks that LLMs can solve at all scales, and those that LLMs can solve at small scales but are guaranteed to fail on at larger scales can be central to the success of some applications of LLMs, particularly where safety guarantees are needed. These questions can be answered with certainty only by mathematical verification. This project is contributing to the study of connections between LLM expressivity and mathematical logic. It is using those connections to reap both theoretical and practical benefits, in the form of new guarantees for LLMs, new extensions of LLMs, new methods for explaining how LLMs work, as well as new developments in mathematical logic. Just as the Curry-Howard isomorphism established a deep connection between logic and programming languages that enabled many results to be exchanged between the two fields, we are developing a "Curry-Howard isomorphism for neural networks": not merely a connection between one kind of neural network and one logic, but a correspondence between the elements of neural networks and the elements of logic that leads to a rich exchange of ideas between the two fields. This connection is establishing new theoretical results about neural networks and driving the development of new neural networks. In the other direction, the proposed research program is pursuing new and exciting developments in logic and model theory, particularly at the intersection of finite model theory and continuous logic, which has not been previously studied. The project is creating interdisciplinary collaborations, not only within the project itself but also between researchers in logic and deep learning more broadly. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.