Tata Institute of Fundamental Research
Formal Verification for the Real World
STCS Seminar
Speaker:
Arnav Mehta (Pramaana Labs & UC Berkeley)
Organiser:
Jatin Batra
Date:
Monday, 20 Jul 2026, 16:00 to 17:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
Recent 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 paradigm can be extended beyond mathematics to real-world domains such as law, taxation, security protocols, and institutional rule systems.
This talk will begin with an introduction to formalization for mathematics in Lean4, discussing the Curry–Howard correspondence, the intuition behind interactive theorem proving, and how modern proof assistants are transforming mathematical collaboration. The primary challenge in applying these ideas outside mathematics is formalizing domains whose rules are encoded in natural language.
I will present our approach to domain formalization, motivated by the observation that the design of a formal language fundamentally shapes the tractability of downstream reasoning. I will also discuss the emerging challenge of auto-formalization: translating ambiguous human questions into formal specifications through interactive AI systems.
Finally, I will examine how proving in real-world domains differs from proving in mathematics, motivating hybrid architectures that combine large language 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 formalization.
Bio: Arnav Mehta is a researcher at Pramaana Labs, where he works at the intersection of artificial intelligence and formal methods. His research 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 University of California, Berkeley, where his thesis investigated evaluation metrics for auto-formalization and introduced LeanTutor, a natural language interface for students to receive formally verified feedback on their proofs. At Pramaana, he is developing methods to scale formal verification beyond mathematics to domains such as law, taxation, finance, and security protocols.
| Speaker: | Arnav Mehta (Pramaana Labs & UC Berkeley) |
| Organiser: | Jatin Batra |
| Date: | Monday, 20 Jul 2026, 16:00 to 17:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Recent 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 paradigm can be extended beyond mathematics to real-world domains such as law, taxation, security protocols, and institutional rule systems.
This talk will begin with an introduction to formalization for mathematics in Lean4, discussing the Curry–Howard correspondence, the intuition behind interactive theorem proving, and how modern proof assistants are transforming mathematical collaboration. The primary challenge in applying these ideas outside mathematics is formalizing domains whose rules are encoded in natural language.
I will present our approach to domain formalization, motivated by the observation that the design of a formal language fundamentally shapes the tractability of downstream reasoning. I will also discuss the emerging challenge of auto-formalization: translating ambiguous human questions into formal specifications through interactive AI systems.
Finally, I will examine how proving in real-world domains differs from proving in mathematics, motivating hybrid architectures that combine large language 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 formalization.
Bio: Arnav Mehta is a researcher at Pramaana Labs, where he works at the intersection of artificial intelligence and formal methods. His research 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 University of California, Berkeley, where his thesis investigated evaluation metrics for auto-formalization and introduced LeanTutor, a natural language interface for students to receive formally verified feedback on their proofs. At Pramaana, he is developing methods to scale formal verification beyond mathematics to domains such as law, taxation, finance, and security protocols.