Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic

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 reasoning about software logic, we introduce code-logic-bench, a benchmark targeting the middle ground between theorem proving and software engineering benchmarks. It measures reasoning correctness about program state spaces, control flow, coverage constraints, and edge cases, with ground truth defined via formal modeling and region decomposition. Comparing LLM-only reasoning against LLMs augmented with CodeLogician, formal augmentation yields substantial improvements, closing a 41-47 percentage point gap in reasoning accuracy. These results demonstrate that neurosymbolic integration is essential for scaling program analysis toward rigorous, autonomous software understanding.