Call for Papers

In the VerifAI: AI Verification in the Wild workshop we invite papers and discussions that discuss how to bridge the fields of formal analysis and artificial intelligence. Potential angles include, but are not limited to the following:

• Generative AI for formal methods: Formal methods offer strong guarantees of desired or undesired properties, but they can be challenging to implement. When faced with nonhalting proofs or extensive search spaces, machine learning approaches can help guide those search processes effectively and LLMs may even write the theorems themselves. How can we further integrate AI to enhance verification practices? How can we ensure that AI-generated test conditions align with actual desired properties?

• Formal methods for generative AI: Generative AI can benefit from formal methods, which provide assurance and thus build trust. For example, satisfiability solvers can be used as a bottleneck in reasoning domains, code generated by the model can be annotated with specifications for program analysis tools to ensure its correctness, and even simple symbolic methods such as automata simulators can steer AI generations towards more logically consistent behavior. How else can we integrate formal methods into generative AI development and usage?

• AI as verifiers: Hard guarantees can be notoriously rigid and difficult to achieve. In these cases, probabilistic methods are appealing alternatives to provide “soft assurances”. How can we develop more robust and trustworthy verifiers from probabilistic methods? In what settings is it appropriate to make verification more flexible using probabilistic methods?

• Datasets and benchmarks: The advancement of research at the intersection of generative AI and formal methods relies heavily on the availability of robust datasets and benchmarks. We welcome papers that present new datasets and benchmarks in reasoning, theorem proving, code generation, and related areas. How can we design benchmarks that accurately reflect the challenges in combining probabilistic models with formal (or informal) verification?

• Special Theme: LLMs for Code Generation: The use of LLMs for code generation has grown significantly, with a growing body of research advocating for the integration of formal structures and tools, such as context-free grammars , static analyzers , and SMT-guided repair . These methods aim to improve both the safety and effectiveness of code generated by LLMs, particularly for low-resource programming languages. In the context of code generation, LLM agents can leverage tool use and learning from execution feedback to validate their generations. This year, our special theme invites researchers to explore how techniques from programming languages and formal methods communities can further enhance LLM-driven code generation.

• Tiny and short papers: We have a separate track for tiny papers. The goal is to encourage submissions of budding findings that are modest but interesting, have not yet have had the resources to execute full-scale experiments, or are a fresh perspective on existing ideas.

We welcome novel methodologies, analytic contributions, works in progress, negative results, and positional papers that will foster discussion.

Important Dates

Paper submission opens: January 6, 2025
Deadline for paper submission: February 3, 2025
Notification: March 5, 2025
Camera Ready: March 20, 2025
Workshop: April 27/28, 2025

Submission Requirements

Submissions to VerifAI are limited to 8 pages of content for regular submissions, and 2 pages of content for tiny papers.

Outside of the content page limit, submissions may also contain an unlimited number of pages for references and appendices. These may not necessarily be read by the reviewers. We request and recommend that authors rely on the supplementary material only to include minor details (e.g., hyperparameter settings, reproducibility information, etc.) that do not fit in the main content pages pages. The review process is double-blind, so please ensure that all papers are appropriately anonymised.

All submissions must be formatted with LaTeX using the ICLR paper format.

All accepted papers will be presented in an in-person poster session, and some will be selected for oral presentation. We also permit papers that have been recently published or are under submission to another venue. Please mark such papers accordingly upon submission. Accepted papers will be displayed on the VerifAI homepage, but are to be considered non-archival.

Submit here: OpenReview portal.