# Anti-unification and Generalization: A Survey

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 99 references that are in the map.
- First posted on arXiv 1 Feb 2023.

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

- [Learning programs by learning from failures](https://mlsanity.com/paper/2005.02259/) (2020)
- [Top-Down Synthesis for Library Learning](https://mlsanity.com/paper/2211.16605/) (2022)
- [Inductive logic programming at 30](https://mlsanity.com/paper/2102.10556/) (2021)
- [Getafix: Learning to Fix Bugs Automatically](https://mlsanity.com/paper/1902.06111/) (2019)
- [babble: Learning Better Abstractions with E-Graphs and Anti-Unification](https://mlsanity.com/paper/2212.04596/) (2022)
- [Learning Higher-Order Programs without Meta-Interpretive Learning](https://mlsanity.com/paper/2112.14603/) (2021)
- [Learning Symbolic Rules for Reasoning in Quasi-Natural Language](https://mlsanity.com/paper/2111.12038/) (2021)
- [Learning Quick Fixes from Code Repositories](https://mlsanity.com/paper/1803.03806/) (2018)
- [Overwatch: Learning Patterns in Code Edit Sequences](https://mlsanity.com/paper/2207.12456/) (2022)
- [WebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration](https://mlsanity.com/paper/2203.09993/) (2022)
- [Generalisation Through Negation and Predicate Invention](https://mlsanity.com/paper/2301.07629/) (2023)
- [E-Generalization Using Grammars](https://mlsanity.com/paper/1403.8118/) (2014)
- [Theory Exploration Powered By Deductive Synthesis](https://mlsanity.com/paper/2009.04826/) (2020)
- [Analogy-Making as a Core Primitive in the Software Engineering Toolbox](https://mlsanity.com/paper/2009.06592/) (2020)
- [Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification](https://mlsanity.com/paper/2110.11700/) (2021)
- [One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus](https://mlsanity.com/paper/2207.08918/) (2022)

## Built on by (most cited first, 7 of 7)

- [Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis](https://mlsanity.com/paper/2307.09564/) (2023)
- [Generalization-baed similarity](https://mlsanity.com/paper/2302.10096/) (2023)
- [Library learning with e-graphs on jazz harmony](https://mlsanity.com/paper/2605.04622/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [Bilingual analogical proportions via hedges](https://mlsanity.com/paper/2305.05614/) (2023)
- [Algebraic anti-unification](https://mlsanity.com/paper/2407.15510/) (2024)
- [LeanPolish: Verified Supervision for Lean Proof Compression](https://mlsanity.com/paper/2609.38384/) (2026)

## Abstract (arXiv)

Anti-unification (AU) is a fundamental operation for generalization computation used for inductive inference. It is the dual operation to unification, an operation at the foundation of automated theorem proving. Interest in AU from the AI and related communities is growing, but without a systematic study of the concept nor surveys of existing work, investigations often resort to developing application-specific methods that existing approaches may cover. We provide the first survey of AU research and its applications and a general framework for categorizing existing and future developments.