Síntese de Programas

O que é síntese de programas (program synthesis)?

Síntese de programas é a tarefa de construir automaticamente um programa que satisfaça uma especificação (specification) dada. A especificação pode ser formal (por exemplo, restrições lógicas), baseada em exemplos (pares entrada–saída) ou informal (linguagem natural). O resultado sintetizado normalmente é um programa executável em uma linguagem de propósito geral (Python, C, SQL) ou, mais frequentemente, em uma linguagem específica de domínio (domain-specific language, DSL), projetada para tornar a busca e a verificação tratáveis.

A síntese de programas fica na interseção de:

  • Busca e restrições (próximo de Satisfação de Restrições (Constraint Satisfaction) e da resolução SAT/SMT (SAT/SMT solving))
  • Aprendizado a partir de exemplos (inferência indutiva (inductive inference), generalização e compromissos viés/variância (bias/variance tradeoffs))
  • Métodos formais (formal methods) (lógicas de programas, tipos e verificação)
  • Aprendizado de máquina (machine learning) (modelos neurais (neural models) que propõem código, frequentemente verificados ou reparados com métodos simbólicos)

Um modelo mental útil é:

Encontre um programa (P) tal que (P \models \text{Spec}), otimizando um custo (simplicidade, tempo de execução, tamanho) e, idealmente, generalizando além das restrições/exemplos observados.

Por que isso importa

A síntese de programas é atraente porque muitas tarefas de programação são subespecificadas por humanos, mas podem ser descritas por:

  • alguns exemplos (“transforme estas strings assim”),
  • um invariante (“este loop deve preservar a ordenação”),
  • uma intenção em linguagem natural (“parsear um CSV e agrupar pela coluna X”).

Isso torna a síntese valiosa para:

  • Produtividade de desenvolvedores: geração de código, refatoração, boilerplate
  • Programação por usuários finais: planilhas, preparação de dados, macros
  • Confiabilidade: geração de código com provas/restrições
  • Segurança e safety: imposição de políticas, prevenção de comportamentos inseguros via restrições

Dentro da IA clássica/simbólica, a síntese de programas é um exemplo canônico de uso de estrutura explícita — gramáticas, lógica e busca — para produzir artefatos corretos, conectando-se à Representação do Conhecimento (Knowledge Representation) e (em alguns contextos) ao Planejamento (Simbólico) (Planning (Symbolic)).

Formas comuns de especificações

Diferentes métodos de síntese dependem fortemente do tipo de especificação.

1) Exemplos entrada–saída (Programação por Exemplos (Programming by Example, PBE))

Você fornece pares ((x_i, y_i)); o sintetizador encontra um programa (P) tal que (P(x_i) = y_i) para todos os exemplos.

  • Ponto forte: natural para usuários; não exige lógica formal
  • Risco: sobreajuste (overfitting) (muitos programas podem coincidir com um conjunto finito de exemplos)

Exemplo (transformação de string)
Dado:

  • "john_smith" -> "John Smith"
  • "jane_doe" -> "Jane Doe"

Um sintetizador pode descobrir: dividir em _, capitalizar tokens, juntar com espaço.

2) Restrições lógicas (dedutivo/baseado em restrições)

As especificações são expressas como fórmulas lógicas, pré/pós-condições, invariantes ou restrições relacionais. Isso viabiliza garantias formais de corretude.

Exemplo (função de vetor de bits)
Sintetize f(x) tal que, para todo x de 32 bits: f(x) = x & (x - 1) limpa o bit 1 menos significativo, e satisfaz uma propriedade declarada sobre redução de popcount.

3) Restrições guiadas por sintaxe (síntese guiada por sintaxe (syntax-guided synthesis, SyGuS))

A síntese guiada por sintaxe combina ambos: você fornece uma especificação lógica e restringe o espaço de soluções via uma gramática (uma linguagem específica de domínio).

  • Ponto forte: reduz ambiguidades e o espaço de busca
  • Amplamente usada em benchmarks e competições (SyGuS-Comp)

Miniesboço ao estilo SyGuS (ilustrativo)

; Find an expression over x,y using +,-,ite,<=
(synth-fun max2 ((x Int) (y Int)) Int
  ((Start Int (x y
               (+ Start Start)
               (- Start Start)
               (ite (<= Start Start) Start Start)))))

(constraint (and (>= (max2 x y) x)
                 (>= (max2 x y) y)
                 (or (= (max2 x y) x) (= (max2 x y) y))))
(check-synth)

4) Programas parciais / esboços

Um humano fornece um programa com lacunas (desconhecidos). O sintetizador preenche essas lacunas.

  • Conhecido como esboçamento (sketching) (por exemplo, o sistema Sketch)
  • Ótimo para combinar intuição humana com automação

Exemplo: “O algoritmo é um loop sobre o array; não tenho certeza sobre a condição e a atualização.”

5) Especificações em linguagem natural (natural-language specifications)

Linguagem natural é flexível, mas ambígua. Sistemas modernos normalmente:

  1. usam um modelo de linguagem grande (large language model, LLM) para propor código,
  2. validam-no contra testes/restrições,
  3. reparam ou fazem nova amostragem se falhar.

Isso frequentemente é neuro-simbólico (neuro-symbolic): proposta neural + checagem simbólica.

Abordagens centrais

Métodos de síntese de programas variam em como exploram o espaço de programas e como impõem corretude.

Abordagem A: Busca e resolução de restrições (síntese simbólica)

Essa família trata a síntese como um problema de busca estruturada: explorar programas candidatos até que um satisfaça a especificação. Em síntese simbólica (symbolic synthesis), a exploração e a checagem são conduzidas por representações explícitas (gramáticas, restrições, lógica).

Busca enumerativa (enumerative search) (frequentemente sobre uma linguagem específica de domínio)

O sintetizador enumera programas por tamanho/custo crescente e os verifica.

Ideias-chave:

  • Linguagem específica de domínio + gramática para definir o espaço de hipóteses
  • Modelo de custo (cost model) (tamanho, profundidade, operações)
  • Poda (pruning) usando avaliação parcial (partial evaluation), classes de equivalência (equivalence classes) ou restrições

Exemplo de brinquedo: síntese enumerativa para PBE

# DSL: expressions built from input x and ops: +1, -1, *2
ops = [lambda e: e + 1, lambda e: e - 1, lambda e: e * 2]

def synthesize(examples, max_depth=6):
    # each candidate is a function from int->int; in real systems, store ASTs
    candidates = [lambda x: x]
    for depth in range(max_depth):
        new = []
        for c in candidates:
            for op in ops:
                f = lambda x, c=c, op=op: op(c(x))
                if all(f(x) == y for x, y in examples):
                    return f  # found a program
                new.append(f)
        candidates = new
    return None

f = synthesize([(1, 4), (2, 6)])  # maybe f(x)=2x+2

Sintetizadores reais não enumeram lambdas “cruas”; eles enumeram e simplificam árvores de sintaxe abstrata (abstract syntax tree, AST), usam memoização (memoization) e fazem poda agressiva de programas equivalentes.

Síntese baseada em restrições (constraint-based synthesis) (SMT)

Em vez de enumerar programas explicitamente, codifique o programa desconhecido (ou seus parâmetros) como variáveis desconhecidas (unknown variables) e gere restrições tais que qualquer atribuição satisfatória corresponda a um programa correto.

Codificações comuns:

  • Síntese baseada em template (template-based synthesis): escolher uma forma fixa de programa com constantes/escolhas desconhecidas
  • Síntese de vetores de bits (bit-vector) / circuitos aritméticos
  • Programas de estados finitos (finite-state programs)

Isso pode ser extremamente eficaz quando:

  • o programa pode ser expresso com tamanho limitado,
  • a lógica é suportada de forma eficiente por um solucionador SMT.

CEGIS: Síntese Indutiva Guiada por Contraexemplos (Counterexample-Guided Inductive Synthesis, CEGIS)

Uma técnica fundamental é CEGIS:

  1. Propor um programa candidato que funciona em um conjunto finito de entradas de teste.
  2. Usar um verificador para checá-lo contra a especificação completa.
  3. Se falhar, o verificador retorna uma entrada de contraexemplo (counterexample).
  4. Adicionar esse contraexemplo ao conjunto de testes e repetir.

CEGIS conecta suposição indutiva e checagem dedutiva — muitas vezes fornecendo desempenho prático e garantias fortes de corretude quando o verificador é sólido.

Abordagem B: Síntese indutiva de programas (inductive program synthesis) (aprendizado a partir de exemplos)

A síntese indutiva enfatiza a generalização a partir de dados. Isso inclui sistemas de PBE e algoritmos que mantêm um conjunto de programas consistentes com os exemplos.

Espaços de versões (version spaces) e gestão de ambiguidades

Dado um conjunto de exemplos, pode haver muitos programas consistentes. Os sistemas lidam com isso por meio de:

  • Viés (bias): restringir a uma linguagem específica de domínio que combine com o domínio
  • Ranqueamento (ranking): preferir programas mais simples (navalha de Occam) ou programas que correspondam a padrões comuns
  • Síntese interativa (interactive synthesis): pedir ao usuário exemplos adicionais para desambiguar

Um padrão clássico em ferramentas de PBE (por exemplo, sistemas no estilo “Flash Fill” de planilhas) é:

  • gerar muitas transformações candidatas consistentes com exemplos,
  • ranqueá-las,
  • mostrar o melhor resultado,
  • solicitar mais exemplos se necessário.

Síntese guiada por tipos e gramáticas (type- and grammar-directed synthesis)

Tipos podem reduzir dramaticamente o espaço de busca:

  • gerar apenas programas bem tipados (well-typed),
  • usar tipos para guiar composição,
  • aproveitar polimorfismo (polymorphism) e tipos algébricos de dados (algebraic data types).

Isso se conecta a como sistemas simbólicos representam e restringem hipóteses — outro vínculo com Representação do Conhecimento.

Abordagem C: Síntese neural e neuro-simbólica (neural and neuro-symbolic synthesis)

Métodos neurais tratam a síntese como um problema de predição (prediction): mapear uma especificação (exemplos, texto, código parcial) para um programa.

Geração neural de código (neural code generation) (sequência-para-sequência (seq2seq), Transformers, LLMs)

Sistemas modernos frequentemente usam modelos de Arquitetura Transformer (Transformer Architecture) para propor tokens de código ou ASTs.

Pontos fortes:

  • lida bem com linguagem natural,
  • aproveita pré-treinamento em grande escala sobre código,
  • amostragem rápida.

Pontos fracos:

  • sem garantia inerente de corretude,
  • dificuldade com tarefas fora da distribuição (out-of-distribution),
  • pode produzir código plausível, porém errado.

Síntese neuro-simbólica: propor + verificar + reparar

Um padrão prático comum é:

  1. O modelo neural propõe candidatos (busca em feixe (beam search), amostragem (sampling)).
  2. Um verificador simbólico (symbolic checker) executa testes ou verificação formal (formal verification).
  3. Se falhar, reparar via:
    • resolução de restrições (preencher lacunas),
    • loop de CEGIS,
    • nova amostragem guiada por testes,
    • reescrita simbólica (symbolic rewriting).

Essa abordagem híbrida busca combinar:

  • cobertura e priores (priors) neurais (qual código é provável),
  • solidez (soundness) simbólica (qual código é correto).

Um exemplo prático completo: sintetizando uma transformação de preparação de dados

Suponha que um usuário queira normalizar códigos de produto:

Entrada → Saída:

  • "sku-001_blue" → "001 (BLUE)"
  • "sku-120_red" → "120 (RED)"

Um sintetizador PBE típico usaria uma linguagem específica de domínio para strings:

  • Split(s, delim)
  • Select(tokens, i)
  • Upper(s)
  • Replace(s, a, b)
  • Concat(...)
  • RegexExtract(s, pattern, group)

Um programa sintetizado plausível:

  1. Dividir em - para separar "sku" do restante.
  2. Dividir o restante em _ para separar número e cor.
  3. Formatar como num + " (" + UPPER(color) + ")".

Em um pseudocódigo ao estilo de uma linguagem específica de domínio:

t1 = Split(x, "-")[1]          # "001_blue"
t2 = Split(t1, "_")[0]         # "001"
t3 = Split(t1, "_")[1]         # "blue"
y  = Concat(t2, " (", Upper(t3), ")")

A principal escolha de projeto é a linguagem específica de domínio: ela codifica conhecimento do domínio (“tarefas com strings geralmente envolvem split/concat/regex”), tornando a síntese viável e os resultados interpretáveis.

Fundamentos teóricos (o que torna a síntese difícil)

Explosão do espaço de busca

Mesmo pequenas linguagens específicas de domínio produzem espaços enormes de programas conforme a profundidade aumenta. A síntese costuma ser exponencial no tamanho do programa sem poda forte ou restrições.

Subespecificação (underspecification) e identificabilidade (identifiability)

Com exemplos finitos, muitos programas podem satisfazer a especificação. O sintetizador precisa decidir qual é “o certo” — geralmente via:

  • priores de simplicidade (simplicity priors),
  • heurísticas de ranqueamento específicas do domínio,
  • interação adicional com o usuário,
  • especificações mais fortes (restrições, invariantes).

Relação com verificação formal

Verificação pergunta: O programa (P) satisfaz a especificação (S)?
Síntese pergunta: Encontre um (P) que satisfaça (S).

A síntese pode ser vista como “verificação com desconhecidos”, e muitas técnicas de síntese reutilizam mecanismos de verificação (SMT, interpretação abstrata (abstract interpretation), verificação de modelos (model checking)). Esse é um dos principais motivos pelos quais a síntese é frequentemente agrupada com IA simbólica e métodos formais.

Critérios de avaliação e trade-offs

Um bom sistema de síntese não é apenas “capaz de encontrar um programa”. A avaliação prática equilibra vários objetivos:

Corretude

  • Corretude funcional (functional correctness): corresponde a todos os exemplos; ou satisfaz a especificação lógica completa.
  • Solidez (soundness): quando o sistema afirma sucesso, ele é garantidamente correto?
  • Completude (completeness): se existe uma solução na linguagem específica de domínio, ela será encontrada (dado tempo suficiente)?

Sistemas apenas neurais tipicamente trocam solidez por velocidade/cobertura, enquanto métodos baseados em solucionadores podem fornecer garantias fortes sob suposições limitadas.

Generalização

Especialmente em PBE e especificações em linguagem natural, ter sucesso nos exemplos de treino não implica corretude em entradas não vistas.

Mitigações comuns:

  • solicitar exemplos mais diversos,
  • escolher primitivas da linguagem específica de domínio que reduzam sobreajuste,
  • usar contraexemplos (CEGIS) quando possível,
  • geração de testes / teste por fuzzing (fuzzing) para expandir cobertura.

Interpretabilidade e manutenibilidade

Mesmo que dois programas sejam corretos, um pode ser preferível se for:

  • mais curto,
  • usar construções de mais alto nível,
  • alinhar-se à intenção humana (legível, idiomático).

Síntese baseada em linguagem específica de domínio frequentemente produz resultados mais interpretáveis do que circuitos de vetores de bits de baixo nível; a geração neural pode ser legível, mas pode esconder bugs sutis.

Eficiência (tempo e memória)

Sistemas práticos medem:

  • tempo até a primeira solução,
  • taxa de sucesso sob limites de tempo,
  • escalabilidade com o tamanho da especificação e a expressividade da linguagem específica de domínio.

Robustez e segurança

Para sistemas que geram código para ambientes reais:

  • evitar padrões inseguros,
  • respeitar políticas de sandboxing e dependências,
  • garantir comportamento determinístico quando necessário.

Aplicações práticas

Programação por usuários finais e automação

  • Transformações em planilhas (PBE)
  • Parsing de logs e normalização de texto
  • Pipelines de ETL/limpeza de dados

Esses domínios se beneficiam de linguagens específicas de domínio restritas e refinamento interativo.

Ferramentas para desenvolvedores

  • Autocompletar e geração de código em IDEs (frequentemente neural + testes)
  • Sugestões de refatoração (“substituir loop por map/filter”)
  • Auxiliares de migração de API

Reparo de programas (program repair)

Dado um programa com bug e uma suíte de testes/especificação, sintetizar uma correção (patch) que arrume o bug preservando o comportamento pretendido. Isso é intimamente relacionado à síntese com um objetivo de “edição mínima (minimal edit)”.

Métodos formais e componentes verificados

  • Síntese de invariantes de loop
  • Geração de controladores que satisfaçam restrições de safety
  • Síntese de protocolos ou circuitos a partir de especificações em lógica temporal

Aqui, métodos simbólicos (SMT, verificação de modelos) dominam devido à necessidade de garantias fortes.

Robótica e cenários semelhantes a planejamento

Quando o “programa” é uma política (policy) ou controlador com estrutura discreta, a síntese se assemelha ao planejamento simbólico e à resolução de restrições (ver Planejamento (Simbólico)), às vezes combinados com aprendizado.

Escolhas de projeto que afetam fortemente o sucesso

Escolher a linguagem específica de domínio certa

Uma linguagem específica de domínio deve ser:

  • expressiva o suficiente para cobrir tarefas reais,
  • restrita o suficiente para manter a busca tratável,
  • alinhada com a forma como usuários pensam sobre o problema.

Em muitos sistemas bem-sucedidos, a linguagem específica de domínio é o “ingrediente secreto”.

Ranqueamento e funções de custo

Quando muitos programas satisfazem a especificação, o ranqueamento determina a usabilidade. Vieses comuns:

  • menor profundidade/tamanho de AST,
  • menos constantes,
  • menos condicionais,
  • primitivas mais “de biblioteca” (operações de alto nível).

Interação

Como especificações podem ser ambíguas, síntese interativa é comum:

  • o sistema pede outro exemplo,
  • ou faz uma pergunta de esclarecimento (“Sublinhados devem sempre virar espaços?”).

Isso transforma a síntese em um processo de aprendizado com humano no loop, ecoando temas de Sistemas Especialistas (Expert Systems): elicitação de conhecimento e desambiguação continuam sendo desafios centrais.

Tendências atuais (anos 2020)

  • Síntese guiada por LLM (LLM-driven synthesis): linguagem natural para código agora é amplamente implantada, mas corretude é o gargalo.
  • Geração ciente de verificação (verification-aware generation): aumento do uso de testes unitários (unit tests), verificações de propriedades (property checks) e validadores simbólicos (symbolic validators) para filtrar/reparar saídas de LLM.
  • Agentes ampliados por ferramentas (tool-augmented agents): sistemas que iterativamente propõem código, o executam, inspecionam falhas e revisam (uma variante prática, guiada por testes, de CEGIS).
  • Híbridos neuro-simbólicos: integração mais forte de mecanismos neurais de proposta com restrições simbólicas, especialmente em domínios estruturados (SQL, regex, transformações).

Principais limitações e problemas em aberto

  • Ambiguidade da especificação: linguagem natural e pequenos conjuntos de exemplos frequentemente são insuficientes.
  • Escalabilidade: programas grandes continuam difíceis; a maior parte da síntese se destaca em componentes pequenos a médios.
  • Realismo de benchmarks (benchmark realism): alguns datasets enfatizam demais tarefas de linguagens específicas de domínio “de brinquedo”; restrições do mundo real (bibliotecas, efeitos colaterais, desempenho) complicam a síntese.
  • Confiança (trust): usuários precisam de explicações compreensíveis, proveniência (provenance) (“por que este programa?”) e garantias.

Resumo

A síntese de programas busca gerar automaticamente programas que satisfaçam especificações que vão de exemplos entrada–saída a restrições lógicas formais e descrições em linguagem natural. A área abrange:

  • Busca simbólica e resolução de restrições (SMT/SAT, CEGIS, síntese guiada por sintaxe),
  • Síntese indutiva (PBE, espaços de versões, ranqueamento e interação),
  • Métodos neurais e neuro-simbólicos (proposta por LLM + verificação/reparo simbólicos).

Entre abordagens, os principais trade-offs são corretude vs. flexibilidade, generalização vs. sobreajuste e interpretabilidade vs. expressividade. Na prática, os sistemas mais confiáveis acoplam firmemente uma linguagem específica de domínio bem escolhida com checagem forte — frequentemente combinando propostas baseadas em aprendizado com validação simbólica.