miniCodeProps: a Minimal Benchmark for Proving Code Properties
miniCodeProps benchmarks neural theorem provers' ability to automatically verify simple to complex program properties in Lean 4, revealing current limitations.
Key Findings
Methodology
This work constructs miniCodeProps, a benchmark with 201 specifications of self-contained programs involving lists, natural numbers, and binary trees. The programs are derived from TIP's Haskell code, translated into Lean 4 with added termination and sorting properties. The benchmark spans easy to hard levels, designed to test core capabilities like recursion, induction, and sorting correctness. The models evaluated include GPT-4 and ntp-ctx-1.3B, employing full proof generation and tactic-based strategies. The methodology emphasizes recursive reasoning, inductive proof, and multi-step refinement, aiming to assess the models’ understanding of fundamental program properties.
Key Results
- GPT-4 achieved 75.6% success on easy properties, but only 4.34% on medium and hard ones, with overall success at 34.8%. Incorporating proof refinement improved medium success to 6.96% and overall to 37.3%. ntp-ctx-1.3B outperformed GPT-4 on medium difficulty, reaching 72.1%. Results highlight the gap in current neural models’ ability to handle complex inductive proofs, especially for recursive and sorting properties. Multi-round refinement strategies significantly boost proof success, demonstrating the importance of algorithmic improvements.
- The benchmark effectively tests core reasoning skills such as recursive termination, sorting correctness, and inductive proofs. The results reveal that while models can handle simple properties, their performance drops sharply on more complex tasks. The experiments show that specialized training and multi-step strategies are promising directions. The success of ntp-ctx-1.3B suggests that domain-specific training can enhance proof automation, though high computational costs remain a challenge.
- These findings are significant for both academia and industry, as they identify key weaknesses in current neural theorem proving approaches. miniCodeProps provides a standardized platform to benchmark progress, guiding future research toward models that can reliably verify code properties. The work emphasizes the importance of combining learning-based methods with strategic proof refinement, paving the way for practical AI-assisted software verification and safety assurance.
Significance
This work introduces a minimal yet challenging benchmark for automated program property verification, exposing the limitations of current neural theorem provers. By focusing on fundamental capabilities like recursion, induction, and sorting, miniCodeProps offers a clear target for future model improvements. Its public release enables consistent evaluation across research efforts, accelerating progress in AI-driven formal verification. The benchmark bridges the gap between mathematical theorem proving and real-world program verification, fostering the development of more robust, scalable, and interpretable proof systems. Ultimately, this advances the goal of integrating AI into software safety and correctness assurance, with broad implications for industry and society.
Technical Contribution
The paper presents miniCodeProps, a systematically designed benchmark comprising 201 specifications derived from TIP programs, translated into Lean 4 with added termination and sorting lemmas. It integrates multiple proof strategies, including full proof generation and tactic-based search, evaluated with GPT-4 and ntp-ctx-1.3B models. The approach emphasizes core reasoning skills such as recursive termination, inductive proofs, and sorting correctness. The introduction of multi-round proof refinement demonstrates a novel method to improve proof success rates. The benchmark’s design facilitates targeted evaluation of foundational capabilities necessary for automated program verification, setting a new standard for neural theorem proving in software contexts.
Novelty
This is the first systematic benchmark focusing on verifying simple, self-contained program properties in Lean 4, derived from TIP's inductive programs. Unlike existing benchmarks centered on mathematical theorems or large verification projects, miniCodeProps emphasizes core program verification skills in a controlled, minimal setting. The integration of multi-step proof refinement with state-of-the-art language models represents a novel approach, demonstrating significant performance gains over baseline methods. Its design enables precise diagnosis of model weaknesses and guides targeted improvements, marking a new direction in neural-assisted program verification research.
Limitations
- Current models, including GPT-4, perform poorly on medium and hard properties, indicating limitations in handling complex inductive and recursive proofs. The benchmark’s simplicity, while beneficial for controlled evaluation, may not fully capture industrial-scale verification challenges. High computational costs for training and inference restrict scalability, and the models’ reasoning capabilities remain limited in deep recursive and sorting proofs. Future work must address these gaps by developing more specialized architectures, training data, and hybrid symbolic-neural methods to improve robustness and scalability.
Future Work
Future directions include enhancing models’ understanding of recursive and inductive reasoning, integrating symbolic reasoning modules, and developing multi-step proof strategies. Expanding the benchmark to include more complex programs and properties will better reflect industrial needs. Additionally, exploring transfer learning from mathematical theorem proving to program verification, and reducing computational costs through model compression and efficient inference, are promising avenues. The authors also plan to investigate explainability and interpretability of proofs, aiming to build trustworthy AI proof assistants capable of handling real-world software verification tasks.
AI Executive Summary
Deep Dive
Plain Language Accessible to non-experts
想象你在学校的科学实验室里，老师给你一份简单的实验步骤，比如用水和盐做盐水。你只要按照步骤操作，成功的概率很高。但如果老师给你一份复杂的化学配方，比如调配一种新药，就需要很多复杂的步骤和细心的计算。程序验证就像做实验，确保每个步骤都正确，才能得到可靠的结果。现在，科学家们用AI像是帮你做实验的助手，但它还只能处理简单的实验。miniCodeProps就像是给AI的基础实验步骤，让它练习，看看能不能学会做更复杂的实验。未来，AI可能会帮人做出各种复杂的科学实验，保证每一步都正确无误，就像一个超级实验员一样。
ELI14 Explained like you're 14
想象你在学校的科学课上，老师让你做一些简单的实验，比如用水和盐做盐水。只要按照步骤来，成功几率很高。但如果老师让你调配一种复杂的新药，就得经过很多复杂的步骤，还要非常小心。程序验证就像做这些实验，确保每一步都正确，才能保证结果可靠。科学家们用AI帮忙做验证，但现在它还只能做简单的实验。miniCodeProps就像是给AI的基础实验步骤，让它练习，看看能不能学会做更复杂的实验。未来，AI可能会帮人做出各种复杂的科学实验，保证每一步都正确无误，就像一个超级实验员一样。
Abstract
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. We present miniCodeProps, a benchmark of 201 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 sufficient to break current LLM-based provers, with state-of-the-art methods showing promise on the easy properties in miniCodeProps, yet failing to prove nearly all of the medium and hard properties. We publicly release miniCodeProps as a benchmark for furthering automated theorem proving in the context of formally verified code.