Verified Autonomy: Why Large Language Models Alone Aren't Enough, and What a Neuro-Formal Stack Looks Like

Title of the Talk: Verified Autonomy: Why Large Language Models Alone Aren’t Enough, and What a Neuro-Formal Stack Looks Like
Host Faculty: Dr.Ashish Mishra
Speaker: Mr.Aditya Vempaty
Date: 19 August
Time: 11:00 am
Venue: CSE Seminar Hall

Abstract
Large language models have gotten astonishingly good at short, exam-style tasks, but the moment we ask them to operate autonomously over long horizons, to compose across agents, or to touch systems where a bad decision costs millions, they fail in ways that no amount of scaling seems to fix. Emergence AI’s recent Emergence World study makes this concrete: give ten agents fifteen days in a live, tool-grounded world and some frontier models collapse entirely, some drift into rubber-stamp governance, and, most sobering, populations of well-behaved agents can be contaminated into rule-breaking by a single misaligned peer. The relevant unit of safety is the deployed system, not the model.

In this talk, we argue that closing this gap requires a neuro-formal stack: LLMs handle proposal, negotiation, and natural-language interfaces while formal methods - SMT solvers, proof assistants, verified kernels — hold the load-bearing correctness guarantees and surface actionable diagnostics when the world violates assumptions. We’ll show how we’ve been learning to build this stack by grounding it in real domains: airline irregular-operations recovery, where a Z3 pre-feasibility gate and Lean 4 proven repair functions turn a silent 1.5-second wrong answer into a 20-millisecond unsat core with concrete relaxations; and semiconductor post-silicon test-data analysis, where a 69-rule Lean 4 kernel lifts an LLM’s bug-detection recall from ~0.60 to ~0.97 and, critically, widens that gap as bugs interact — a knowledge gap that a stronger model does not close. We’ll close with early results from a general-purpose verifiable code-generation tool, which turns natural-language requirements into pip-installable Python packages whose core components carry Dafny or Lean proofs into runtime precondition enforcement.

Bio

Aditya Vempaty is a Research Scientist at Emergence AI, where he works on verified autonomous systems, combining large language models with formal verification methods to build agents that are provably correct in the domains where correctness matters. His current work spans a general-purpose verifiable code-generation pipeline, a Lean-4 kernel for semiconductor post-silicon analysis, a neuro-formal recovery system for airline irregular operations, and Emergence World — a long-horizon multi-agent evaluation platform. Prior to Emergence AI, Aditya held research role at IBM Research, and holds a Ph.D. in Electrical Engineering and Computer Science from Syracuse University. He has published widely on machine learning, human–AI collaboration, and inference over noisy signals, and co-authored the book Secure Networked Inference with Unreliable Data Sources (Springer, 2018).