Specifications and Explanations in Automatic Programming - SpecRover
Abstract
Automatic Programming has had a significantly long heritage in Computer Science – starting with model driven development, program synthesis and program repair. A key difficulty in achieving automatic programming, is the lack of formal specifications in practice, for guiding automated code generation. Recently Large Language Model (LLM) prompt driven code generation has attracted attention – where the prompt acts as the only (natural language) specification to guide code generation. This naturally leaves the question of how to capture more rigorous specifications and explanations in automatic programming via LLMs.
In this thesis, we study and develop a host of techniques towards this shared goal and vision. In a pre-LLM setup, we study the problem setup of test-based program repair where the tests provide an incomplete specification of correctness. The lack of specifications is alleviated by automated test generation in the approach – however this requires us to manually design test oracles (expected behavior or intent) – leading to manual burden. In a post-LLM but pre-agentic AI study, we then observe that problem of oracle construction can be partially achieved by LLMs provided it is provided with discrepancies across semantically equivalent clusters of automatically generated programs. Finally, in a fully agentic AI setup for automatic programming – we construct oracle specifications by inferring the local intent of selected code methods, with the natural language issue serving as the global intent of the program. We further observe that LLM agents producing code can be accompanied by symbolic explanations in the form of property-based tests. This means that the explanations are executable, checkable and have a formal intuition beneath them – thereby bringing greater rigor to the fast-emerging field of agentic programming.
Bio
Haifeng Ruan is a PhD candidate in Computer Science at the National University of Singapore, advised by Prof. Abhik Roychoudhury. His research focuses on trustworthy automated programming, in particular program repair and coding agents. He is a core developer of AutoCodeRover, an early open-source coding agent, which was acquired as an NUS spin-off. He was also one of two lead designers of the Sonar Foundation Agent, which reached the top of the SWE-bench leaderboard. His work has been published at top software engineering venues including ICSE, ISSTA, and TOSEM.