Abstract Synthesis

Andrew Cropper, logic luminary and creator of the popular Popper, discusses the paper "Inductive Logic Programming at 30: A New Introduction."This episode examines how inductive logic programming (ILP) learns symbolic rules from examples and background knowledge, and what it takes to build ILP systems that scale. As machine learning has shifted toward opaque, data-hungry models, ILP offers a path to interpretable, constrained programs learned from data. The paper distills 30 years of ideas (learning settings, bias, search, recursion, predicate invention, and system design) into a modern entry point for symbolic generalization.Cropper reflects on how the paper emerged alongside his work on Popper, a high-performance ILP system designed around falsification and solver-backed search. He traces this line of thinking back to his training under Stephen Muggleton, the most influential researcher in ILP.In This Episode -

• Inductive bias to constrain search.• Utilizing SAT/ASP-style engines as solver tools.• Why recursion is a decisive capability for true generalization on algorithmic tasks.• Predicate invention enabling more compact programs and better abstraction.• Popper’s core idea: learning by ruling out hypotheses via failures.• A practical research workflow advantage: adding constraints to prune search can yield orders-of-magnitude speedups without rewriting the learner.• ILP in the wild: scientific discovery loops (the "Robot Scientist" pattern), program-by-example tools (Flash Fill), and rule learning to guide RL agents.References -

• https://arxiv.org/abs/2008.07912• https://github.com/logic-and-learning-lab/Popper/• https://www.cs.cmu.edu/~tom/mlbook.html• https://europepmc.org/abstract/MED/14724639• https://www.microsoft.com/en-us/research/publication/automating-string-processing-spreadsheets-using-input-output-examples/About the Paper -

"Inductive logic programming at 30: a new introduction"Andrew Cropper, Sebastijan Dumančić

Journal of Artificial Intelligence Research (JAIR), 2022The paper explains how ILP learns symbolic rules from labeled examples plus background knowledge, and it breaks down ILP system design into learning settings, bias/representation choices, and search strategies. It also surveys major systems and practical limitations, framing modern ILP around solver-backed search, recursion, and predicate invention.https://arxiv.org/abs/2008.07912About the Guest -

Andrew Cropper is an Associate Professor at the University of Helsinki and a principal investigator at ELLIS Institute Finland, where he works on combining logical reasoning with machine learning. His research centers on inductive logic programming and on building high-performance ILP systems (including Popper) that leverage modern SAT/ASP/MaxSAT solving to learn interpretable rules from data.https://andrewcropper.com/Credits -

• Host & Music: Bryan Landers, Technical Staff, Ndea

• Editor: Alejandro Ramirez

• https://x.com/ndea

• https://x.com/bryanlanders

• https://ndea.com

Moshe Vardi, Professor at Rice University and one of the most influential figures in logic, verification, and theoretical computer science, discusses his paper “Symbolic LTLf Synthesis”.

This conversation explores how Linear Temporal Logic over finite traces (LTLf) provides a more practical and scalable foundation for program and controller synthesis, especially compared to classical approaches based on infinite executions. The discussion traces the deep theoretical roots of synthesis in logic, automata, and games, while connecting them to modern challenges in AI, planning, and autonomy.

Moshe shares the origin story of the paper, which grew out of collaborations with AI researchers and a visiting student, explains why “simpler” finite-trace reasoning turned out to be a strength rather than a limitation, and reflects on how LTLf has helped shift the direction of research and tooling in temporal synthesis.

In This Episode -

• The history of program synthesis

• Why infinite traces dominate classical LTL

• Linear Temporal Logic over finite traces (LTLf)

• Automata theory in both verification and synthesis

• Implications for reactive systems, autonomy, and agent design

• The future of symbolic synthesis + neurosymbolic AI research

About the Paper -

“Symbolic LTLf Synthesis”

Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi

IJCAI, 2017

This paper introduces an automata-based approach to synthesizing controllers from LTLf specifications, leveraging the finite-trace setting to achieve simpler constructions and improved scalability. It demonstrates how symbolic techniques can make temporal synthesis more practical for AI and planning-oriented applications.

https://arxiv.org/abs/1705.08426

About the Guest -

Moshe Vardi is University Professor at Rice University, where his research spans logic, automata theory, formal verification, and the foundations of computer science. He has played a central role in bringing temporal logic and model checking from theory into industrial practice, while also contributing to broader discussions about AI and society.

https://www.cs.rice.edu/~vardi/

Credits -

• Host & Music: Bryan Landers, Technical Staff, Ndea

• Co-Host: Mark Santolucito, Assistant Professor, Barnard College/Columbia U

• Editor: Alejandro Ramirez

• https://x.com/ndea

• https://x.com/bryanlanders

• https://ndea.com

This is a special episode of the Abstract Synthesis podcast featuring a series of live interviews from NeurIPS 2025 in sunny San Diego, California.

Rather than centering on a single paper, this episode captures a snapshot of the current research landscape at the Neural Information Processing Systems annual conference, highlighting how program synthesis and symbolic reasoning are increasingly intersecting with vision, reinforcement learning, world models, and scientific discovery.

The conversations collectively illustrate why these ideas are resurfacing as key tools for efficiency, interpretability, and generalization.

In This Episode -

• Visual concept induction using program synthesis combined with vision-language models

• Program synthesis as a tool for scientific discovery and interpretability in quantum computing

• Symbolic world modeling and efficiency-driven learning in reinforcement learning environments

• Composed program induction on structured domains such as the Rubik’s cube• Program synthesis as a lens for understanding brain, behavior, and neural representations

• Interpretability perspectives framing neural network training as an implicit form of program synthesis

Guests & Papers Mentioned -Clément Bonnet / Technical Staff, Ndeahttps://x.com/ClementBonnet16https://arxiv.org/abs/2411.08706Antonia Wüst / PhD Student, TU Darmstadthttps://ml-research.github.io/people/awuest/index.htmlhttps://arxiv.org/abs/2511.18964Leopoldo Sarra / Senior AI Research Scientist, Axiomatic_AIhttps://leopoldo.sarra.eu/https://arxiv.org/abs/2411.00230Wasu Top Piriyakulkij / PhD Student, Cornell Universityhttps://www.cs.cornell.edu/~wp237/https://topwasu.github.io/poe-worldJumyung Park / Student, Gwangju Institute of Science and Technology (GIST)https://jumyung-park.vercel.app/https://intrig.vercel.app/research/composed-program-induction-with-latent-program-latticeColin “Coco” Conwell / Research Scientist, MIThttps://colinconwell.com/https://openreview.net/forum?id=nuZBUyzBs0Chris Hamblin / Research Scientist, After Thoughthttps://chrishamblin.xyz/

Other Mentions -DreamCoder, Kevin Ellis et al.https://arxiv.org/abs/2006.08381ARC-AGI Benchmarkhttps://arcprize.org/arc-agiCredits -

• Host & Music: Bryan Landers, Technical Staff, Ndea• Camera & Audio: Rowan Rintala• Editor: Alejandro Ramirez• https://x.com/ndea• https://x.com/bryanlanders• https://ndea.com

Leading formal methods researcher Kedar Namjoshi (Distinguished Member of Technical Staff, Nokia Bell Labs) discusses his extended abstract “Program Synthesis And Non-monotonic Reasoning”.

This conversation explores why standard logical specifications, while well-suited for verification, can lead synthesis procedures to produce programs with unnecessary or undesirable actions, and how introducing minimality and preferences fundamentally changes the reasoning model required for synthesis.

Kedar shares the research motivations behind the work, tracing its roots to non-monotonic logic and his experience synthesizing real-world control programs, and reflects on how practical scenarios like IoT device coordination expose deep gaps between formal specifications and human expectations of reasonable system behavior.

In This Episode -

• Why logical specifications are ideal for verification but problematic for synthesis

• The notion of superfluous actions in synthesized programs

• An IoT case study - door locks and refrigerators

• How preference and minimality introduce non-monotonicity into synthesis

• Compact strategies and minimizing behaviors in reactive systems

• Checking minimality versus performing synthesis• Scaling synthesis to multi-agent systems (i.e., robotics)

• Automaton-based approach limitations and LLM-based synthesis

References -

• https://synt2025.github.io/

• https://link.springer.com/chapter/10.1007/978-3-030-99524-9_3

• https://en.wikipedia.org/wiki/Alonzo_Church

• https://dl.acm.org/doi/10.1145/3689624

• https://www.youtube.com/watch?v=H53JDxt_cbI

• https://www.youtube.com/watch?v=s6GKwRIQRf0

About the Paper -

“Program Synthesis And Non-monotonic Reasoning (Extended Abstract)”

Kedar S. NamjoshiPresented at SYNT 2025 Workshop

The paper shows that enforcing minimality in program synthesis breaks monotonic reasoning assumptions, reframing the avoidance of unnecessary actions as a problem of preference-based, non-monotonic reasoning.

https://drive.google.com/file/d/1btOZ52OLD_RuvYc8KIkEk0rLDBn0lBvR/view?usp=sharing

About the Guest -

Kedar Namjoshi is a Distinguished Member of Technical Staff at Nokia Bell Labs. His research spans formal methods, program synthesis, verification, distributed systems, and the design of correct-by-construction systems, with an emphasis on bridging theory and real-world applications.

https://kedar-namjoshi.github.io

Credits -

• Host & Music: Bryan Landers, Technical Staff, Ndea

• Editor: Alejandro Ramirez

• https://x.com/ndea

• https://x.com/bryanlanders

• https://ndea.com

Leading program synthesis researcher Mark Santolucito (Assistant Professor, Barnard College, Columbia University) discusses his paper "Grammar Filtering for Syntax-Guided Synthesis".

This conversation explores how machine learning can be used to shrink the search space of syntax-guided synthesis (SyGuS) problems, dramatically speeding up synthesis without sacrificing the strong correctness guarantees of formal methods.

Mark shares the unexpected origin story of the paper, which began at a hackathon in Bermuda, explains the core ideas behind grammar filtering, and reflects on the broader role of neurosymbolic approaches in modern program synthesis.

In This Episode -

• What program synthesis is and why it matters

• Intro to syntax-guided synthesis (SyGuS)

• Why grammar size dominates synthesis runtime

• How machine learning can safely prune grammars before synthesis

• Predicting both criticality and runtime impact of grammar terminals

• Combining neural guidance with SMT-based synthesis solvers

• Results from SyGuS benchmarks (including ~50% runtime improvements)

• Reflections on the future of neurosymbolic program synthesis

About the Paper -

"Grammar Filtering for Syntax-Guided Synthesis"

Kairo Morton, William Hallahan, Elven Shum, Ruzica Piskac, Mark Santolucito

Published at AAAI 2020

The paper introduces a machine-learning–based technique for identifying and removing low-utility grammar terminals in SyGuS problems, significantly accelerating synthesis while maintaining correctness guarantees.

https://arxiv.org/abs/2002.02884

About the Guest -

Mark Santolucito is an Assistant Professor of Computer Science at Barnard College, Columbia University, where he develops novel program synthesis and analysis techniques to help programmers interact with code more effectively with a focus on Temporal Logic.

https://www.marksantolucito.com

Credits -

• Host & Music: Bryan Landers, Technical Staff, Ndea

• Editor: Alejandro Ramirez

• https://x.com/ndea

• https://ndea.com

• https://x.com/bryanlanders

Welcome to Abstract Synthesis - a podcast where we share the stories behind interesting academic papers in the world of program synthesis.

Brought to you by AGI research lab Ndea.

Subscribe wherever you get your podcasts to stay tuned for in-depth, technical interviews with leaders in the space of symbolic AI.

https://ndea.com