FVSpec: Real-World Property-Based Tests as Lean Challenges

• URL: http://arxiv.org/abs/2606.01008v1
• Date: Sun, 31 May 2026 04:51:27 GMT
• Title: FVSpec: Real-World Property-Based Tests as Lean Challenges
• Abstract summary: We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks.<n>We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate 2,772 of them into 9,415 Lean 4 specifications.
• Score: 3.2338802435415794
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate 2,772 of them (25%) into 9,415 Lean 4 specifications with sorry placeholders (about 3 formalizations/PBT; we retain multiple attempts when none dominates on quality metrics). Translating PBTs into Lean specifications is challenging: it requires modeling Python semantics in Lean, inferring the logical property encoded in an imperative PBT, and handling the inherent difficulties of dependently-typed programming in a seldom-used language. We describe a three-agent LLM pipeline for transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model based approaches. All code (scraper and agents) and data (PBTs and Lean specifications) are open source. Our benchmark aims to drive progress on the underexplored problem of AI-assisted formal verification of real-world software, which is of increasing interest as AI produces more and more of the world's code.

Related papers

• Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning [7.228124845671868]
  Neuro-formal verification (NFV) harnesses that automation for developers of mainstream programming languages.<n>An AI coding agent translates, an established verifier decides, and a question posed in a mainstream language is answered push-button, at empirical accuracy rather than soundness, with a machine-checked proof.<n>Results on a dataset of correct and incorrect Python problems are encouraging compared to an llm-as-judge baseline.
  arXiv  Detail & Related papers  (2026-08-21T18:00:02Z)
• Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing [6.28395649374318]
  This paper investigates recurring property patterns in Apache Spark computation.<n>We design an agentic, dual-track validation framework that uses property templates to formally verify correctness in the Lean 4 theorem prover.<n>Our evaluation shows that property templates increase agentic proof engineering success by up to 2.6x (1.6x on average) and reduce proof hallucinations by 59%.
  arXiv  Detail & Related papers  (2026-07-10T03:33:47Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents [7.228124845671868]
  Agentic AI systems can now generate code with remarkable fluency.<n>But a fundamental question remains: emphdoes the generated code actually do what the user intended?
  arXiv  Detail & Related papers  (2026-03-17T21:28:59Z)
• Toward Training Superintelligent Software Agents through Self-Play SWE-RL [66.11447353341926]
  Self-play SWE-RL is a first step toward training paradigms for superintelligent software agents.<n>Our approach takes minimal data assumptions, only requiring access to sandboxed repositories with source code and installed dependencies.<n>Our results, albeit early, suggest a path where agents autonomously gather extensive learning experiences from real-world software repositories.
  arXiv  Detail & Related papers  (2025-12-21T00:49:40Z)
• Propose, Solve, Verify: Self-Play Through Formal Verification [75.44204610186587]
  We study self-play in the verified code generation setting, where formal verification provides reliable correctness signals.<n>We introduce Propose, Solve, Verify (PSV) a simple self-play framework where formal verification signals are used to create a proposer capable of generating challenging synthetic problems and a solver trained via expert iteration.<n>We show that performance scales with the number of generated questions and training iterations, and through ablations identify formal verification and difficulty-aware proposal as essential ingredients for successful self-play.
  arXiv  Detail & Related papers  (2025-12-20T00:56:35Z)
• FeatBench: Evaluating Coding Agents on Feature Implementation for Vibe Coding [11.846768103642583]
  FeatBench is a novel benchmark for vibe coding that focuses on feature implementation.<n> FeatBench is built on a multi-level filtering pipeline to ensure quality and a fully automated pipeline to evolve the benchmark.<n>Our evaluation reveals that feature implementation within the vibe coding paradigm is a significant challenge, with the highest success rate of only 29.94%.
  arXiv  Detail & Related papers  (2025-09-26T11:47:50Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• Automated Repair of Ambiguous Problem Descriptions for LLM-Based Code Generation [9.943472604121425]
  ambiguity of natural language (NL) can harm software quality.<n>We introduce an automated repair of ambiguous NL descriptions.<n>We implement this approach in a tool called SpecFix.
  arXiv  Detail & Related papers  (2025-05-12T06:47:53Z)
• Towards Automated Formal Verification of Backend Systems with LLMs [9.66648456498893]
  We propose a novel framework that leverages functional programming and type systems to translate backend code into formal Lean representations.<n>Our pipeline automatically generates theorems that specify the intended behavior of APIs and database operations, and uses LLM-based provers to verify them.<n>We evaluate our method on realistic backend systems and find that it can formally verify over 50% of the test requirements, which suggests that half of a testing engineer's workload can be automated.
  arXiv  Detail & Related papers  (2025-04-13T16:49:37Z)
• SOPBench: Evaluating Language Agents at Following Standard Operating Procedures and Constraints [59.645885492637845]
  SOPBench is an evaluation pipeline that transforms each service-specific SOP code program into a directed graph of executable functions.<n>Our approach transforms each service-specific SOP code program into a directed graph of executable functions and requires agents to call these functions based on natural language SOP descriptions.<n>We evaluate 18 leading models, and results show the task is challenging even for top-tier models.
  arXiv  Detail & Related papers  (2025-03-11T17:53:02Z)
• Can Large Language Models Write Good Property-Based Tests? [5.671039991090038]
  Property-based testing (PBT) is still relatively underused in real-world software. We investigate using modern language models to automatically synthesize PBTs using two prompting techniques. We find that with the best model and prompting approach, a valid and sound PBT can be synthesised in 2.4 samples on average.
  arXiv  Detail & Related papers  (2023-07-10T05:09:33Z)
• LeTI: Learning to Generate from Textual Interactions [60.425769582343506]
  We explore LMs' potential to learn from textual interactions (LETI) that not only check their correctness with binary labels but also pinpoint and explain errors in their outputs through textual feedback. Our focus is the code generation task, where the model produces code based on natural language instructions. LETI iteratively fine-tunes the model, using the objective LM, on a concatenation of natural language instructions, LM-generated programs, and textual feedback.
  arXiv  Detail & Related papers  (2023-05-17T15:53:31Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.