⚠️ Travel Advisory:
Due to the strong number of contributions received, AIPV is now planned as a two-day event, taking place from May 18 to May 19. Please take this into account when making your travel and accommodation arrangements.

⚠️ Regarding Participation:
AIPV is planned as an in-person workshop. Remote presentations are not a standard option and will only be considered in exceptional cases upon prior agreement with the organisers. Thank you for your understanding.

AI, Proof and Verification 2026 (AIPV2026)

Collocated with FM 2026 May 18–19, 2026 Tokyo, Japan

Table of Contents

  1. About AIPV
  2. Organization
  3. Local Organising Team
  4. Administrative Support
  5. Sponsor (Partner)
  6. Dates
  7. Venue
  8. 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:

AIPV 2026 Poster

Organising Team

Yutaka Link to the page of Yutaka. Jonathan Link to the page of Jonathan. Andreea Link to the page of Andreea. Stefan R Link to the page of Stefan.

Local Organising Team

Minchao Link to the page for machine learning. Yutaka Link to the page for machine learning.

Review Team

Andreea Link to the page of Andreea. Jonathan Link to the page of Jonathan. Yutaka Link to the page of Yutaka. Stefan R Link to the page of Stefan. Stefan N Link to the page of Stefan.

Administrative Support

The administrative and financial operations of AIPV 2026 are supported by ASTER (Association for Software Test Engineering and Research), which kindly assists with sponsorship processing and financial management for the workshop.

Harmonic Postcard

Important Dates

The following is the tentative timeline of AIPV

Venue

AIPV2026 will take place at Hitotsubashi Hall in Tokyo, Japan.

Submission

The submission deadline has passed, but inquiries about possible contributions are welcome. Please contact the organiser at nagashima+cs.cas.cz (replace + with @).

Contact

The main point of contact is Yutaka’s email address: nagashima+cs.cas.cz (replace + with @).

Random Image