Connectionists: Call for Participation: AAAI-24 Bridge Program on Deep Automated Program and Proof Synthesis

[Garrett Katz]

**** AAAI-24 Bridge Program on Deep Automated Program and Proof Synthesis
(AP2S) ****

February 20, 2024 at AAAI-24
Vancouver Convention Center
https://garrettkatz.github.io/ap2s-bridge/

*** 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 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.  We invite contributions in the form of educational lectures
and tutorials of 30, 45, or 90 minute durations.

*** 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, and each problem can 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

Topic areas 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 Format ***

This one-day bridge, scheduled for February 20, will consist of three
educational sessions, with presentations grouped by area, and a fourth
group discussion session.

*** Submission requirements ***

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 through Microsoft CMT at this link:

https://cmt3.research.microsoft.com/AP2S2024/Submission/Index

*** 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 at syr.edu
- Kristopher Micinski, Syracuse University, kkmicins at syr.edu

*** Bridge webpage ***

For a copy of this CFP and more information (confirmed speakers, program
schedule, lecture slides, etc.) see this web page for the bridge:

https://garrettkatz.github.io/ap2s-bridge/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.srv.cs.cmu.edu/pipermail/connectionists/attachments/20231110/2de5161b/attachment.html>