Liyi Li, Myra Cohen, and Ali Jannesari have been awarded a $1,000,000 collaborative grant with the University of Illinois at Chicago from the National Science Foundation’s Formal Methods in the Field program for their research on just-in-time verification for high-performance compilers. Liyi Li, Assistant Professor, is the grant's Principal Investigator.
The goal of the project is to formalize and enhance the reliability and performance of parallelizing compilers by automatically verifying that translated code retains the functionality of the original sequential program. This will involve testing on a real-world large language model (LLM)-based parallelizing compiler to ensure the tool's ability to guarantee correct translations. It will also provide feedback that helps improve code accuracy and efficiency.
The Need for Reliable Parallel Computing
The latest advancements in modern scientific research rely on compilers to transform sequential programs, designed to execute one operation at a time, into parallel ones capable of handling hundreds or even thousands of simultaneous operations. These parallel programs are essential for optimizing computational performance, particularly in data-intensive fields like genomics, climate modeling, and artificial intelligence. Overall, the reliance on accurate and efficient parallel computing is growing as researchers gain access to more powerful computers and larger datasets.
However, the complexity of parallel programs introduces significant challenges for assuring correctness. These programs are notoriously difficult to understand, and we lack formal approaches to reason about sequential to parallel transformations. This can lead to unpredictable interactions and bugs that undermine the accuracy of the programs; even minor computational errors can lead to misleading models and false conclusions, slowing scientific progress and wasting resources.
Integrating Large Language Models in Compiler Technology
One of the approaches for transforming sequential programs to parallel ones is to use Large Language Models (or LLMs). LLM transformation provide automation of a difficult manual task, however, it increases the challenges for verification since step by step reasoning and traceability is lacking. Research on this project will address these challenges by developing verification mechanisms that check the accuracy of LLM-generated code and offer insights to improve its quality of transformation. This is expected to accelerate scientific progress as researchers will be able to conduct experiments with greater confidence in their computational results, which will lead to more accurate models, faster discoveries, and a reduced likelihood of errors occurring through the research process.