Formalizing Knowledge at Scale – Arnav Mehta, Pramaana Labs

Abstract:

"Recent advances in AI have made generating answers easy, but verifying their correctness remains a fundamental challenge. This talk explores how machine-checkable proofs and formal methods can extend beyond mathematics to real-world domains such as law, taxation, and security protocols.

A central challenge in this effort is translating rules expressed in natural language into precise formal representations. I will present Pramaana's approach to domain formalization, emphasizing how the design of a formal language shapes the tractability of downstream reasoning. I will also discuss auto-formalization: translating ambiguous human questions into precise specifications through interactive AI systems.

Finally, I will examine how reasoning in real-world domains differs from mathematical proof and motivate hybrid architectures that combine large language models with SMT solvers. The talk will conclude with Pramaana's broader research agenda toward scalable formalization across domains."

Speaker: https://www.linkedin.com/in/arnav-mehta-b92420219/

_____

Also, Philippe Dumonet will be giving a lightning talk on "Representing Non-Terminating Computation using iTrees"

Speaker: https://x.com/real_philogy

_____

The SF Lean meetup: Weekly presentations and discussions about formal methods, software verification, AI, and math. Beginners welcome!

Website: https://sflean.group/
Join our Discord server: https://discord.com/invite/bXNPhQyjfe