核心发现
方法论
该研究构建了miniCodeProps基准，包含201个自包含程序的规格，涵盖列表、自然数、二叉树等基本数据结构。通过将TIP中的Haskell程序翻译成Lean 4，结合递归终止性和排序算法的性质，设计了多层次难度的证明任务。采用GPT-4和ntp-ctx-1.3B模型进行全自动证明，结合策略搜索和逐步证明验证，评估模型在不同难度级别的表现。该方法强调模型对递归、归纳和排序性质的理解能力。
关键结果
- 在easy属性中，GPT-4模型的成功率达75.6%，而medium和hard属性的成功率仅为4.34%，显示出当前模型在复杂证明中的不足。引入证明细化策略后，medium难度提升至6.96%，整体成功率提升至37.3%。ntp-ctx-1.3B模型在中等难度表现优于GPT-4，验证了专用训练的潜力。研究结果表明，miniCodeProps能有效挑战现有神经定理证明模型，推动自动化证明技术的发展。
- 该基准的设计充分体现了程序验证中的核心能力，包括递归终止、排序正确性等关键性质。通过多样化难度和简洁的程序结构，揭示了模型在归纳推理和复杂证明策略上的局限，为未来模型的改进提供了明确目标。实验还显示，策略搜索和多轮推理能显著改善证明成功率，强调算法优化的重要性。
- 这些发现对学术界和工业界具有重要意义，有助于推动自动化定理证明在软件安全、程序验证等领域的应用，特别是在AI辅助的安全保障体系中。miniCodeProps作为一个简洁而具挑战性的基准，为未来研究提供了标准测试平台，促进深度学习模型在形式验证中的创新。
研究意义
该研究通过构建简洁而具有挑战性的程序验证基准，揭示了当前神经网络在自动证明中的不足，推动了形式验证自动化的发展。miniCodeProps的设计强调基础能力的测试，有助于识别模型在递归、归纳和排序等关键技术上的短板，为未来模型的改进提供明确方向。其公开发布为学术界和工业界提供了统一的评估平台，有望加速自动化定理证明在软件工程中的落地应用，提升软件安全性和可靠性。研究还强调了结合策略搜索和多轮推理的重要性，为下一代证明模型的设计提供了理论基础。
技术贡献
本研究提出了miniCodeProps基准，系统性地涵盖了程序验证中的核心能力，包括递归终止、排序性质和归纳推理。通过将TIP中的Haskell程序翻译到Lean 4，结合递归终止性证明和排序算法性质，设计了多层次难度的验证任务。引入GPT-4和ntp-ctx-1.3B模型，结合全自动证明和逐步策略搜索，展示了当前模型在基础验证任务中的表现。研究还提出了多轮证明细化技术，有效提升了复杂证明的成功率，为未来模型的训练和优化提供了新思路。
新颖性
该工作首次系统性地将TIP中的程序规格转化为Lean 4验证任务，构建了涵盖不同难度的验证基准。不同于传统的复杂项目验证，miniCodeProps强调基础能力的测试，具有高度的可控性和可扩展性。引入多轮证明细化策略和专门训练的语言模型，显著提升了自动证明的效果，展示了深度学习在形式验证中的潜力。这些创新为自动化定理证明提供了新的研究方向和工具基础。
局限性
- 模型在中等和困难属性上的成功率仍然较低，说明当前方法在复杂归纳和排序证明中存在明显瓶颈。证明的复杂性和递归终止性证明的难度限制了模型的自动化能力，尤其是在需要深层次归纳推理的场景中。
- 该基准主要基于程序的简洁性和特定数据结构，可能未能充分覆盖工业界的复杂验证场景。模型在处理大规模、多模块的代码库时仍面临挑战，未来需要扩展验证任务的多样性。
- 当前实验主要依赖GPT-4和ntp-ctx-1.3B模型，缺乏对更大规模或专用训练模型的评估。高昂的计算成本和有限的训练数据限制了模型的泛化能力，未来需探索更高效的训练策略。
未来方向
未来将着重于提升模型在复杂归纳和排序证明中的表现，探索多轮推理和策略学习的结合。还计划扩展基准的规模和多样性，涵盖更多程序结构和验证性质。此外，将结合符号推理和深度学习，开发混合方法以增强证明能力。研究还将关注模型的可解释性和验证效率，为工业应用提供可行的自动化工具。
AI 总览摘要
在软件安全和程序可靠性日益重要的背景下，自动化定理证明成为关键技术之一。现有方法虽在数学证明中取得一定进展，但在程序验证领域仍面临巨大挑战。miniCodeProps基准的提出，旨在评估神经网络在自动证明程序属性方面的能力，特别是在Lean 4环境中。该基准由201个自包含程序规格组成，涵盖列表、自然数和二叉树等基础数据结构，难度从简单到复杂逐步递增。通过将TIP中的Haskell程序翻译到Lean，结合递归终止性和排序性质，设计了多层次验证任务。采用GPT-4和ntp-ctx-1.3B模型进行自动证明，结果显示模型在简单任务中表现尚可，但在中等和复杂任务中明显不足。引入证明细化策略后，性能有所提升，但仍需突破模型在归纳推理和排序证明中的瓶颈。该研究揭示了当前深度学习模型在基础程序验证中的局限性，也为未来模型的优化提供了明确方向。miniCodeProps的发布，为学术界和工业界提供了统一的评估平台，推动自动化定理证明技术的快速发展，最终有望实现AI在软件安全保障中的广泛应用。未来工作将聚焦于多轮推理、策略学习和模型扩展，旨在实现更强的自动验证能力，助力软件工程的智能化升级。
深度分析
研究背景
程序验证作为软件工程中的核心环节，经历了从手工证明到自动化工具的演变。早期依赖形式化方法如Hoare逻辑和模型检测，逐步引入交互式定理证明器（如Coq、Lean、Isabelle），极大提升了验证的可靠性。近年来，深度学习和大规模预训练模型的兴起，为自动证明带来了新的可能性。相关工作包括Lean的Mathlib自动证明、Coq的ProverBot和Diva，以及基于符号推理的SMT工具。尽管如此，复杂程序的自动证明仍面临归纳、递归终止和排序性质等难题，限制了其在工业中的应用。miniCodeProps旨在通过简洁、具有代表性的验证任务，推动基础能力的突破。
核心问题
当前神经定理证明模型在复杂归纳和排序性质验证中表现不足，尤其在中等和困难难度级别。模型缺乏对递归、归纳推理和排序算法的深刻理解，导致成功率低。验证程序属性的难点在于证明的结构复杂、证明长度长、涉及多层次逻辑推导。现有基准多偏重数学定理，难以反映实际程序验证的挑战。如何设计既简洁又能充分测试模型能力的验证任务，成为亟待解决的问题。
核心创新
本研究的创新点包括：1）构建涵盖基础数据结构和排序算法的验证基准miniCodeProps，强调程序验证的核心能力；2）将TIP中的Haskell程序高效翻译到Lean 4，结合递归终止性和排序性质，设计多难度验证任务；3）引入多轮证明细化策略，结合GPT-4和ntp-ctx-1.3B模型，提升自动证明性能。这些创新突破了传统复杂项目验证的局限，强调基础能力的测试，为未来自动化验证提供了新工具和思路。
方法详解
- �� 采集TIP中的Haskell程序，筛选出适合验证的代码片段，翻译成Lean 4。
- �� 为每个程序定义递归终止性证明和排序性质，确保验证任务的完整性。
- �� 根据难度将验证任务划分为easy、medium和hard三类，设计不同的证明目标。
- �� 利用GPT-4和ntp-ctx-1.3B模型，进行全自动证明尝试，包括：
- 全局证明：模型生成完整证明，验证通过即成功。
- 策略搜索：逐步生成证明步骤，结合验证器确认正确性。
- �� 引入多轮证明细化，模型在失败后学习改进，提升复杂证明的成功率。
实验设计
采用TIP中的程序作为验证对象，覆盖列表、自然数和二叉树等结构。模型对每个任务进行多次尝试，记录成功比例。基线模型包括GPT-4和ntp-ctx-1.3B，分别进行全自动证明和策略搜索。评估指标为成功率（pass@32），同时分析不同难度和策略对性能的影响。实验还包括对证明长度、复杂度和模型推理能力的分析，验证多轮细化策略的有效性。通过对比不同模型和策略，揭示自动证明的潜在瓶颈和改进空间。
结果分析
GPT-4在easy任务中成功率达75.6%，medium和hard任务成功率分别为4.34%，整体成功率为34.8%。引入证明细化后，medium成功率提升至6.96%，整体成功率提升至37.3%。ntp-ctx-1.3B模型在中等难度表现优于GPT-4，成功率达72.1%。实验显示，基础模型在简单任务中表现尚可，但在复杂任务中仍显不足。多轮细化策略显著改善了复杂证明的成功率，验证了算法优化的重要性。这些结果表明，miniCodeProps能有效挑战当前神经证明模型，推动未来技术发展。
应用场景
该基准可用于评估和训练自动化证明模型，特别适合软件安全、程序验证和AI辅助开发。工业界可以借助miniCodeProps开发更智能的验证工具，减少人工验证成本。学术界则可利用其作为基础能力测试平台，推动基础算法创新。未来，结合深度学习和符号推理，有望实现更高效、更可靠的自动证明系统，提升软件工程的自动化水平。
局限与展望
模型在中高难度任务中的表现仍有限，特别在复杂归纳和排序证明中存在明显瓶颈。验证任务偏向简洁程序，难以直接迁移到工业级复杂代码。高昂的计算成本限制了大规模训练和应用。未来需要改进模型的归纳推理能力、扩展验证任务的多样性，以及降低推理成本，以实现更广泛的工业应用。
通俗解读 非专业人士也能看懂
想象你在厨房里做菜，很多菜谱都写得很简单，比如炒个蛋、煮个面。这些简单的菜谱容易理解，也容易做成功，但如果要做一道复杂的法式大餐，步骤多、技巧高，难度就大了。程序验证就像做菜，程序中的每个步骤都要正确，否则菜就会失败。现在，科学家们用AI像厨师一样，试图让它自己学会做复杂菜肴，但目前AI还只能做一些简单的菜。miniCodeProps就像是给AI出的一份简单菜谱，让它练习，看看能不能学会做更复杂的菜。通过不断练习，AI可以变得越来越厉害，未来甚至能帮人做出最复杂的菜肴，确保每一道都完美无缺。
简单解释 像给14岁少年讲一样
想象你在学校的烹饪课上，老师给你一些简单的菜谱，比如煎蛋或做三明治。你只要按照步骤做，就能成功。可是如果老师要你做一道复杂的法国大餐，比如蜗牛焗饭，就难多了，因为步骤多、技巧复杂，还要确保每一步都正确。科学家们也在教AI像你一样学会做菜，但AI还只会做简单的菜。miniCodeProps就像是给AI的练习菜谱，让它试试能不能做出一些简单的菜，然后逐渐变得更厉害。未来，AI可能会帮人做各种复杂的菜，保证每一道都好吃又安全。就像你在厨房里不断练习，最后变成大厨一样。
原文摘要
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.