November 26th, Stewart House, London

Welcome to Towards General Autoformalization, our first multi-disciplinary autoformalization workshop at Royal Holloway, University of London.

Large language models routinely translate natural language into formal languages that machines can check and reason with: proofs in Lean or Isabelle, logical formulas, Prolog programs, PDDL plans, ontologies, and more. We call this task “autoformalization”, and we think that understanding it well is central to building AI that we can trust. So far we see that researchers in mathematics, verification, planning, and knowledge representation often tackle the same autoformalization problems separately and under different names. In this workshop, we aim to bring together researchers in these communities from across the UK, to share benchmarks, methods, and ideas, and to help shape a common foundation for autoformalization and (through it) reliable and verifiable AI.

Program

9am: Doors open

9:15am to 9:30am: Welcome

9:30am to 10:30am: Presentation Session 1

10:30am to 11am: Coffee Break

11am to 12:30pm: Presentation Session 2

12:30pm to 1:45pm: Lunch

1:45pm to 3:15pm: Presentation Session 3

3:15pm to 3:45pm: Coffee Break

3:45pm to 4:45pm: Panel

4:45pm to 5pm: Closing Remarks

Venue

The Workshop will take place from 9am to 5pm in: Stewart House, Room 2 32 Russell Square, London WC1B 5DN

Getting There

Stewart House, Royal Holloway’s London campus, is in the heart of Bloomsbury, London. Public transport is the easiest way to reach us.

By Underground

By train King’s Cross St Pancras and Euston: about 15–20 minutes on foot, or take the Piccadilly line one stop from King’s Cross to Russell Square.

Organisation