What's On arrow

AI talk: Professor Lawrence Paulson FRS on Automated Theorem Proving

18:30 Pull up a groove and get fabulous! (AKA registration – please arrive early) 19:00 Scheduled talk: “Automated Theorem Proving: A Technology Roadmap” 20:00 Pizza pizza pizza pizza pizza! (Stimulating conversation encouraged…) 21:00 Event close – you don’t have to go home, but you can’t stay here!

  • 8th March 2023 - 8th March 2023
  • 6:30 pm - 9:00 pm

Where

Bradfield Centre

184 Cambridge Science Park

Milton Road

Cambridge

CB4 0GA

When

Wednesday, 8 March 2023

Tickets

  • Please note that this is a ticket only event – you must have a ticket to attend
  • Tickets are £11.80 + VAT and may be purchased here
  • PLACES ARE STRICTLY LIMITED – PLEASE BOOK EARLY TO AVOID MISSING OUT!

Agenda

18:30 Pull up a groove and get fabulous! (AKA registration – please arrive early)

19:00 Scheduled talk: “Automated Theorem Proving: A Technology Roadmap”

20:00 Pizza pizza pizza pizza pizza! (Stimulating conversation encouraged…)

21:00 Event close – you don’t have to go home, but you can’t stay here!

Introduction

With the November 2022 release of OpenAI’s ChatGPT, the rate of advance in AI has seemingly gone from meteoric to meteoric on steroids. But many commentators have expressed doubts that Large Language Models such as ChatGPT are truly intelligent.

What do advanced AI systems need in order to be able to think rationally? Not just give the impression that they are doing so (to a lay and impressionable observer), but for real…?

Consider the following: If all cats are crazy, and Jonathan is a cat, then Jonathan is crazy.

This is an example of deduction, one of the three primary modes of reasoning (along with induction and abduction) underlying critical thought and general problem solving. Any advanced AI system currently on the drawing board with ambitions of becoming a general problem solver, or AGI (Artificial General Intelligence), will unavoidably need to perform reliable deduction somehow, either as an explicit high-level function or as an emergent property of its low-level behaviour, and every AI researcher with an interest in AGI – or AI company with ambitions to become an AGI company – needs to know about deduction.

The art of getting a mindless automaton (a.k.a. computer) to perform deduction is called Automated Theorem Proving (ATP), and Professor Paulson has been a recognised world leader in ATP for over 40 years. Who better than Professor Paulson to deliver the inaugural CAIS talk at the Bradfield Centre, Cambridge, on Wednesday 8 March? No one, that’s who!

About the talk

Title: “Automated Theorem Proving: a Technology Roadmap”

Abstract: The technology of automated deduction has a long pedigree. For ordinary first-order logic, the basic techniques had all been invented by 1965: DPLL (for large Boolean problems) and the tableau and resolution calculi (for quantifiers). The relationship between automated deduction and AI has been complex: does intelligence emerge from deduction, or is it the other way around? Interactive theorem proving further complicates the picture, with a human user working in a formal calculus much stronger than first-order logic on huge, open-ended verification problems and needing maximum automation. Isabelle is an example of a sophisticated interactive prover that also relies heavily on automatic technologies through its nitpick and sledgehammer subsystems. The talk will give an architectural overview of Isabelle and its associated tools. The speaker will also speculate on how future developments, especially machine learning, could assist (not replace) the user.

About the speaker

Paulson graduated from the California Institute of Technology with a BS in Mathematics in 1977, and obtained a PhD in Computer Science from Stanford University in 1981. After a brief spell as a research assistant at Edinburgh University, Paulson moved to Cambridge University in 1983, where he has been ever since. Elevated to Professor of Computational Logic in 2002, a position he held for 20 years, Paulson has been Director of Research at the University of Cambridge Computer Laboratory since 2022. Paulson was elected Fellow of the ACM (Association of Computing Machinery) in 2008, and Fellow of the Royal Society in 2017. He has been an editor of the Journal of Automated Reasoning for many years, and a trustee of the Conference on Automated Deduction (CADE) since 2010.

About CAIS

Cambridge AI Social (CAIS) seeks to deliver a series of in-person “AI + pizza” events in Cambridge (one of Europe’s hottest AI hubs) throughout 2023 (and beyond!)

Fundamental to the CAIS vision are:

  • speakers must be a recognised world leader in their field
  • events are non-profit, with minimal cost to attendees
  • each event comprises a roughly one-hour talk followed by socialisation (with pizza!) 

Sponsors

CAIS would not be possible without the support of its sponsors:

Please note

  • This is an in-person event (audience and speaker), and will not be livestreamed.
  • A recording of the talk, and images of the event, will subsequently be posted online.
  • In particular, CAIS may license the event video to e.g. commercial VoD channels.
  • Please do not attend if you have COVID-, cold-, or flu-like symptoms.
  • We reserve the right to refuse admission to anyone for any reason.
icon

Did you know?

One of Cambridge’s most beloved community events is the Mill Road Winter Fair, which takes place annually on the first Saturday in December. Offering stalls, entertainment and a parade, it’s been running since 2005 and attracts around 15,000 people a year.