Си́нтез програ́мм, процесс автоматического или интерактивного построения программы по формализованному описанию постановки задачи (спецификации программы). Подходы к синтезу программ различаются формой спецификации, способом задания пространства поиска (семейства программ, среди которых ищется решение) и методом поиска.

Для описания постановки задачи в синтезе программ используются:

• логические спецификации, определяющие соотношения между входными и выходными данными (например, с помощью пред- и постусловий);

• примеры, задающие выходные данные или трассы исполнения для выборочных входных данных;

• эталонные программы (модели), реализующие требуемую функциональность, но не удовлетворяющие некоторым другим характеристикам (уровню абстракции, эффективности и др.).

Соответственно, различают три основных подхода к синтезу программ:

• дедуктивный (логический) подход, где построение программы базируется на конструктивном доказательстве теоремы существования решения;

• индуктивный подход, в котором программа строится по примерам входных и выходных данных;

• трансформационный подход, где результирующая программа получается путём эквивалентных преобразований (трансляции) заданной эталонной программы.

Появление дедуктивных методов синтеза программ (в том числе классического метода Манны – Уолдингера) связано с развитием конструктивной математики и методов автоматического доказательства теорем. Применимость дедуктивных методов ограничена вычислительной сложностью процедур поиска логического вывода и требованием полноты спецификации (описание постановки задачи может быть сопоставимым по размеру с синтезируемой программой).

К дедуктивному синтезу программ примыкают две парадигмы: доказательное программирование, в рамках которого разработка программы сопровождается доказательством её корректности (соответствия спецификации), и логическое программирование, в рамках которого программа представляется логической формулой (в узком понимании – системой хорновских дизъюнктов), а её исполнение есть логический вывод (строящийся, например, с помощью SLD-резолюции).

Промышленно применимые методы синтеза программ, как правило, реализуют индуктивный синтез, управляемый контрпримерами (англ. CounterExample-Guided Inductive Synthesis – CEGIS) (Solar-Lezama. 2008). Это итерационный процесс с чередованием этапов поиска решения и верификации: решатель на основе упрощённой спецификации строит программу-кандидат; верификатор (оракул) проверяет её соответствие исходной спецификации. При несоответствии генерируется контрпример (пара вход-выход, реализуемая программой, но не допустимая спецификацией, или – в конструктивном варианте – описываемая спецификацией, но нереализуемая в программе); контрпример передается решателю для уточнения поиска на следующей итерации.

Для построения программ-кандидатов используются различные техники: перебор, дедукция, разрешение ограничений, стохастический поиск (машинное обучение, генетическое программирование и тому подобное) и др. Проверка соответствия программы спецификации выполняется SAT/SMT-решателями. Чтобы сузить пространство поиска, применяются шаблоны (скелетоны), ограничивающие структуру программы и используемые в ней конструкции (операторы).

Последние достижения в области синтеза программ связаны с синтаксически управляемым синтезом (англ. Syntax-Guided Synthesis – SyGuS) (Syntax-Guided Synthesis. 2013). Так называется способ постановки задачи синтеза программ, в рамках которого помимо спецификации программы (семантических ограничений) задаётся контекстно-свободная грамматика, используемая для порождения текста программы (синтаксические ограничения). Вокруг этого направления сформировалось активное научно-исследовательское сообщество, в котором ведутся работы по стандартизации формата представления задач синтеза программ, разработке тестовых примеров и организации соревнований инструментов синтеза программ.

Современные методы синтеза программ позволяют строить достаточно крупные программные фрагменты, но по-прежнему редко используются в промышленных проектах. Синтез программ находит применение в таких областях, как извлечение и структуризация данных (англ. Data Wrangling), исправление ошибок в программах (англ. Code Repair), генерация рекомендаций по продолжению кода (англ. Code Completion) и др.