Top Program Organizers Call for Participation

λ⊢∘

AP2S: Automated Program and Proof Synthesis

Automated Program and Proof Synthesis (AP2S) are two long-standing, closely-related challenges in AI, recently advanced through the incorporation of deep learning. However, much research focuses exclusively on one or the other, instead of leveraging synergies between them. This bridge workshop, a continuation of last year's 2023 inaugural meeting, aims to connect researchers from each sub-field and educate them about the other, including but not limited to recent applications of deep learning. The workshop will involve a series of tutorial lectures followed by group discussion.

Program

When: February 20, 2024
Where: Vancouver Convention Centre -- West Building, Room TBA

**Tentative Schedule, subject to change:

Opening Remarks
Garrett Katz, Syracuse University
9:00-9:15am

Session 1: Program Synthesis
Speakers TBA
9:30-10:30am

Session 2: Interactive Proof Systems
Speakers TBA
11:00am-12:30pm

Session 3: Automated Theorem Proving
Speakers TBA
2:00pm-3:30pm

Session 4: Group/Panel Discussion
Speakers TBA
4:00pm-5:00pm

Organizers

	Garrett Katz Syracuse University
	Kristopher Micinski Syracuse University

Call for Participation

Automated Program and Proof Synthesis (AP2S) are two long-standing, closely-related challenges in AI, recently advanced through the incorporation of deep learning. However, much research focuses exclusively on one or the other, instead of leveraging synergies between them. This bridge program aims to connect researchers from each sub-field and educate them about the other, including but not limited to recent deep-learning techniques. Contributions are welcome in the form of educational lectures and tutorials.

Program Scope

The focus of the bridge is on underlying principles common to both program and proof synthesis. Both problems involve document generation in strict formal languages, leveraging large structured prior "knowledge" (known theorems or existing software libraries), navigating vast search spaces (possible proofs and programs), and high-level cognitive abilities (creativity and abstraction). Both problems have witnessed recent advances with deep learning, making this program especially timely. Each problem can also be framed as an instance of the other. Grand challenges envisioned for this bridge include:

Automatically synthesized constructive existence proofs for novel algorithms with improved complexity characteristics
Deciding as-yet unsolved conjectures by automatically synthesizing programs in the languages of interactive proof systems
"Executing" a partially developed proof on concrete examples as "input", similarly to running a program, to guide the automated proof synthesis process
State-of-the-art in both program and proof synthesis using a common core deep learning technique
Fast, automated program and proof repair when a dependency (software library or axiomatization) is changed

Topics for educational lectures/tutorials include:

Automated theorem proving techniques (e.g. resolution, paramodulation, term rewriting, etc.)
Automated program synthesis methods (e.g. abstraction domains, genetic programming)
Interactive proof systems (e.g. Metamath, Lean, Coq, Isabelle/HOL, etc.)
Automated proof systems (e.g. Vampire, E, etc.)
Deep learning techniques relevant to AP2S (e.g. transformers, graph neural networks, etc.)
Recent datasets relevant to AP2S (e.g. HOLStep, ProgRES, etc.)
Human reasoning processes during human program and/or proof synthesis

Program Structure

The bridge will be a one-day program with the following format:

Quarter-day session with lectures/tutorials related to automated program synthesis
Quarter-day session with lectures/tutorials related to interactive proof systems
Quarter-day session with lectures/tutorials related to automated theorem proving
Quarter-day session for group discussion

Each session will be separated by a coffee or lunch break.

Target audience and attendance

The bridge aims to include 6-9 educational lectures/tutorials and 20-40 attendees. Space permitting, all are welcome to attend, with priority given to speakers, their collaborators, and students.

Submission Requirements

Proposals for educational lecture/tutorials should include draft presentation slides in PDF format, CVs of the speaker(s) in 2-page NSF Biosketch Format, and a brief cover page. The cover page must include a paragraph summary of the talk, a proposed duration (either 30, 45, or 90 minutes), and the names, affiliations, and contact information for the speaker(s).

Submissions should be made on Microsoft CMT here.

Important dates:

November 24, 2023: Deadline for submissions
Friday, December 11, 2023: Submission decision notifications posted
Monday, December 20, 2023: Early registration deadline
February 20, 2024, 9:00AM - 5:00PM: Bridge Workshop at AAAI-24

Bridge Chairs

Garrett Katz, Syracuse University, gkatz01@syr.edu
Kristopher Micinski, Syracuse University, kkmicins@syr.edu