# VerifAI: AI Verification in the Wild

## Overview
This workshop explores the intersection of scale-driven generative artificial intelligence (AI) and the correctness-focused principles of verification.

Formal analysis tools such as theorem provers, satisfiability solvers, and execution monitoring have demonstrated success in ensuring properties of interest across a range of tasks in software development and mathematics where precise reasoning is necessary. However, these methods face scaling challenges. Recently, generative AI such as large language models (LLMs) has been explored as a scalable and adaptable option to create solutions in these settings. The effectiveness of AI in these settings increases with more compute and data, but unlike traditional formalisms, they are built around probabilistic methods – not correctness by construction.

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.

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