Google Form for Business Meeting

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. Sponsor (Contributor)
  7. Dates
  8. Venue
  9. 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.

AIPV was supported by the research programme of the Strategy AV21 AI: Artificial Intelligence for Science and Society.

Harmonic Postcard

Noeon Research Postcard

Axiom builds AI systems that reason with mathematical precision for applications in finance, cryptography, software verification and scientific research—domains where correctness isn’t optional. Founded in March 2025 by Morgan Prize winner Carina Hong, Axiom raised $64M in seed funding at a $300M valuation. The team includes researchers from Meta’s FAIR lab and mathematician Ken Ono, former VP of the American Mathematical Society. Axiom’s AI system AxiomProver achieved a perfect score on the Putnam, the world’s hardest undergraduate math exam, and has autonomously solved research math problems with zero human guidance - including the Chen-Gendron conjecture and Fel’s conjecture.

Axiomatic is building AI for science and engineering that can reason, not just generate. At the core of Axiomatic’s platform is Axiomatic AI’s Lemma, a system that combines large-scale machine learning with formal mathematical and physical reasoning to produce outputs that are verifiable, interpretable, and grounded in first principles. Rather than relying solely on statistical patterns, Axiomatic AI’s Lemma enables engineers and researchers to work with AI systems that can model, analyze, and validate complex technical problems with rigor. Axiomatic’s technology supports workflows across domains such as photonics, electronics, mechanics, and signal processing—helping teams accelerate design, extract insights from technical data, and ensure consistency with real-world constraints. By embedding verification directly into the AI process, Axiomatic reduces the gap between experimentation and reliable deployment. Axiomatic’s mission is to increase the velocity of scientific discovery and engineering innovation by building AI systems that scientists and engineers can trust.

Important Dates

The following is the tentative timeline of AIPV

Venue

AIPV2026 will take place at Hitotsubashi Hall in Tokyo, Japan (see also Google Maps).

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