LLM-powered automated software testing

AID stands for Automated Input Diversification, a new approach combining LLMs with differential testing to create robust test cases. AID leverages the computational power of LLMs to generate diverse program variants, and then employs differential testing to compare these variants. By examining discrepancies in outputs, AID finds bugs.

Here is my math interpretation:

Every correct program (from a format verification standpoint) is plausibly correct, as it passes tests.

Every program is trivially plausibly correct if the set of unit tests is empty (indeed you can write plausibly correct programs by not writing tests!)

If the input space is not finite, since the set of tests is finite, we cannot determine if a plausibly correct program is indeed correct using tools like AID.

A program under test from a sample in the training data passes all the given unit tests — it can be treated as a lossy reconstruction of the correct program (or a set of all correct programs) with perhaps some measure of how close that program is to the correct program by inducing some metric on the test set.

In some other hand-wavy sense, the trickiest programs to debug are the one that appear “dense” in the test set — they pass an infinite subset of the input space test cases with one off problem points that are not obvious edge cases (e.g. a function that takes a single integer as an input only fails on input 10).

As software developers, we don’t formally prove that a program is correct — though we do try to execute something close to that process, informally, and perhaps even inductively, in our heads, to prove to ourselves that our algorithm is correct.

Now, imagine taking this to the next level: asks LLMs formally verify a program, ensuring it is provably correct. This could be part of the next-gen LLM-powered CI/CD pipeline!