Saturation-Guided Inductive Synthesis (Invited Talk)

Abstract

Proof by induction is common-place in mathematics [Josef Urban and Geoff Sutcliffe, 2010; Martin Desharnais et al., 2022], formal verification [Raven Beutner and Bernd Finkbeiner, 2024; Wolfgang Ahrendt et al., 2000; Pamina Georgiou et al., 2022], cybersecurity [Simon Jeanteur et al., 2024; Evan Laufer et al., 2024], and many more areas. This talk overviews recent progress in automating inductive reasoning in quantified logic, with applications to code synthesis. Key to our work is saturation-based first-order theorem proving [Laura Kovács and Andrei Voronkov, 2013], using variants of the superposition calculus [Robert Nieuwenhuis and Albert Rubio, 2001]. We show that induction and synthesis are better together in saturation, allowing us not only to prove quantified properties F, but also generate a functional implementation of F during proof search. We showcase our results using the first-order theorem prover Vampire [Filip Bártek et al., 2025], a completely automatic push-button theorem prover for first-order logic with theories, including arithmetic, inductively defined datatypes, induction, and higher-order logic. 

We structure our talk within three inter-connected parts.

First, we overview the main ingredients behind saturation provers [Filip Bártek et al., 2025; Stephan Schulz et al., 2019; Christoph Weidenbach et al., 2009] using superposition. Such provers work by negating an input conjecture F, transforming ¬ F into a clausal normal form, and using superposition inferences to derive new clauses from existing ones until a contradiction is reached; when a contradiction is derived, validity of F is established. Many years of development in saturation-based theorem proving have gone into making this process as efficient as possible, while deriving new clauses only when needed in order to tame growth of the search space. Doing so, highly-efficient superposition calculi parametrized by so-called clause selection functions have been proposed, in order to make as few inferences between clauses as possible. Redundancy elimination techniques further prune the search space. 

Next, we show how to formalize applications of induction in the saturation process [Márton Hajdú et al., 2022], without bringing drastic changes into the overall framework of first-order proving. A natural choice for implementing induction would be by reducing goals to subgoals, in particular by proving a base case and an inductive step case of a valid induction principle. For example, a goal ∀ x. F(x) over natural numbers x can be proven using structural induction: we prove F[0] (base case) and ∀ x. F(x) ⇒ F(x+1) (step case). However, saturation theorem proving is not about reducing goals to subgoals: in principle, each clause in the search space can be chosen during any step of saturation. We therefore automate induction in saturation as follows. When a clause F(x) is chosen and inductive reasoning over F should be applied (for example, because F uses inductively defined data types x, such as natural numbers), we combine the application of a valid induction schema over F(x) with resolution. Put it simply, induction and resolution are combined in one step of saturation, allowing us to use parts of F(x) as subgoals of F(x). Interestingly with this approach is that clauses generated during saturation may be stronger than the induction schema and, most importantly, are friendly to saturation provers: they are mostly quantifier-free Horn clauses and their (at most one) positive equality cannot be used in many inferences during saturation. Thus, applying many induction inferences during proof search would hardly affect the performance of a saturation prover. Figure 1 lists a property over natural numbers: every natural number x is the half of another natural number y. Proving this property in saturation, and in particular using Vampire, can be achieved by (structural) induction over x. 
Finally, we extend saturation proof search with code synthesis [Petra Hozzová et al., 2024]. While proving formula F, we track the constructive parts of the proof of F using so-called answer literals [Cordell Green, 1969]. We use these parts to synthesize a program satisfying F and use the applications of induction in saturation to construct recursive programs satisfying F. In a nutshell, the base case and inductive case steps of induction in saturation express how to construct the desired program for the next recursive step using the program for the previous recursive step; we capture this information via answer literals. When we apply induction in saturation, we introduce a special term into the answer literal and record the program corresponding to the induction step. As we prove induction steps, we capture their corresponding programs in the answer literal. Finally, we convert the special tracker terms from the answer literals into recursive functions, and obtain a program satisfying property F. For example, from the proof of property of Figure 1, our approach implemented in Vampire infers the following functional implementation of a recursive function r, while using only the signature of Figure 1: 

𝗋(0) & :=  0 
𝗋(s(x)) & :=  s(s(𝗋(x)))

The above inferred function r satisfies the property of Figure 1 and, for each input natural number x, computes a natural number 𝗋(x) such that x is half of 𝗋(x).

In summary, induction and synthesis are better together in saturation-based theorem proving using the superposition calculus. Soundness and practical use of our work has been addressed and experimented using the Vampire theorem prover, both in the case of automating induction [Márton Hajdú et al., 2022; Márton Hajdú et al., 2024] and program synthesis [Petra Hozzová et al., 2023; Petra Hozzová et al., 2024]. Interesting questions regarding completeness arise: if a program satisfying a given property exists, can we derive it from saturation-based proof search? Our recent results [Hajdu et al., 2026] answer this question for recursion-free program using additional assumptions of realizability. A natural direction for future work is to identify realizability assumptions for recursive program synthesis and induction.