BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1747
DTSTAMP:20260714T094646Z
SUMMARY:Formal Verification for the Real World
DESCRIPTION:Speaker: Arnav Mehta (Pramaana Labs & UC Berkeley)\n\nAbstract:
  \nRecent advances in AI have made generating answers easy\, but verifying
  their correctness remains a great challenge. Mathematics offers a notion 
 of trust: machine-checkable proof. In this talk we explore how this paradi
 gm can be extended beyond mathematics to real-world domains such as law\, 
 taxation\, security protocols\, and institutional rule systems.\nThis talk
  will begin with an introduction to formalization for mathematics in Lean4
 \, discussing the Curry–Howard correspondence\, the intuition behind int
 eractive theorem proving\, and how modern proof assistants are transformin
 g mathematical collaboration. The primary challenge in applying these idea
 s outside mathematics is formalizing domains whose rules are encoded in na
 tural language.\nI will present our approach to domain formalization\, mot
 ivated by the observation that the design of a formal language fundamental
 ly shapes the tractability of downstream reasoning. I will also discuss th
 e emerging challenge of auto-formalization: translating ambiguous human qu
 estions into formal specifications through interactive AI systems.\nFinall
 y\, I will examine how proving in real-world domains differs from proving 
 in mathematics\, motivating hybrid architectures that combine large langua
 ge models and SMT solvers. I will conclude by outlining Pramaana's broader
  research agenda toward scalable formalization across domains. Our central
  thesis is that many difficult problems can be made tractable via formaliz
 ation.\nBio: Arnav Mehta is a researcher at Pramaana Labs\, where he work
 s at the intersection of artificial intelligence and formal methods. His r
 esearch focuses on auto-formalization\, the problem of translating natural
  language specifications into formal representations\, and on building AI 
 systems for theorem proving. He received his master's degree from the Univ
 ersity of California\, Berkeley\, where his thesis investigated evaluation
  metrics for auto-formalization and introduced LeanTutor\, a natural langu
 age interface for students to receive formally verified feedback on their 
 proofs. At Pramaana\, he is developing methods to scale formal verificatio
 n beyond mathematics to domains such as law\, taxation\, finance\, and sec
 urity protocols.\n \n
URL:https://www.tcs.tifr.res.in/web/events/1747
DTSTART;TZID=Asia/Kolkata:20260720T160000
DTEND;TZID=Asia/Kolkata:20260720T170000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR