Title:
Autoformalization with Large Language Models

13:30 - 14:30, Dec. 2, 2023, UTC+8.

Yuhuai(Tony) Wu

Yuhuai Wu, the Co-Founder of xAI, completed his postdoc at Stanford and his Ph.D. from the University of Toronto. His primary interest lies in developing models for reliable reasoning, with a specific emphasis on solving math. His previous research on mathematical reasoning was featured in the New York Times and Quanta Magazine.

Abstract:
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. While the long-term goal of autoformalization seemed elusive for a long time, we show large language models provide new prospects towards this goal.