miniCodeProps: a Minimal Benchmark for Proving Code Properties

Understand

AI agents have shown initial promise in automating mathematical theorem proving in proof assistants such as Lean.

• The same proof assistants can be used to verify the correctness of code by pairing code with specifications and proofs that the specifications hold.
• Automating the writing of code, specifications, and proofs could lower the cost of verification, or, ambitiously, enable an AI agent to output safe, provably correct code.
• However, it remains unclear whether current neural theorem provers can automatically verify even relatively simple programs.