AI-Assisted Autoformalization of Combinatorics Problems in Proof Assistants
Formal Methods
This program is tentative and subject to change.
Proof assistants such as Coq and \textsf{LEAN} have been increasingly used by renowned mathematicians to formalize and prove mathematical theorems. Despite their growing use, writing formal proofs is challenging, as it requires a deep understanding of these systems’ languages. Recent advancements in AI, especially LLMs, have shown promise in automating this formalization task. However, domains such as combinatorics pose significant challenges for AI-assisted proof assistant systems due to their cryptic nature and the lack of existing data to train AI models.
We introduce \textsf{AutoForm4Lean}, a system designed to leverage LLMs to aid in formalizing combinatorics problems for \textsf{LEAN}. By combining LLM power with SE/FM techniques such as synthesis and validation, \textsf{AutoForm4Lean} generates formalizations of combinatorics problems more effectively than current state-of-the-art LLMs. Moreover, this project seeks to provide a comprehensive collection of formalized combinatorics problems, theorems and lemmas, which would enrich the \textsf{LEAN} library and provide valuable training data for LLMs. Preliminary results demonstrate the effectiveness of \textsf{AutoForm4Lean} in formalizing combinatorics problems in \textsf{LEAN}, making a step forward in AI-based theorem proving.
This program is tentative and subject to change.
Wed 30 AprDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30 | |||
11:00 15mTalk | SpecGen: Automated Generation of Formal Program Specifications via Large Language ModelsFormal Methods Research Track Lezhi Ma Nanjing University, Shangqing Liu Nanyang Technological University, Yi Li Nanyang Technological University, Xiaofei Xie Singapore Management University, Lei Bu Nanjing University | ||
11:15 15mTalk | Gpass: a Goal-adaptive Neural Theorem Prover based on Coq for Automated Formal VerificationFormal Methods Research Track Yizhou Chen Peking University, Zeyu Sun Institute of Software, Chinese Academy of Sciences, Guoqing Wang Peking University, Dan Hao Peking University | ||
11:30 15mTalk | AI-Assisted Autoformalization of Combinatorics Problems in Proof AssistantsFormal Methods New Ideas and Emerging Results (NIER) | ||
11:45 15mTalk | Formally Verified Binary-level Pointer AnalysisFormal Methods Research Track Freek Verbeek Open Universiteit & Virginia Tech, Ali Shokri Virginia Tech, Daniel Engel Open University Of The Netherlands, Binoy Ravindran Virginia Tech | ||
12:00 15mTalk | EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution FrameworkFormal Methods Research Track ziji wu National University of Defense Technology, yu huang National University of Defense Technology, peishan huang National University of Defense Technology, shanghua wen National University of Defense Technology, minglong li National University of Defense Technology, Ji Wang National University of Defense Technology | ||
12:15 7mTalk | SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code GenerationFormal Methods New Ideas and Emerging Results (NIER) Junjie Sheng East China Normal University, Yanqiu Lin East China Normal University, Jiehao Wu East China Normal University, Yanhong Huang East China Normal University, Jianqi Shi East China Normal University, Min Zhang East China Normal University, Xiangfeng Wang East China Normal University | ||
12:22 7mTalk | Listening to the Firehose: Sonifying Z3’s BehaviorFormal Methods New Ideas and Emerging Results (NIER) | ||