Using LLMs and Automated Reasoning to Mathematically Prove That Programs are Correct.

What is it about?

To prove that a program is correct, i.e., it always does what it is meant to do and never does something bad or unsafe, it is necessary to reason about every possible input and subsequent execution. This is particularly challenging for programs that repeat some actions based on some input - for example, taking a number and counting its prime factors by looking at each smaller number. In this case, it is not possible to know all possible executions as it is unbounded. The trick we use here is to find a mathematical formula, called an invariant, that expresses this unbounded work and use that to represent the work in the analysis. The problem with using invariants is that they are hard to find. Automated approaches often struggle to capture the required creativity. This is where this paper comes in. We use an LLM to suggest likely invariants, but we don't completely trust the LLM. They can make mistakes (we just said that finding them is hard). Hence, we use automated reasoning tools, which can reason about the truth of mathematical equations, to check whether the proposed invariants are safe replacements for the unbounded work. We found that this generally works well, although the LLM requires help expressing the invariants in the right format and sometimes doesn't guess the right ones immediately.

Featured Image

Photo by Krishna Pandey on Unsplash

Photo by Krishna Pandey on Unsplash

Why is it important?

Bugs cost the economy, so we want to mathematically prove that programs are correct to eliminate the possibility of bugs. Verification engineers are expensive. If we can replace any creative steps that an expensive human needs to do with an LLM, then we can scale verification at less cost.

Perspectives