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.

In this work residual error estimates are constructed using Neural Networks for Finite Element Method. These can be used to do adaptive mesh refinement. Two neural networks are developed the Multilayer Perceptron and the Transformer model. The error estimates are made for 1d poisson equations but the idea will generalise to higher dimensions as well.