Retrieval-Augmented TLAPS Proof Generation with Large Language Models

TL;DR

This paper introduces a retrieval-augmented approach using large language models to automate proof generation in TLA+ proofs, effectively handling intermediate complexity proof obligations but facing challenges with more complex theorems.

Contribution

It presents a novel combination of sub-proof obligation generation and retrieval-augmented proof synthesis, advancing LLM applications in formal verification.

Findings

Successfully generates valid proofs for intermediate complexity obligations

Faces limitations with complex theorems

Demonstrates potential for LLM-assisted proof development

Abstract

We present a novel approach to automated proof generation for the TLA+ Proof System (TLAPS) using Large Language Models (LLMs). Our method combines two key components: a sub-proof obligation generation phase that breaks down complex proof obligations into simpler sub-obligations, and a proof generation phase that leverages Retrieval-Augmented Generation with verified proof examples. We evaluate our approach using proof obligations from varying complexity levels of proof obligations, spanning from fundamental arithmetic properties to the properties of algorithms. Our experiments demonstrate that while the method successfully generates valid proofs for intermediate-complexity obligations, it faces limitations with more complex theorems. These results indicate that our approach can effectively assist in proof development for certain classes of properties, contributing to the broader goal of integrating LLMs into formal verification workflows.