Connectionists: Call for Participation: AAAI-23 Bridge Program on Deep Automated Program and Proof Synthesis (AP2S)

[Garrett Katz]

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

February 7-8, Washington D.C. at AAAI-23

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 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:

https://easychair.org/conferences/?conf=ap2s

** 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-8, 2023: AAAI-23 Bridge Program

** 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, recorded talks, 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/20221103/a1d6cad8/attachment.html>