Kindly register for the online talk here: https://nus-sg.zoom.us/webinar/register/WN_KXVjj8hzQuCEcscgw4S_QA

Abstract:

Language models can produce convincing answers, but how do we check whether their reasoning is correct? Vikash will discuss how translating natural language into logical constraints allows SMT solvers such as Z3 to check claims and provide feedback that improves reasoning. Yet a solver can correctly check the wrong formulation, so checking the translation itself is essential. He’ll explore how formal checks, model refinement and the detection of translation errors can address this challenge. He’ll also show how verified policy checkers built with Lean evaluate tool calls before execution, extending verification from model reasoning to AI agent actions.

Vikash is a PhD student in Computer Science at Case Western Reserve University, advised by Professor Vipin Chaudhary. His research combines language models with SMT solvers and theorem provers to verify reasoning, identify errors in natural-language-to-logic translations and enforce policies on agent actions. His broader interests include uncertainty quantification and efficient AI systems.