# Genetic Algorithm for Program Synthesis

arXiv: https://arxiv.org/abs/2211.11937 · HTML: https://mlsanity.com/paper/2211.11937/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 20 references that are in the map.
- First posted on arXiv 22 Nov 2022.

## Builds on (most cited first, 12 of 12)

- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving](https://mlsanity.com/paper/1703.00426/) (2017)
- [PaMpeR: Proof Method Recommendation System for Isabelle/HOL](https://mlsanity.com/paper/1806.07239/) (2018)
- [A Proof Strategy Language and Proof Script Generation for Isabelle/HOL](https://mlsanity.com/paper/1606.02941/) (2016)
- [Towards Evolutionary Theorem Proving for Isabelle/HOL](https://mlsanity.com/paper/1904.08468/) (2019)
- [Structuring the Synthesis of Heap-Manipulating Programs - Extended Version](https://mlsanity.com/paper/1807.07022/) (2018)
- [LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL](https://mlsanity.com/paper/1906.08084/) (2019)
- [Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)](https://mlsanity.com/paper/2004.10667/) (2020)
- [Faster Smarter Induction in Isabelle/HOL](https://mlsanity.com/paper/2009.09215/) (2020)
- [Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction](https://mlsanity.com/paper/2010.10296/) (2020)

## Abstract (arXiv)

A deductive program synthesis tool takes a specification as input and derives a program that satisfies the specification. The drawback of this approach is that search spaces for such correct programs tend to be enormous, making it difficult to derive correct programs within a realistic timeout. To speed up such program derivation, we improve the search strategy of a deductive program synthesis tool, SuSLik, using evolutionary computation. Our cross-validation shows that the improvement brought by evolutionary computation generalises to unforeseen problems.