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 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 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 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 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 is an important problem in computer science. One method often employed is enumerative program synthesis, which produces a sequence of programs in the target language until one solves the required input-output examples. This can yield undesirable runtimes for some problems that require complex programs to solve them. This research is about how simpler problem solutions can be used to build a library of useful helper functions and to use it for further synthesis in order to reduce the depth of the enumerative search for more complex problems. Drawing inspiration from the work by Ellis, et al on DreamCoder, this research describes ways of obtaining simpler programs, and extending the grammar using parts of the solutions. Experiments have been performed on the proposed synthesis algorithm, which is implemented using the Herb.jl framework, and results for each part of the synthesis algorithm being replaced by different strategies are provided. Allowing holes in the new grammar substitutions and using smaller size or frequency as their utility has proven superior. There needs to be more work done about the conciseness of the produced programs.

Program synthesis is the task of generating a program that satisfies some specification. An important aspect of program synthesis is the method of specification. There are various ways in which a desired program can be specified, such as I/O examples, traces, and natural language. This research paper aims to explore a novel method of specifying a desired program in program synthesis -- rewards. This concept is explored by adjusting the Probe program synthesiser to solve the dense navigation environments in MineRL. In order to avoid local maxima, it is necessary to increase the amount of exploration. To that end, different ways of increasing exploration were tested by changing the parameters of Probe. By increasing the amount of exploration, it is possible to solve more environments, or solve them faster. But increasing exploration could also have the opposite effect, depending on the environment.

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.

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.

This paper explores the application of landmark-based planning algorithms, specifically focusing on AND/OR landmark extraction methods. Drawing from classical planning principles and recent advancements, we investigate the effectiveness of landmark extraction in guiding the search for solutions to planning problems. Our research questions center on identifying effective domains for landmark extraction, assessing the utility of extracted landmarks, and comparing our implementation with existing literature. Utilizing the Symbolicplanners.jl framework, we implement AND/OR landmark extraction and evaluate its performance across various domains. Due to challenges in implementation, the landmarks we were able to extract had limited meaning. We propose future work to refine the AND/OR method and expand our analysis to include the Hm procedure.

The Fast Downward planning system is currently mainly used for solving classical problems. Another alternative to Fast Downward is SymbolicPlanners, which sacrifices speed for generality and extensibility. SymbolicPlanners is missing landmark based planners and landmark extraction algorithms. The research question we are trying to answer in this research paper is: What design choices can be made to adapt the forward propagation extraction algorithm into SymbolicPlanners?
The forward propagation landmark generation design choices are discussed and implemented in SymbolicPlanners. The runtime performance of the implementation is only about two times slower than the Fast Downward implementation. Another aspect of the implementation is the incorrect amount of landmarks generated in complex problems caused by limitation in the relaxed planning graph from SymbolicPlanners.

Landmarks are propositions or actions that must be true at some point in every valid solution plan [16]. Using landmarks, planners can develop solutions more efficiently. Different algorithms exist to extract landmarks from a planning problem. The one used in this study is FULL [13], a landmark extraction algorithm by Marzal et al. from 2011.
In this research, the performance of the FULL algorithm is analysed by comparing the total number of landmarks found to two other landmark extraction algorithms, namely forward propagation by Zhu and Givan [22] and backward propagation by Porteous et al. [16].
The original FULL algorithm is slightly modified, by removing orderings and disjunctive landmark extraction. FULL is implemented using Julia and was run on five different domains from the International Planning Competitions.
All of these domains are logical and 15 problems were randomly selected from them.
FULL managed to extract more landmarks in two out of the five domains, Grid and Logistics, compared to the two aforementioned algorithms.
In the three other domains, FULL matched the number of landmarks found by the best out of the two. The two domains where FULL performed well, were both transportation domains and this is where FULL's performance excels.
Runtime was not an issue when extracting landmarks in four of the five domains. Freecell consistently exceeded the timeout put in place, likely due to a bug.
Furthermore, a higher number of landmarks is also a desired outcome due to its use in planners, either as heuristics or intermediary goals.

Many real-world problems fall in the category of sequential decision-making under uncertainty; Markov Decision Processes (MDPs) are a common method for modeling such problems. To solve an MDP, one could start from scratch or one could already have an idea of what good policies look like. Furthermore, there could be uncertainty in this idea. In existing literature, a policy search procedure is accelerated by encoding this prior knowledge in an action distribution which is used for policy sampling. Moreover, this is then extended by inferring these action distributions while inferring the policy through Gibbs sampling. Implicitly, this approach assumes a generalization of good and bad actions over the entire state space.

This thesis extends the existing method by leveraging a division of the state space into regions and inferring action distributions over these regions, rather than over the entire state space. We show that this can accelerate the policy search. We also show that the algorithm manages to recover if the division is unjustified. The division into regions can hence also be considered a form of prior knowledge of the policy with uncertainty. Finally, inference of the regions themselves is also explored and yields promising results.

Algorithmic planners occasionally waste effort and thus computing time trying to solve certain tasks, as they often lack the human ability to recognize essential paths. These essential paths, termed landmarks, are vital for optimizing planning processes. This study revisits landmark-based planning methods introduced by Richter, Helmert, and Westphal in their 2008 paper, adapting and implementing them within a different framework, SymbolicPlanners, using the Julia programming language. The primary research question explores the performance of using landmarks as intermediary goals and pseudo-heuristics in the SymbolicPlanner framework. Sub-questions delve into the effectiveness of specific planning strategies, such as A^∗ Planner with GoalCount and HAdd heuristics, as well as planners utilizing landmarks. Evaluation over diverse domains reveals that LM^Local  and LM^LocalSmart outperform the basic GoalCount
heuristic and are on par with the HAdd heuristic. LM^Count, despite solving fewer instances, exhibits speed improvements over GoalCount in the instances that they both solve. Discussion highlights limitations, such as the non-exhaustive interference check in LM^LocalSmart and limiting factors in the SymbolicPlanner framework.

A lot of research has been conducted to make the task of plan generation more efficient. One idea to do so is the use of landmarks, which are sub-goals that must be true in every solution to the problem. The approximation of landmarks has a lower complexity than solving the task itself, and they can be used to guide the planner in the right direction.
In previous work, ideas to order landmarks are proposed and compared to algorithms that do not use them. We verify if this comparison is fair by testing both algorithms implemented in the same language and framework. In our experiment not many problem instances finish in time, but those that do are in line with previous experiments in that on average planners using landmarks produce longer solutions than planners that do not use them.

Inductive logic programming is a technique that generates logic programs which keep to a given specification using a background knowledge. We propose a new task in the field of pro- gram synthesis called Time-gated Partition-selection Inductive Logic Programming, consisting of splitting the background knowledge into partitions and selecting only the relevant partitions to a given set of examples. In order to show an initial direction of research and demonstrate the effectiveness of the approach, we have constructed a set of partitioning functions and a selection function. These were implemented using existing graph clustering and community detection algorithms applied to static call graphs of existing programs in the target language and using a linear time evaluation selection function. By comparing the inductive logic programming approach Popper to a version of Popper with its search space reduced using this technique, we show that these partitioning- and selection functions can improve the generated programs on three out of four different domains. Finally we show that there is a difference in partition quality by comparing the results to a random partitioning function. This work establishes background knowledge partitioning- and selection as a useful tool in program synthesis research.

Solving routing problems efficiently is instrumental in minimizing operational costs in logistics. These routing problems are hard to solve and often take a lot of time to find a good solution. In this thesis, we present a methodology that tackles the challenge of efficiently solving recurring instances of the Vehicle Routing Problem with Time Windows by recycling solutions. By making more problem-specific assumptions, we introduce a solution recycling approach that can leverage shared solution structures across similar instances. This accelerates the solution-finding process. We implement our methodology in the framework of constraint programming and show that such a methodology is actually useful and is a concept that is yet unexplored in combinatorial optimization.