<div dir="ltr">**** AAAI-23 Bridge Program on Deep Automated Program and Proof Synthesis (AP2S) **** <div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">February 7-8, Washington D.C. at AAAI-23</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0 gmail-x_elementToProof"><a href="https://garrettkatz.github.io/ap2s-bridge/" target="_blank" rel="noopener noreferrer">https://garrettkatz.github.io/ap2s-bridge/</a></div><div class="gmail-x_elementToProof"><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">*** Call for Participation ***</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">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.</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">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.</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">** Program Scope **</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">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.</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">Grand challenges envisioned for this bridge include:</div><div class="gmail-x_ContentPasted0">- Automatically synthesized constructive existence proofs for novel algorithms with improved complexity characteristics</div><div class="gmail-x_ContentPasted0">- Deciding as-yet unsolved conjectures by automatically synthesizing programs in the languages of interactive proof systems</div><div class="gmail-x_ContentPasted0">-
 "Executing" a partially developed proof on concrete examples as 
"input", similarly to running a program, to guide the automated proof 
synthesis process</div><div class="gmail-x_ContentPasted0">- State-of-the-art in both program and proof synthesis using a common core deep learning technique</div><div class="gmail-x_ContentPasted0">- Fast, automated program and proof repair when a dependency (software library or axiomatization) is changed</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">Topics for educational lectures/tutorials include:</div><div class="gmail-x_ContentPasted0">- Automated theorem proving techniques (e.g. resolution, paramodulation, term rewriting, etc.)</div><div class="gmail-x_ContentPasted0">- Automated program synthesis methods (e.g. abstraction domains, genetic programming)</div><div class="gmail-x_ContentPasted0">- Interactive proof systems (e.g. Metamath, Lean, Coq, Isabelle/HOL, etc.)</div><div class="gmail-x_ContentPasted0">- Automated proof systems (e.g. Vampire, E, etc.)</div><div class="gmail-x_ContentPasted0">- Deep learning techniques relevant to AP2S (e.g. transformers, graph neural networks, etc.)</div><div class="gmail-x_ContentPasted0">- Recent datasets relevant to AP2S (e.g. HOLStep, ProgRES, etc.)</div><div class="gmail-x_ContentPasted0">- Human reasoning processes during human program and/or proof synthesis</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">Extended abstracts may present current research or positions on:</div><div class="gmail-x_ContentPasted0">- Program and/or proof synthesis, automated and/or in humans, and with or without deep learning.</div><div class="gmail-x_ContentPasted0">- New datasets and benchmarks for AP2S</div><div class="gmail-x_ContentPasted0">- New directions or practices important to advance AP2S going forward</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">** Program Structure **</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">The bridge will be a one-day program with the following format:</div><div class="gmail-x_ContentPasted0">- Quarter-day session with lectures/tutorials related to automated theorem proving</div><div class="gmail-x_ContentPasted0">- Quarter-day session with lectures/tutorials related to automated program synthesis</div><div class="gmail-x_ContentPasted0">- Quarter-day session with lectures/tutorials related to relevant deep learning techniques</div><div class="gmail-x_ContentPasted0">- 5-minute lightning talks for selected posters</div><div class="gmail-x_ContentPasted0">- Group panel discussion on AP2S going forward</div><div class="gmail-x_ContentPasted0">- Speed-meeting networking session and social hour</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">Breaks in between sessions will be used for poster presentations of accepted abstracts.</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">** Target audience and attendance **</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">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.</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">** Submission Requirements **</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">Submissions are accepted in either of the following categories:</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">-
 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).</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">-
 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.</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">Submissions should be made on EasyChair at this link:</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0 gmail-x_elementToProof"><a href="https://easychair.org/conferences/?conf=ap2s" target="_blank" rel="noopener noreferrer">https://easychair.org/conferences/?conf=ap2s</a></div><div class="gmail-x_elementToProof"><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">** Important dates: **</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">- Friday, November 18, 2022: Deadline for Submissions</div><div class="gmail-x_ContentPasted0">- Friday, December 2, 2022: Notifications Sent to Authors</div><div class="gmail-x_ContentPasted0">- Monday, December 12, 2022: AAAI-23 Early Registration Deadline</div><div class="gmail-x_ContentPasted0">- February 7-8, 2023: AAAI-23 Bridge Program</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">** Bridge Chairs **</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">- Garrett Katz, Syracuse University, <a href="mailto:gkatz01@syr.edu">gkatz01@syr.edu</a></div><div class="gmail-x_ContentPasted0">- Kristopher Micinski, Syracuse University, <a href="mailto:kkmicins@syr.edu">kkmicins@syr.edu</a></div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">** Bridge webpage **</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0">For
 a copy of this CFP and more information (confirmed speakers, program 
schedule, recorded talks, etc.) see this web page for the bridge:</div><div><br class="gmail-x_ContentPasted0" aria-hidden="true"></div><div class="gmail-x_ContentPasted0 gmail-x_elementToProof"><a href="https://garrettkatz.github.io/ap2s-bridge/" target="_blank" rel="noopener noreferrer">https://garrettkatz.github.io/ap2s-bridge/</a></div></div>