Large Language Models
For Lattice-Theoretic Reasoning of Reactive Programs
The Project
The project aims to advance AI for mathematical reasoning by developing a novel approach to proving refinement laws using a Large Language Model (LLM) fine-tuned on a synthesised dataset of refinement propositions. By focusing on creating a comprehensive dataset that includes proofs and counter-examples, the team seeks to enhance the diversity and quality of training datasets, addressing a significant gap in AI for Math. The project will integrate the LLM with state-of-the-art refinement checking techniques to improve the accuracy and efficiency of refinement proofs. This work not only promises to outperform existing methods but also provides a valuable benchmark dataset for future AI model training in mathematical reasoning.
The Team
Pedro Ribeiro is a Lecturer (Assistant Professor) in Computer Science at the University of York, UK. Previously, he was a Research Fellow in the School of Physics Engineering and Technology at York, and before that a Research Associate in Computer Science. He completed his PhD at York on the treatment of angelic non-determinism for process calculi via complete lattice theories in the Unifying Theories of Programming. He has over a decade of experience with formal approaches to software engineering relevant to robotics and cyber-physical systems more generally. His research interests span the breadth of the engineering lifecycle, spanning from design and development of domain-specific notations and their semantics, to testing and formal reasoning using automated mathematical proof techniques, such as model-checking and theorem proving. He is a member of the York's RoboStar centre for Excellence in Software Engineering for Robotics, and a founding member of Formal Methods Europe's communications committee.
Frank Soboczenski is an Assistant Professor in Computer Science (AI/ML) at the University of York and holds an affiliate scientist position at King’s College London. His research centers on deep learning and Transformer models, explainable machine learning and quantum machine learning, focusing primarily on applications in space and healthcare. Frank is a STEM scientist for NASA’s & NOAA’s GLOBE program, a NASA GeneLab AI-focused working group member on human spaceflight data, an IBM Quantum Researchers Program Scientist, a member of NASA’s Nancy Grace Roman Spacecraft Working Group, part of the Laser Interferometer Space Antenna (LISA) working group, a European Laboratory for Learning and Intelligent Systems (ELLIS) Scholar, part of the international astronomical union (IAU). Frank frequently collaborates with NASA centers, including leading past machine learning workshops at Kennedy Space Center and serving as a speaker at NASA’s Biomedical Symposiums. His work has garnered multiple accolades, such as the NASA TechLeap Prize; NASA/NOAA/U.S. Department of State recognition for outstanding mentorship; and several Frontier Development Lab honors.