Vision Paper: Proof-Carrying Code Completions
Parnian Shabani Kamran, Prémkumar Dévanbu, Caleb Stanford · 2024
Code completions produced by today's large language models (LLMs) offer no formal guarantees. We propose proof-carrying code completions (PC3). In this paradigm, a high-resourced entity (the LLM provided by the server) must provide a code completion together with a proof of a chosen safety property which can be independently checked by a low-resourced entity (the user). In order to provide safety proofs without requiring the user to write specifications in formal logic, we statically generate preconditions for all dangerous function calls (i.e., functions that may violate the safety property) which must be proved by the LLM.