Neural networks 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 a machine learning system to output provably correct code.
However, it remains unclear whether current neural theorem provers can
automatically verify even relatively simple programs. We present miniCodeProps,
a benchmark of 177 program specifications in the Lean proof assistant, aimed at
the subproblem of automatically generating a proof for a provided program and
specification. miniCodeProps contains specifications about simple,
self-contained programs (e.g., lists, natural numbers, binary trees) with
varied proof difficulty. Despite its simplicity, miniCodeProps is challenging
for current LLM-based provers, which succeed in proving about 25 percent of the
specifications. We publicly release miniCodeProps as a benchmark for furthering
automated theorem proving in the context of formally verified code.

利用神经网络的数学定理证明、代码验证和自动化定理证明等领域的研究，提出了一个测试用例，旨在进一步发展形式验证代码的自动定理证明。