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
CodeLogician bridges LLM-based software understanding with formal reasoning by translating code into executable formal models and delegating rigorous analysis to ImandraX. The approach shifts away from verification-as-filtering toward building explicit models whose reasoning is exhaustively explored via region decomposition and formal proofs, enabling answers about state spaces, boundaries, and edge cases. Empirical evaluation on code-logic-bench shows that formal augmentation closes a 41–47 percentage-point gap in reasoning accuracy relative to LLM-only methods, underscoring the value of neurosymbolic integration for scalable, precise software analysis. The framework is designed to be reasoner-agnostic and extensible, with a server architecture and PyIML strategies enabling project-wide formalization and continuous verification in real-world development workflows.
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.