Iteratively refined symbolic encodings with agentic AI

Formal encodings allow the representation of knowledge and constraints. Inference mechanisms enable verification, deduction, automated reasoning, and much more. Yet, all such processes presuppose that the underlying formalization correctly represents the intended logic of the problem, constituting a major bottleneck. Automatically synthesizing sound encodings from natural language remains an open challenge. With the ongoing improvements in large language models, coupling them with formal logic – commonly termed neuro-symbolic methods – has emerged as a promising approach. In this thesis, we present a framework that combines methods from logic, natural language processing, and graph theory to facilitate encoding generation. We implement synthesis as an iterative refinement process that exploits different states of reasoning. Additionally, we propose a measure of closeness that relates synthesized formulations to the underlying ground truth, and discuss its properties. We show that this measure is able to steer synthesis to sound and complete formulations. We empirically underpin the proposed framework by evaluating it on a range of arithmetic and combinatorial problems. Results indicate that we were able to substantially improve synthesis compared to naïve, single-shot generation approaches.