The field of formal theorem proving and probabilistic modeling is experiencing significant developments, with a focus on improving the accuracy and efficiency of large language models (LLMs) in discharging proof obligations and generating formal statements. Researchers are exploring new architectures and training techniques to enhance the performance of LLMs in these tasks. Notably, the integration of syntactic and consistency information into the formalization process is showing promising results. Additionally, advancements in probabilistic modeling are being made, including the development of diagrammatic calculi for reasoning about hybrid probabilistic models and the introduction of new monads for modeling ordered nondeterministic computations.

Some noteworthy papers in this area include: FormalML, which introduces a benchmark for evaluating formal subgoal completion in machine learning theory. Aria, which presents a system for conjecture-level formalization in Lean that emulates human expert reasoning via a two-phase Graph-of-Thought process. Autoformalizer with Tool Feedback, which proposes a novel approach that incorporates syntactic and consistency information into the formalization process. A Complete Diagrammatic Calculus for Conditional Gaussian Mixtures, which develops a string diagrammatic syntax for expressing and combining hybrid probabilistic models.