A carregar...
Publicação
Program Synthesis with Refinement Typed Genetic Programming
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 3.56 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
This dissertation presents the design and evaluation of a framework for Refinement-Typed Genetic Programming (RTGP). The framework combines refinement types with genetic programming, enabling the automatic generation of programs that are not only syntactically valid but also semantically consistent with type constraints. The work addresses a common limitation of search-based synthesis systems, where a significant portion of computational effort is spent generating invalid or incoherent candidates, leading to inefficient exploration of the search space. By incorporating refinement types, RTGP restricts the search space in a principled manner while preserving expressiveness. The approach was implemented by extending the ÆON declarative synthesis language, a programming language that integrates a built-in synthesizer for program synthesis problems, and by integrating it with the GENETICENGINE framework. The resulting architecture introduces dynamic grammar generation, refinement validation, and mechanisms for extracting fitness information. The experimental evaluation was conducted in two parts. First, 22 problems from the Program Synthesis Benchmark Suite 2 were used to assess the behavior of the base ÆON synthesizer. The results show that simpler problems involving at most two primitive types produced a higher number of valid programs, whereas problems involving multiple primitive or composite types resulted in significantly fewer valid solutions. In this context, invalid programs correspond to candidates that, although syntactically well-formed and well-typed, produce runtime errors or fail to satisfy the intended semantic behavior. RTGP itself was evaluated in a procedural content generation case study based on Super Mario. In this scenario, grammars with refinement types, corresponding to our RTGP implementation, produced exclusively valid individuals, whereas grammars without refinements generated only invalid candidates. Overall, the results demonstrate that grammars with refinement types effectively constrain the evolutionary search process, significantly increasing the proportion of valid programs while reducing semantically incorrect candidates.
Descrição
Tese de mestrado, Engenharia Informática, 2026, Universidade de Lisboa, Faculdade de Ciências
Palavras-chave
Program Synthesis Genetic Programming Refinement Types Refinement-Typed Genetic Programming