<div dir="ltr">**** AAAI-24 Bridge Program on Deep Automated Program and Proof Synthesis (AP2S) ****<br><br>February 20, 2024 at AAAI-24<br>Vancouver Convention Center<br><a href="https://garrettkatz.github.io/ap2s-bridge/">https://garrettkatz.github.io/ap2s-bridge/</a><br><br>*** Call for Participation ***<br><br>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.<br><br>*** Program Scope ***<br><br>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:<br><br>- Automatically synthesized constructive existence proofs for novel algorithms with improved complexity characteristics<br>- Deciding as-yet unsolved conjectures by automatically synthesizing programs in the languages of interactive proof systems<br>- "Executing" a partially developed proof on concrete examples as "input", similarly to running a program, to guide the automated proof synthesis process<br>- State-of-the-art in both program and proof synthesis using a common core deep learning technique<br>- Fast, automated program and proof repair when a dependency (software library or axiomatization) is changed<br><br>Topic areas for educational lectures/tutorials include:<br><br>- Automated theorem proving techniques (e.g. resolution, paramodulation, term rewriting, etc.)<br>- Automated program synthesis methods (e.g. abstraction domains, genetic programming)<br>- Interactive proof systems (e.g. Metamath, Lean, Coq, Isabelle/HOL, etc.)<br>- Automated proof systems (e.g. Vampire, E, etc.)<br>- Deep learning techniques relevant to AP2S (e.g. transformers, graph neural networks, etc.)<br>- Recent datasets relevant to AP2S (e.g. HOLStep, ProgRES, etc.)<br>- Human reasoning processes during human program and/or proof synthesis<br><br>*** Program Format ***<br><br>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.<br><br>*** Submission requirements ***<br><br>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).<br><br>Submissions should be made through Microsoft CMT at this link:<br><br><a href="https://cmt3.research.microsoft.com/AP2S2024/Submission/Index">https://cmt3.research.microsoft.com/AP2S2024/Submission/Index</a><br><br>*** Important dates: ***<br><br>- November 24, 2023: Deadline for submissions<br>- Friday, December 11, 2023: Submission decision notifications posted<br>- Monday, December 20, 2023: Early registration deadline<br>- February 20, 2024, 9:00AM - 5:00PM: Bridge Workshop at AAAI-24<br><br>*** Bridge Chairs ***<br><br>- Garrett Katz, Syracuse University, <a href="mailto:gkatz01@syr.edu">gkatz01@syr.edu</a><br>- Kristopher Micinski, Syracuse University, <a href="mailto:kkmicins@syr.edu">kkmicins@syr.edu</a><br><br>*** Bridge webpage ***<br><br>For a copy of this CFP and more information (confirmed speakers, program schedule, lecture slides, etc.) see this web page for the bridge:<br><br><a href="https://garrettkatz.github.io/ap2s-bridge/">https://garrettkatz.github.io/ap2s-bridge/</a><br></div>