SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Sat 18 Oct 2025 13:45 - 14:00 at Orchid Plenary Ballroom - Synthesis 2

The goal of active learning for program synthesis is to synthesize the desired program by asking targeted questions that minimize user interaction. While prior work has explored active learning in the purely symbolic setting, such techniques are inadequate for the increasingly popular paradigm of neurosymbolic program synthesis, where the synthesized program incorporates neural components. When applied to the neurosymbolic setting, such techniques can — and, in practice, do — return an unintended program due to mispredictions of neural components. This paper proposes a new active learning technique that can handle the novel challenges posed by neural network mispredictions. Our approach is based upon a new evaluation strategy called constrained conformal evaluation (CCE), which accounts for neural mispredictions while taking into account user-provided feedback. Our proposed method iteratively makes CCE more precise until all remaining programs are guaranteed to be observationally equivalent. We have implemented this method in a tool called SmartLabel and experimentally evaluated it on two neurosymbolic domains. Our results demonstrate that SmartLabel identifies the ground truth program for 98% of the benchmarks, requiring under 5 rounds of user interaction on average. In contrast, prior techniques for active learning are only able to converge to the ground truth program for 65% of the benchmarks.

This program is tentative and subject to change.

Sat 18 Oct

Displayed time zone: Perth change

13:45 - 15:30
13:45
15m
Talk
Active Learning for Neurosymbolic Program Synthesis
OOPSLA
Celeste Barnaby University of Texas at Austin, Jocelyn Qiaochu Chen New York University, University of Alberta, Ramya Ramalingam University of Pennsylvania, Osbert Bastani University of Pennsylvania, Işıl Dillig University of Texas at Austin
14:00
15m
Talk
Language-Parametric Reference Synthesis
OOPSLA
Daniel A. A. Pelsmaeker Delft University of Technology, Netherlands, Aron Zwaan Delft University of Technology, Casper Bach University of Southern Denmark, Arjan J. Mooij Zürich University of Applied Sciences
14:15
15m
Talk
Multi-Modal Sketch-based Behavior Tree Synthesis
OOPSLA
Wenmeng Zhang College of Computer Science and Technology, National University of Defense Technology, Changsha, China, Zhenbang Chen College of Computer, National University of Defense Technology, Weijiang Hong National University of Defense Technology, Changsha, China
14:30
15m
Talk
Synthesizing DSLs for Few-Shot Learning
OOPSLA
Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
14:45
15m
Talk
Synthesizing Implication Lemmas for Interactive Theorem Proving
OOPSLA
Ana Brendel University of Texas at Austin, Aishwarya Sivaraman Meta, Todd Millstein University of California at Los Angeles
15:00
15m
Talk
Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
OOPSLA
Jacob Laurel Georgia Institute of Technology, Ignacio Laguna Lawrence Livermore National Laboratory, Jan Hueckelheim Argonne National Laboratory
15:15
15m
Talk
Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
OOPSLA
Guanlin Chen Peking University, Ruyi Ji Peking University, Shuhao Zhang Peking University, Yingfei Xiong Peking University