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

• URL: http://arxiv.org/abs/2601.11840v1
• Date: Sat, 17 Jan 2026 00:16:41 GMT
• Title: Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
• Authors: Hongyu Lin, Samer Abdallah, Makar Valentinov, Paul Brennan, Elijah Kagan, Christoph M. Wintersteiger, Denis Ignatovich, Grant Passmore,
• Abstract summary: Large Language Models (LLMs) have shown strong performance on code understanding tasks.<n>LLMs lack the ability to perform precise, exhaustive mathematical reasoning about program behavior.<n>We present CodeLogician, a neurosymbolic agent for precise analysis of software logic, integrated with ImandraX.
• Score: 23.59512682324697
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Enhancing Mathematical Problem Solving in LLMs through Execution-Driven Reasoning Augmentation [18.636244209466266]
  Iteratively Improved Program Construction (IIPC) is a reasoning method that iteratively refines programmatic reasoning chains and combines execution feedback with the native Chain-of-thought abilities of the base LLM.<n>IIPC surpasses competing approaches in the majority of reasoning benchmarks on multiple base LLMs.
  arXiv  Detail & Related papers  (2026-02-03T19:13:31Z)
• An Agentic Framework for Autonomous Materials Computation [70.24472585135929]
  Large Language Models (LLMs) have emerged as powerful tools for accelerating scientific discovery.<n>Recent advances integrate LLMs into agentic frameworks, enabling retrieval, reasoning, and tool use for complex scientific experiments.<n>Here, we present a domain-specialized agent designed for reliable automation of first-principles materials computations.
  arXiv  Detail & Related papers  (2025-12-22T15:03:57Z)
• Training LLMs with LogicReward for Faithful and Rigorous Reasoning [75.30425553246177]
  We propose LogicReward, a reward system that guides model training by enforcing step-level logical correctness with a theorem prover.<n>An 8B model trained on data constructed with LogicReward surpasses GPT-4o and o4-mini by 11.6% and 2% on natural language inference and logical reasoning tasks.
  arXiv  Detail & Related papers  (2025-12-20T03:43:02Z)
• From Code Foundation Models to Agents and Applications: A Practical Guide to Code Intelligence [150.3696990310269]
  Large language models (LLMs) have transformed automated software development by enabling direct translation of natural language descriptions into functional code.<n>We provide a comprehensive synthesis and practical guide (a series of analytic and probing experiments) about code LLMs.<n>We analyze the code capability of the general LLMs (GPT-4, Claude, LLaMA) and code-specialized LLMs (StarCoder, Code LLaMA, DeepSeek-Coder, and QwenCoder)
  arXiv  Detail & Related papers  (2025-11-23T17:09:34Z)
• SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation [5.88623604115872]
  We introduce SymCode, a neurosymbolic framework that reframes mathematical problem-solving as a task of verifiable code generation.<n>We evaluate SymCode on challenging benchmarks, including MATH-500 and OlympiadBench, demonstrating significant accuracy improvements.
  arXiv  Detail & Related papers  (2025-10-29T21:17:57Z)
• Do LLMs Dream of Discrete Algorithms? [0.7646713951724011]
  Large Language Models (LLMs) have rapidly transformed the landscape of artificial intelligence.<n>Their reliance on probabilistic inference limits their effectiveness in domains requiring strict logical reasoning.<n>This paper proposes a neurosymbolic approach that augments LLMs with logic-based reasoning modules.
  arXiv  Detail & Related papers  (2025-06-29T22:03:01Z)
• Computational Thinking Reasoning in Large Language Models [69.28428524878885]
  Computational Thinking Model (CTM) is a novel framework that incorporates computational thinking paradigms into large language models (LLMs)<n>Live code execution is seamlessly integrated into the reasoning process, allowing CTM to think by computing.<n>CTM outperforms conventional reasoning models and tool-augmented baselines in terms of accuracy, interpretability, and generalizability.
  arXiv  Detail & Related papers  (2025-06-03T09:11:15Z)
• Computational Reasoning of Large Language Models [51.629694188014064]
  We introduce textbfTuring Machine Bench, a benchmark to assess the ability of Large Language Models (LLMs) to execute reasoning processes.<n> TMBench incorporates four key features: self-contained and knowledge-agnostic reasoning, a minimalistic multi-step structure, controllable difficulty, and a theoretical foundation based on Turing machine.
  arXiv  Detail & Related papers  (2025-04-29T13:52:47Z)
• Evaluating Intermediate Reasoning of Code-Assisted Large Language Models for Mathematics [15.695635219034328]
  We conduct an in-depth analysis of code-assisted LLMs generated programs in response to math reasoning tasks.<n>Our findings show that the capabilities of models significantly impact the logic implemented to solve the problem.
  arXiv  Detail & Related papers  (2025-04-24T15:34:24Z)
• Code to Think, Think to Code: A Survey on Code-Enhanced Reasoning and Reasoning-Driven Code Intelligence in LLMs [53.00384299879513]
  In large language models (LLMs), code and reasoning reinforce each other.<n>Code provides verifiable execution paths, enforces logical decomposition, and enables runtime validation.<n>We identify key challenges and propose future research directions to strengthen this synergy.
  arXiv  Detail & Related papers  (2025-02-26T18:55:42Z)
• Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment [21.12989936864145]
  Chain-of-Thought (CoT) prompting has shown promise in enhancing the reasoning capabilities of large language models (LLMs)<n>We propose Reasoning-as-Logic-Units (RaLU), which constructs a more reliable reasoning path by aligning logical units between the generated program and their corresponding NL descriptions.
  arXiv  Detail & Related papers  (2025-02-05T08:23:18Z)
• Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models [56.34029644009297]
  Large language models (LLMs) have demonstrated the ability to overcome various limitations of formal Knowledge Representation (KR) systems. LLMs excel most in abductive reasoning, followed by deductive reasoning, while they are least effective at inductive reasoning. We study single-task training, multi-task training, and "chain-of-thought" knowledge distillation fine-tuning technique to assess the performance of model.
  arXiv  Detail & Related papers  (2023-10-02T01:00:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.