Top Program Organizers Call for Participation

λ⊢∘

AP2S: Automated Program and Proof Synthesis Bridge Program

Program

When: February 7, 2023
Where: Walter E. Washington Convention Center, Room TBA

**Tentative Schedule, subject to change:

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

Program Synthesis using Transformers and Sequence Prediction Models [Slides]
Shirish Karande, TCS Research
Ganesh Prasath, TCS Research
9:30-10:15am

From Language Modeling to Grammar-Guided Code Sketch Generation [Slides]
Alexey Svyatkovskiy, Microsoft Research
10:30-11:00am

Staged Relational Programming for Synthesis
Nada Amin, Harvard University
William Byrd, University of Alabama at Birmingham
11:15am-12:00pm

Metamath and Metamath Zero [Slides]
Mario Carneiro, Carnegie Mellon University
1:00-1:55pm

Cross-over with Inductive Logic Programming tutorial
Andrew Cropper, University of Oxford
2:00-4:00pm

Opportunities for Synergy between Automated Program and Proof Synthesis Techniques
Group Discussion
4:30-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.

The AP2S bridge welcomes contributions in the form of educational lectures/tutorials and extended research abstracts. The majority of the program will consist of 30-45 minute lectures/tutorials, grouped by topic into 90 minute sessions. Time in between sessions will be allocated for poster presentations of accepted abstracts. The final session will include brief 5-minute lightning talks for selected posters, a group panel discussion, and a speed-meeting networking event.

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

Extended abstracts may present current research or positions on:

Program and/or proof synthesis, automated and/or in humans, and with or without deep learning.
New datasets and benchmarks for AP2S
New directions or practices important to advance AP2S going forward

Program Structure

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

Quarter-day session with lectures/tutorials related to automated theorem proving
Quarter-day session with lectures/tutorials related to automated program synthesis
Quarter-day session with lectures/tutorials related to relevant deep learning techniques
5-minute lightning talks for selected posters
Group panel discussion on AP2S going forward
Speed-meeting networking session and social hour

Breaks in between sessions will be used for poster presentations of accepted abstracts.

Target audience and attendance

The bridge aims to include 6-9 educational lectures/tutorials, 4-6 panel speakers, and 10-20 accepted posters, 5 of which will be selected for lightning talks. Space permitting, all are welcome to attend, with priority given to speakers, authors of accepted abstracts, their collaborators and students.

Submission Requirements

Submissions are accepted in either of the following categories:

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).
Extended abstracts should conform to the AAAI paper guidelines, and be a maximum of 4 pages excluding references. Abstracts will be accepted for poster presentation and a subset will be selected for 5-minute lightning talks at the bridge meeting.

Submissions should be made on EasyChair at this link.

Important dates:

~~Friday, November 18, 2022: Deadline for Submissions~~
~~Friday, December 2, 2022: Notifications Sent to Authors~~
~~Monday, December 12, 2022: AAAI-23 Early Registration Deadline~~
February 7, 2023, 8:30AM - 6:00PM EST: Bridge Workshop at AAAI-23

Bridge Chairs

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

Bridge webpage

https://garrettkatz.github.io/ap2s-bridge/ (this page)