AI, Proof and Verification 2026 (AIPV2026)

About AIPV
Organization
Dates
Contact

About AIPV

Artificial intelligence and machine learning have shown remarkable progress in recent years, particularly through large language models (LLMs) and neural approaches. Yet despite their successes in natural language processing and perception tasks, reasoning remains a major open challenge for AI. LLMs are not inherently good at rigorous reasoning: they can generate plausible but invalid arguments, lack guarantees of soundness, and often fail on tasks requiring compositional or symbolic inference. This creates both an opportunity and a challenge: theorem proving and formal verification provide precisely the kind of rigorous environment where AI methods can be stress-tested, improved, and guided towards more trustworthy reasoning.

At the same time, the gap between the AI community (AAAI, NeurIPS, ICML, IJCAI) and the logic/theorem proving/verification community (FM, CAV, FMCAD, CADE, ITP, IJCAR) remains wide. The differences are not merely technical but also cultural — from evaluation criteria, benchmarks, and publication norms, to expectations about rigor versus empirical performance. This culture gap impedes knowledge transfer and slows down progress at the intersection. A dedicated forum that lowers this barrier can accelerate mutual understanding and collaboration.

Even within the logic-based communities themselves there is diversity: different proof assistants, logics, and verification frameworks (e.g., higher-order logics, dependent type theories, SMT-based systems, model checkers) present different challenges for AI integration. Some require guiding interactive proof search, others demand scaling verification of complex hardware/software systems, and others seek reliable translation between informal and formal representations. Bringing together researchers across these different traditions is essential to identify commonalities, share successes and failures, and shape a coherent research agenda.

The AI for Proof and Verification (AIPV) addresses precisely these needs. By gathering researchers from theorem proving, formal verification, and AI/ML, it provides a forum to:

Critically assess the capabilities and limitations of current AI/LLM approaches for rigorous reasoning.
Share experiences across different logics and verification frameworks.
Bridge the culture gap between AI and logic-based communities through dialogue and collaboration.
Chart new directions for AI-assisted formal reasoning that balance scalability with soundness and trust.