# Synteza sterowana gramatyką i solwerami (SyGuS)

EN: **Syntax-guided and solver-based synthesis (SyGuS)** · id `sygus` · aliases: syntax-guided synthesis, SyGuS, synteza sterowana składnią

Path: [AI Atlas](https://aiatlasgraph.com/llms.txt) › [Fundamenty i rozumowanie](https://aiatlasgraph.com/t/foundations.md) › [Synteza programów](https://aiatlasgraph.com/t/programsynthesis.md) › Synteza sterowana gramatyką i solwerami (SyGuS)

## Description

- PL: Synteza funkcji spełniającej formułę w teorii tła (SMT) i jednocześnie wyrażalnej gramatyką; standaryzowana formatem SyGuS-IF i konkursem SyGuS-Comp.
- EN: Synthesising a function satisfying a formula in a background theory (SMT) while expressible in a grammar; standardised by the SyGuS-IF format and SyGuS-Comp.

## In one sentence

- PL: Szukanie programu, który spełnia ściśle zapisany warunek logiczny i zbudowany jest tylko z dozwolonych klocków.
- EN: Searching for a program that meets a precisely written logical condition and uses only permitted building blocks.

## Problem it solves

- PL: W kodzie krytycznym nie wystarczy, że program działa na kilku przykładach; musi działać dla każdego możliwego wejścia.
- EN: In critical code it is not enough for a program to work on a few examples; it must work for every possible input.

## What it does

- PL: Łączy zgadywanie z kontrolą: jeden mechanizm proponuje program, drugi szuka wejścia, na którym zawodzi, i tak aż do skutku.
- EN: Combines guessing with checking: one part proposes a program, another hunts for an input where it fails, until none remains.

## Everyday example

- PL: Narzędzie dla programistów samo wylicza warunek, który musi być prawdziwy w każdym obrocie pętli, żeby udowodnić jej poprawność.
- EN: A developer tool works out by itself a condition that must hold on every loop iteration, to prove the loop correct.

## This concerns you if you…

- PL: piszesz oprogramowanie, które musi być dowodliwie poprawne
- PL: interesuje cię łączenie AI z formalną weryfikacją
- EN: write software that must be provably correct
- EN: are interested in combining AI with formal verification

## Keywords

SyGuS-IF · SyGuS-Comp · CEGIS · cvc5 · EUSolver · Sketch · Rosette · invariant synthesis

## How it works

- PL: Problem SyGuS zadaje specyfikację semantyczną jako formułę logiczną i ograniczenie składniowe jako gramatykę kandydatów. Solwery stosują enumerację z przycinaniem równoważnych wyrażeń, metody oparte na SMT oraz pętlę CEGIS, w której weryfikator zwraca kontrprzykłady, a syntezator poprawia kandydata. Typowe zadania to arytmetyka, wektory bitowe i niezmienniki pętli.
- EN: A SyGuS problem gives a semantic specification as a logical formula and a syntactic constraint as a grammar of candidates. Solvers use enumeration with pruning of equivalent expressions, SMT-based methods and the CEGIS loop, where a verifier returns counterexamples and the synthesiser refines the candidate. Typical tasks are arithmetic, bit-vectors and loop invariants.

## Limits

- PL: Wymaga formalnej specyfikacji, którą trudno napisać poza wąskimi dziedzinami. Skuteczność spada szybko z rozmiarem szukanego wyrażenia, a wynik zależy od starannie dobranej gramatyki.
- EN: Requires a formal specification, which is hard to write outside narrow domains. Effectiveness drops quickly with the size of the target expression, and results depend on a carefully chosen grammar.

## Key terms

- PL: **teoria tła**: Dziedzina matematyczna formuł, np. liczby całkowite lub ciągi bitów.
- PL: **kontrprzykład**: Wejście, na którym proponowany program łamie specyfikację.
- PL: **niezmiennik pętli**: Warunek prawdziwy przed każdym obrotem pętli.
- EN: **background theory**: The mathematical domain of formulas, e.g. integers or bit-vectors.
- EN: **counterexample**: An input on which the proposed program breaks the specification.
- EN: **loop invariant**: A condition true before every loop iteration.

## Know first

- [Solwery SAT i SMT (SAT and SMT solvers)](https://aiatlasgraph.com/t/satsmt.md)

## Sources

- [SyGuS-Comp 2016: Results and Analysis](<https://arxiv.org/abs/1611.07627>) `sygus-comp-2016-results` · by Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama

---

AI Atlas revision 125 (2026-11-01) · HTML: https://aiatlasgraph.com/t/sygus · index: https://aiatlasgraph.com/llms.txt · everything: https://aiatlasgraph.com/llms-full.txt · updated 2026-11-01