Program synthesis is the task of constructing a program that satisfies specified constraints. One popular formulation of program synthesis is example-based synthesis. Here, the synthesizer attempts to find a program in a specified domain that satisfies a set of input-output examples. Enumeration is the most common approach to finding the desired program. However, the exponentially growing search space makes this infeasible. The size of the domain can be largely attributed to its inefficient representation. Often, programs are only syntactically distinguished, meaning programs that behave the same are seen as different. We introduce Context-Sensitive E-Graph Saturation, a novel method that limits the search space to programs that solve at least one of the provided examples. This allows focusing only on programs that behave similarly to the desired one. Crucial is finding contextual equivalences for each example over a generated termset. These equivalences allow generating many solutions for each individual example. A program in the intersection of these programs solves all examples. In experiments on a subset from SyGus SLIA, our method solves the problems that enumeration solves, but not more. These results highlight a trade-off: with a small termset, the discovered equivalences are often too limited to capture the relationships needed to find a universal solution. Conversely, increasing the termset size quickly leads to inefficiency. To address this, we propose a strategy for constructing a more expressive yet small termset, enabling our method to solve a broader range of synthesis problems.

Understanding how local molecular interactions give rise to global cellular outcomes is a central challenge in computational systems biology. Rule-based modeling frameworks such as Kappa provide a way to specify these interactions compactly as rules, which can be simulated to produce causal ``stories'' explaining how a specified event of interest (EOI) arises. However, even small changes in the conditions of a rule can change these causal structures in ways that are difficult to anticipate. This thesis addresses the question: how do modifications to rules affect the causal stories produced by a model? We propose a novel program synthesis framework that automates the generation and exploration of Kappa programs. First, we construct a grammar specialized to a given program's agent signature, extended with constraints to ensure only valid rules are produced. Second, we introduce a rule modification procedure that systematically adds structural contextual conditions to rules while preserving their core transformations. Together, these techniques allow us to enumerate the space of modified programs and retrieve subsets of this space guided by user-defined specifications over the stories. Our experiments show that the constraints reduce the search space by several orders of magnitude, making exhaustive exploration feasible for small models. Using static analysis tools, we reduce the exploration time by 45\%. We demonstrate how different specifications, such as ensuring EOI reachability, can be used to retrieve a subset of modified programs that satisfy them automatically. Together, this work demonstrates the effectiveness of the program synthesis approach in modeling kappa programs and posing questions about their causal structure.

Automated Planning, also known as Artificial Intelligence (AI) planning is a branch of AI focused on automated decision-making and scheduling. A sub-problem within AI Planning is domain-independent planning, where we want to develop methods that are generalisable for solving planning problems in many domains. A popular modelling language for domain-independent planning is PDDL. In PDDL we model our problems as having some start state and some goal state; these states are defined by the truth-values of a set of defined predicates applied to a set of objects with corresponding types. In this work we explore the concept of dynamic macro-actions for PDDL, which are macro-actions whose utility are re-evaluated as we solve more problems, and does not require prior training. We find that dynamic macro-actions are a promising method, showing average improvements in the number of nodes explored in the search space of up to 84\% depending on the domain.

This thesis explores the automated construction of Chemical Reaction Networks (CRNs) from incomplete experimental data, a task traditionally dependent on expert knowledge and manual effort. CRNs model the interactions between chemical species through a network of reactions and are essential in fields such as medicine and chemistry. However, many real-world systems include unobserved or unmeasurable species, making CRN construction challenging. To address this, this thesis frames CRN discovery as a program synthesis problem, using grammars and constraints to define the space of possible CRNs. A modular synthesis pipeline is developed that incrementally builds candidate molecules, reactions, and networks given a problem definition. Experimental results demonstrate that constraints effectively reduce the search space and that the solver is capable of identifying the correct reaction networks. Moreover, a scoring mechanism ranks the expected CRN highly among generated candidates.

Probabilistic programming offers an intuitive and expressive way to define statistical models, rendering it particularly effective in modeling problems where uncertainty plays a crucial role.
As adoption increases and models become more expressive, the challenge of effective inference becomes increasingly pronounced.
Effective inference often requires tailoring algorithms to the structure of the underlying model. While many probabilistic programming systems allow users to implement custom inference strategies via programmable inference, this process remains largely manual and heavily reliant on domain-specific expertise, particularly for sampling-based methods.
This paper investigates the use of Satisfiability Modulo Theories (SMT) to automate the generation of tailored, observation-aware proposals for guiding inference within Metropolis-Hastings in Gen, a probabilistic programming system. By reformulating the search for high-likelihood traces as a constraint optimization problem, this work explores whether SMT-based solutions can improve proposal quality and convergence. Empirical results indicate that SMT-derived traces offer a promising starting point for inference but are less effective as an active search heuristic. These findings suggest a new direction for automated, structure-aware proposal generation in probabilistic programming.

All over the world, people plan their daily activities. These plans include a lot of different tasks and can vary widely in kinds of activities. These plans must account for uncertainties and unknowns in the world. Planning around these uncertainties is difficult and hard to accomplish with traditional means of programming. For this set of problems, probabilistic programming is proposed. Given the Minecraft planner from the Planning Domain Definition Language (PDDL) gym library, is it possible to create Robust plans that incorporate inference without changing the underlying planner? "PDDL is a human-readable format for problems in automated planning that gives a description of the possible states of the world, a description of the set of possible actions, a specific initial state of the world, and a specific set of desired goals." [6] The current approach is using heuristics to find the optimal plan for the problem. In this research paper, an alternative method is proposed; using probabilistic programming and the existing planner to create a simulated world of Minecraft. This model introduces inference without changing the already existing planner.

Scheduling problems are present in many real-world situations, such as construction projects, manufacturing processes, or train timetabling. One common formalization is the Resource Constrained Project Scheduling Problem (RCPSP), where the goal is to find an optimal schedule given limited resources. Traditional algorithms optimize for project duration under deterministic assumptions, which could lead to poor performance under uncertainty. This thesis explores how to create robust schedules, meaning they can withstand uncertainty, for stochastic task durations. Robust schedules minimize delays, measured as the difference between a task's completion time and its deadline. The method proposed uses probabilistic programming as a tool to accomplish this. A robustness distribution over schedules is inferred using importance sampling, and a robust schedule can be selected from that explored distribution. Importantly, this approach presented in this thesis can be applied on top of existing scheduling and simulation algorithms without requiring any knowledge or changes to themselves. Created schedules can also be abstracted, thus do not need to be analyzed or seen. This makes the proposed method general and easy to adopt in practice.

Planning is very important in everyday life, whether it would be creating schedules for planes or plans for manufacturing. These domains contain uncertainties requiring plans that are robust. However, there is a need for an approach which creates robust plans regardless of the domain and without changing its planning agent. Here, a replanning approach is proposed akin to the Metropolis-Hastings algorithm and its performance is compared to the performance of importance sampling. Replanning works by iteratively trying to improve the previously generated plan. The performance is compared by means of the Keys and Doors problem. It is found that replanning performed better than importance sampling in the two analysed problems. Furthermore, changing the parameter, σ, used in the replanning approach showed a significant difference in its corresponding performance. While the replanning approach has only been tested on the Keys and Doors problem, the results show that replanning is a promising approach which could work irrespective of the domain at hand.

Train Unit Shunting is a complex process that directs trains through a shunting yard. In real-world railway operations, disturbances are common, requiring shunting schedules to be robust against uncertainties such as delays. Previous research has proposed algorithms for the Train Unit Shunting Problem (TUSP) and one study attempted to create robust shunting plans by defining a probabilistic model of the uncertainties involved and inferring a distribution of robust solutions for the TUSP. Following this approach, this paper investigates the use of probabilistic programming in increasing robustness of shunting plans using an advanced TUSP solver. This research develops a model for uncertain shunting scenarios, solves these scenarios, and applies importance sampling to infer the posterior distribution, producing a distribution of robust shunting plans instead of a single plan. The paper presents examples demonstrating that it is beneficial to use one of the output robust plans over the plan made for the deterministic scenario, revealing the potential of integrating probabilistic programming techniques into the planning process to improve railway efficiency and reduce delays.

Planning problems are a set of problems in which an objective must be reached by a sequence of actions. Planning problems traditionally do not consider uncertainty, however for most real-world planning problems uncertainty must be considered to create effective plans. The objective of this paper is to use an existing deterministic planning algorithm in order to create robust plans that solve an uncertain version of Sokoban called Uncertain Move Sokoban. To this end a probabilistic programming language, Gen.jl, is used, which enables creating probabilistic models and inferring its parameters using code. A probabilistic model is created in Gen.jl, that generates plans for the problem as well as robustness scores using a simulator embedded in the model. Probabilistic inference techniques are then used to obtain a robust plan for the uncertain problem, namely: importance sampling and Metropolis-Hastings. We find that the technique is able to create robust plans for small to medium-sized problems and that Metropolis-Hastings is the better-performing inference technique.

We consider a subset of simple proving exercises that are part of the Lean 4 tutorials. The exercises consist of a statement, and the task will consist of creating a proof term of the desired type through the use of tactics.
Large Language Models on their own are known to be able to produce syntactically correct pieces of text but are unable to come up with semantically correct pieces of text once very similar solutions are lacking in the dataset it was trained on.
This work reviews the Sequential Monte Carlo with Expectation-Maximization (SMX) algorithm for general reinforcement learning problems, and applies it to theorem proving using LLMs.
This work shows that the SMX algorithm is applicable to tasks where formal verification can be performed on the output, allowing the calculated reward to steer the reasoning process.
We furthermore formally prove a theorem that will be important in showing that the resampling step in SMX is necessary to mitigate sample impoverishment.
The theoretical part of this thesis builds on the theory of the SMX paper by verifying the derivation of the E-step, starting from the Evidence Lower Bound (ELBO). This derivation was missing from the original SMX paper.

Program synthesis is often seen as the holy grail of computer science. A user only needs to provide program specifications and a computer will automatically generate the desired program. This often involves searching for the desired program in the program space, which is like searching for a needle in a haystack. Luckily, there is room for improvement here. Many programs in the program space are redundant and should never be considered. To filter out these redundant programs, we propagated grammar constraints during search using a novel built-in constraint solver. Only programs that satisfy these constraints will be considered as candidates for synthesis. To measure the effectiveness of the solver, we have enumerated several program spaces with and without constraints. Although the amount of filtering largely depends on the concrete grammar and constraints, the results show that constraints can often eliminate $99\%$ of the program space. Accounting for the overhead of propagation, this comes down to a 50-fold improvement in runtime.

Program synthesis aims to automatically generate programs that fulfil user-specified constraints. The field has developed many different techniques to enable program synthesis in various application domains. This work will focus on the enumerative approach, which iteratively explores solutions in the program space from the smallest programs to larger ones. This technique works well on small to medium-sized problems. With the exponentially growing program space performance of the enumerative solver rapidly declines.

This work aims to generalize the divide and conquer approach to combine partial solutions found by an enumerative solver. Firstly by forming the smallest subset that satisfies every example in a problem and then using decision trees to find the final program that satisfies all input-output examples. Our prototype named SubsetDT will be incorporated into the Julia library Herb.jl which provides a flexible environment for testing and developing program synthesis ideas.

This methodology was evaluated on SyGuS competition benchmarks from two different tracks. Results indicate that the use of a decision tree on top of enumeration search improves solver performance by 33% on the string manipulation track and significantly on the bit-vector manipulation track, though both tracks showed some overfitting. The experiments demonstrate that the SubsetDT algorithm can substantially improve enumeration solvers, its effectiveness highly depends on the iterators used.

Program synthesis is the task of generating a program that suffices the intent of a user based on a set of input-output examples. Searching over the set of all possible programs becomes intractable very quickly. Therefore, divide and conquer techniques have become popular within the field, but have mainly been applied on the set of examples. However, this paper focuses on applying the strategy on the problem’s context-free grammar by splitting it into subgrammars.
Our new technique first splits the grammar by making a dependency graph showing how all rules relate the different types of symbols. Afterwards, there is an exploration and exploitation phase where different sets of subgrammars will be given a score and get allocated an amount of enumerations to generate programs based on that score.
The new technique is implemented as an iterator in Herb.jl which is a program synthesis framework. The iterator is then benchmarked against a plain BFS iterator using 100 string-manipulation problems. The grammar splitting strategy needs on average more enumerations to find a program solving all examples compared to the BFS iterator. However, running the different grammars from the iterator in parallel could allow the iterator to find a solution from one of the grammars earlier.

Program synthesis tackles the challenge of generating programs from user specifications, a task proven undecidable due to the exponential search space growth. In program synthesis the Divide and Conquer technique can be employed to prune this search. By decomposing specifications into individual examples, multiple programs are synthesized to solve them separately. Later these small programs are combined into a bigger program which should satisfy all input-output pairs by itself. There have been previous successful attempts at using Divide and Conquer, including combining programs using decision trees. However, a gap persists in the program synthesis community regarding comprehensive frameworks for integrating diverse implementation strategies. This project addresses this gap by incorporating a Divide and Conquer algorithm into a program synthesis library, enabling users to explore different ways of generating the small programs while abstracting the unification procedure. Moreover, we also discuss a "greedy" strategy to generate the programs that will be combined. We found that a Divide and Conquer manages to improve naive search, especially when given more than 10 examples.

Program synthesis is the task to construct a program that provably satisfies a given high-level specification. There are various ways in which a specification can be described. This research focuses on adapting the Probe synthesizer, traditionally reliant on input-output examples, to utilize reward-based synthesis. The generalization of Probe allows for flexibility in using various search algorithms, selection and updating algorithms, enhancing its applicability to a general case. By modifying the Probe algorithm to learn from rewards, we explore how exploiting existing programs as partial solutions impacts synthesis performance. Different ways of exploitation were tested, specifically, how much the probabilities change, and how a starting probabilities can affect the synthesis. Exploitation of programs could lead to faster synthesis but it could also lead to no solutions depending on the world environment.

Program synthesis involves finding a program that meets the user intent, typically provided as input/output examples or formal mathematical specifications. This paper explores a novel specification in program synthesis - learning from rewards.
We explore existing synthesizers, Probe and FrAngel, to solve navigation tasks inside the popular Minecraft game. The problem formulation is inspired by reinforcement learning but was adapted to program synthesis. Similar to reinforcement learning, balancing exploration and exploitation is essential for solving the task efficiently. Excessive exploration can prevent finding the correct program because the feedback from the environment is not used. On the other hand, excessive exploitation is not ideal, as seemingly promising programs might not lead to the actual solution. This work compares different trade-offs between exploration and exploitation of Probe and FrAngel when applied to Minecraft environments.

Program synthesis is the process of constructing programs that provably satisfy a given high-level user specification. Recent work in this domain has focused on utilizing domain-specific languages to guide the search procedure. This study proposes a novel approach to enhance the efficiency of such search procedures. By utilizing anti-unification, which is the process of generating the least general pattern between two symbolic expressions, this work aims to find common sub-components to enhance the language used in program synthesis to reduce search depth and improve performance.

Program synthesis has been extensively used for automating code-related tasks, but it has yet to be applied in the realm of reward-based games. FrAngel is a component-based program synthesizer that addresses the aspects of exploration and exploitation, both important for the performance of a program synthesizer. However, its specific implementation makes it hard to study and extend. We first implement a generalized version of FrAngel that takes arbitrary grammars and program generators, while also generalizing most of its features by redesign. We then use it to introduce a novel approach to formulating a reward-based problem into an inductive specification. We integrate this algorithm within MineRL, an AI framework for playing Minecraft. Lastly, we lay the groundwork for using program synthesis for Minecraft by investigating the ways of tuning the algorithm to generate complex subprograms. By changing the configuration parameters, as well as slightly changing the algorithm’s implementation, we managed to observe a significant increase in the complexity of fragments and generated programs. These modifications are a stepping stone towards using program synthesis to solve complex game tasks.

Program synthesis remains largely unexplored in the context of playing games, where exploration and exploitation are crucial for solving tasks within complex environments. FrAngel is a program synthesis algorithm that addresses both of these aspects with its fragments used for the generation of new candidate programs. We introduce a generalised version of the FrAngel program synthesis algorithm that accepts an arbitrary iterator and grammar, enabling flexible modifications. We then formulate Program by Example (PBE) program synthesis from rewards and apply this framework to Minecraft's navigation task, where dense rewards guide the algorithm's exploration. Then, we use the generalised version of the algorithm to conduct experiments in the context of exploration of the algorithm. The experiments show the importance of exploration as a step required for the exploitation and finding the wanted solution to the task while also revealing that sometimes more exploration does not necessarily mean reaching the solution faster.