High-Confidence Transformer-Based Compilation of Partially Ambiguous Programs
PI: David Broman, KTH Royal Institute of TechnologyThis 5-year project is financially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP).
The purpose of the project is threefold: (i) to study a novel future direction of how software can be developed using transformers and large language models, (ii) to create a formal foundation for such a direction, and (iii) to construct and evaluate a sound and secure compiler prototype.
Motivation and Problem
Large language models have in the past years shown to perform exceptionally well in generating content such as text, images, and animations. For instance, large language models, such GPT-4, Llama 3, PaLM 2, Google Gemini, and Claude 2 are designed to perform various tasks, some including multimodal inference that mixes different type of data. Moreover, recent software engineering tools based on large models, such as GitHub Copilot, Amazon CodeWhisperer, Tabnine, and Codeium, can enable developers to increase their productivity by using services such as AI-assisted code completion, code chat features, automatically explaining code, or generating comments. These cloud-based solutions, primarily commercial products, may be seen as AI assisted pair programmers, with the aim of helping the developer to write code.Although helpful for many common programming tasks, AI-assisted pair programming may result in several long-term problems. Specifically, code completion tools are often used to generate new boilerplate code trained on massive amounts of training data, often found in open-source projects with varying code quality. As a consequence, there are three major problems: (i) automatically generating boilerplate code or regenerating existing low-level code may lead to larger and larger automatically generated code bases that should have been encapsulated into libraries and other programming abstractions, (ii) the generated code from AI assistants have shown to generate insecure code with security vulnerabilities since they are trained on existing non-verified source code projects, (iii) because such tools generate code from text prompts, this approach to software engineering is not raising the abstraction: it is an efficient tool for generating code iteratively but does not result in higher-level abstractions within system design and implementation.
Research goals
This project aims to study a dramatically different approach to software development using language models and transformers, aiming to address the problems of current trends in AI-assisted code completion. The overall goal of this project is to:
develop a new theoretical foundation for secure, correct, and efficient compilation of a programming model with multi-level abstractions, including ambiguous abstractions (natural language prompts and informal diagrams) and unambiguous abstractions (declarative mathematical formalisms and well-typed program code)
More specifically, the key research challenges are to:
- design a formal semantics of multi-level-abstraction programs, where an interactive refinement component is capable of refining abstractions semantically correct.
- construct an efficient transformer-based compiler prototype that generates executable programs that are both correct (fulfilling automated oracle requirements) and secure (mitigates the generation of vulnerable code).
Vision and Significance
This project aims to study a new way of programming complex software systems using transformers and language models, where such models are not merely used for code completion. The novelty of the approach is to incorporate multi-level-abstractions within the same programming model, using partially ambiguous programs with the vision to lay the foundation for a novel way of future software development, rethinking how we develop programs and software today.
This is a personal web page. More information.