Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
Hongyu Lin, Samer Abdallah, Makar Valentinov, Paul Brennan, Elijah Kagan, Christoph M. Wintersteiger, Denis Ignatovich, Grant Passmore

TL;DR
This paper introduces CodeLogician, a neurosymbolic system that enhances large language models with formal reasoning capabilities for precise software logic analysis, bridging the gap between code understanding and mathematical reasoning.
Contribution
It presents a novel neurosymbolic approach combining LLMs with formal methods for detailed software analysis and introduces a new benchmark for evaluating reasoning about program logic.
Findings
Formal augmentation improves reasoning accuracy by 41-47 percentage points.
CodeLogician enables automated reasoning about program state spaces and control flow.
The approach demonstrates significant progress towards rigorous, autonomous software understanding.
Abstract
Large Language Models (LLMs) have shown strong performance on code understanding tasks, yet they fundamentally lack the ability to perform precise, exhaustive mathematical reasoning about program behavior. Existing benchmarks either focus on mathematical proof automation, largely disconnected from real-world software, or on engineering tasks that do not require semantic rigor. We present CodeLogician, a neurosymbolic agent for precise analysis of software logic, integrated with ImandraX, an industrial automated reasoning engine deployed in financial markets and safety-critical systems. Unlike prior approaches that use formal methods primarily to validate LLM outputs, CodeLogician uses LLMs to construct explicit formal models of software systems, enabling automated reasoning to answer rich semantic questions beyond binary verification outcomes. To rigorously evaluate mathematical…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Engineering Research · Formal Methods in Verification · Advanced Software Engineering Methodologies
