Work in progress: Making efficient use of language models for theorem proving

Add to your list(s) Download to your calendar using vCal

• Albert Qiaochu Jiang (University of Cambridge)
• Tuesday 08 March 2022, 13:15-14:15
• Zoom.

If you have a question about this talk, please contact Mateja Jamnik.

Join us on Zoom

Language models are neural networks trained on broad data and adaptable to a wide range of downstream tasks. They have shown impressive capabilities in domains such as NLP , vision, robotics, and reasoning. For mathematical reasoning, several SOTA results have been achieved by language models, but the huge computational cost prevents them from a wider adoption in the formal mathematics community. We introduce two methods to make efficient use of language models for theorem proving – one based on augmenting the language model prompt with previous proof steps and the other based on sampling output candidates of larger quantity and diversity. Our model improved the state-of-the-art theorem proving success rate on the Archive of Formal Proofs from 33.2% to 39.6%, without incurring any further computational cost.

This talk is part of the Artificial Intelligence Research Group Talks (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Artificial Intelligence Research Group Talks (Computer Laboratory)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge Forum of Science and Humanities
• Cambridge Language Sciences
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Guy Emerson's list
• Hanchen DaDaDash
• Interested Talks
• School of Technology
• Speech Seminars
• Trust & Technology Initiative - interesting events
• Zoom
• bld31
• ndk22's list
• ob366-ai4er
• rp587
• yk373's list
• yk449

Note that ex-directory lists are not shown.