Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems

• URL: http://arxiv.org/abs/2605.23109v1
• Date: Fri, 22 May 2026 00:05:36 GMT
• Title: Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
• Abstract summary: We present Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof.<n>IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents.<n>IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.
• Score: 100.24694338574402
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI agents increasingly excel at generating, testing, and refining code. However, they fall short on tasks requiring formal guarantees of full coverage that testing alone cannot provide. Distributed systems are a prime example: properties such as consistency between reads and writes must hold under every possible interleaving of events. Mechanized formal verification can guarantee such correctness, but typically demands months to years of expert effort. As evidence, even SOTA coding agents (Codex with GPT-5.4 and Claude Code with Opus 4.6) succeed on only 2/7 distributed key-value-store specifications. In this paper, we present the first effective approach to addressing this gap, Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof, and learns from failed attempts to systematically try promising strategies. Built as an agentic LLM system, IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents. IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.

Related papers

• Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
  Large language models (LLMs) promise to generate proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system.<n>We show that imposing such a strategy is unnecessary and limiting.<n>Handing the whole lemma to a general code agent, free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective.
  arXiv  Detail & Related papers  (2026-07-07T14:39:59Z)
• Plan First, Judge Later, Run Better: A DMAIC-Inspired Agentic System for Industrial Anomaly Detection [51.90293101535452]
  We propose DMAIC-IAD (DMAIC-inspired Agentic Industrial Anomaly Detection), a "Plan First, Judge Later" multi-agent system.<n>We show DMAIC-IAD improves average detection performance over applicable agentic baselines by 37.76%.
  arXiv  Detail & Related papers  (2026-06-03T08:38:14Z)
• From I/O to Code with Discovery Agent [103.88427301265669]
  We propose DIO-Agent, a discovery agent for IO2Code.<n>Our method frames IO2Code as an evolutionary search over discrete program space.<n>Extensive experiments show that DIO-Agent consistently outperforms both traditional program-by-example method and SOTA evolution-agent baselines.
  arXiv  Detail & Related papers  (2026-05-14T18:57:32Z)
• The Productivity-Reliability Paradox: Specification-Driven Governance for AI-Augmented Software Development [0.0]
  Controlled studies report 20-56% productivity gains on well-scoped tasks, while the most rigorous RCT documents a 19% slowdown for experienced developers.<n> telemetry across 10,000+ developers shows 98% more pull requests but 91% longer review times with flat delivery metrics.<n>This paper argues these findings constitute the Productivity-Reliability Paradox (PRP): a systematic phenomenon emerging from non-deterministic code generators and insufficient specification discipline.
  arXiv  Detail & Related papers  (2026-05-01T23:37:50Z)
• Towards Multi-Agent Autonomous Reasoning in Hydrodynamics [0.06999740786886537]
  We present a multi-agent system (MAS) prototype for hydrodynamics in which specialized agents are coordinated through a Layer Execution Graph (LEG)<n>A planner agent constructs query-specific execution topologies from natural-language routings that capture domain knowledge without hard-coding it as rigid control logic.<n>A reporter agent synthesizes the final response, while the runtime logs provenance for every tool invocation to support auditability.
  arXiv  Detail & Related papers  (2026-05-01T21:17:55Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoder is an agentic code verification framework.<n>It enables prove-as-you-generate development where code, invariants, and proofs co-evolve.
  arXiv  Detail & Related papers  (2026-03-31T00:06:44Z)
• Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification [34.98335927187393]
  Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness.<n>We propose a hierarchical proof search framework for automated code verification in Lean4.<n>We train Goedel-Code-Prover-8B, a single unified policy for both decomposition and completion.
  arXiv  Detail & Related papers  (2026-03-18T18:42:04Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  Inference-time compute has re-emerged as a practical way to improve LLM reasoning.<n>Most test-time scaling (TTS) algorithms rely on autoregressive decoding.<n>We propose Prism, an efficient TTS framework for dLLMs.
  arXiv  Detail & Related papers  (2026-02-02T09:14:51Z)
• CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
  Code verifiers play a critical role in post-verification for LLM-based code generation.<n>Existing supervised fine-tuning methods suffer from data scarcity, high failure rates, and poor inference efficiency.<n>We show that naive RL with only functionality rewards fails to generate effective unit tests for difficult branches and samples.
  arXiv  Detail & Related papers  (2026-01-30T10:33:29Z)
• AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution [20.91584024250844]
  AutoICE is an evolutionary search for synthesizing verifiable C code.<n>It successfully verifies $90.36$% of code, outperforming the state-of-the-art (SOTA) approach.
  arXiv  Detail & Related papers  (2025-12-08T12:35:10Z)
• AegisLLM: Scaling Agentic Systems for Self-Reflective Defense in LLM Security [74.22452069013289]
  AegisLLM is a cooperative multi-agent defense against adversarial attacks and information leakage.<n>We show that scaling agentic reasoning system at test-time substantially enhances robustness without compromising model utility.<n> Comprehensive evaluations across key threat scenarios, including unlearning and jailbreaking, demonstrate the effectiveness of AegisLLM.
  arXiv  Detail & Related papers  (2025-04-29T17:36:05Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a procedure that equips LLMs with automation methods at various granularities.<n>Our method is validated on the miniF2F benchmark using the open-source deep-math-7b-base model and the Isabelle proof assistant.<n>We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-seek-Distill-1.5B from 44.3% to 50.4%.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• CoopetitiveV: Leveraging LLM-powered Coopetitive Multi-Agent Prompting for High-quality Verilog Generation [7.2267316594130095]
  Existing approaches use LLM-assisted single-agent prompting or cooperation-only multi-agent learning.<n>We propose an LLM-based coopetitive multi-agent prompting framework, in which the agents cannot collaborate with each other to form the generation pipeline.<n>Our experimental results show that the coopetitive multi-agent framework can effectively mitigate the degeneration risk and reduce the error propagation.
  arXiv  Detail & Related papers  (2024-12-15T01:58:10Z)
• DS-Agent: Automated Data Science by Empowering Large Language Models with Case-Based Reasoning [56.887047551101574]
  We present DS-Agent, a novel framework that harnesses large language models (LLMs) agent and case-based reasoning (CBR) In the development stage, DS-Agent follows the CBR framework to structure an automatic iteration pipeline, which can flexibly capitalize on the expert knowledge from Kaggle. In the deployment stage, DS-Agent implements a low-resource deployment stage with a simplified CBR paradigm, significantly reducing the demand on foundational capabilities of LLMs.
  arXiv  Detail & Related papers  (2024-02-27T12:26:07Z)

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.