論文の概要: Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic

• arxiv url: http://arxiv.org/abs/2601.11840v1
• Date: Sat, 17 Jan 2026 00:16:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-21 22:47:22.339633
• Title: Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
• Title（参考訳）: Imandra CodeLogician:ソフトウェア論理の精密解析のためのニューロシンボリック推論
• Authors: Hongyu Lin, Samer Abdallah, Makar Valentinov, Paul Brennan, Elijah Kagan, Christoph M. Wintersteiger, Denis Ignatovich, Grant Passmore,
• Abstract要約: 大きな言語モデル(LLM)は、コード理解タスクに強いパフォーマンスを示しています。 LLMには、プログラムの振る舞いに関する正確で徹底的な数学的推論を行う能力がない。 本稿では,ImandraXと統合されたソフトウェア論理の精密解析のためのニューロシンボリックエージェントであるCodeLogicianについて述べる。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、コード理解タスクに強いパフォーマンスを示してきたが、プログラムの振る舞いに関する正確で徹底的な数学的推論を実行する能力は基本的に欠如している。 既存のベンチマークでは、実世界のソフトウェアから大きく切り離された数学的証明自動化や、意味論的厳密さを必要としないエンジニアリングタスクに焦点が当てられている。 我々は,ソフトウェアロジックを正確に分析するための神経象徴的エージェントであるCodeLogicianを,金融市場や安全クリティカルシステムに展開する産業用自動推論エンジンであるImandraXと統合した。 形式的手法を主にLCMの出力を検証する以前のアプローチとは異なり、CodeLogicianはLSMを使ってソフトウェアシステムの明示的な形式的モデルを構築し、自動推論によってバイナリ検証結果以上のリッチな意味論に答えることができる。 ソフトウェア論理に関する数学的推論を厳格に評価するために,定理証明とソフトウェア工学ベンチマークの中間点を対象としたベンチマークであるCode-logic-benchを導入する。 プログラム状態空間、制御フロー、カバレッジ制約、エッジケースに関する推論正当性を測定する。 CodeLogician と拡張された LLM に対する LLM のみの推論と比較すると、形式的な拡張は大幅に改善され、推論精度において41-47 のポイントギャップを閉じる。 これらの結果は、プログラム分析を厳密で自律的なソフトウェア理解へと拡張するために、ニューロシンボリック統合が不可欠であることを証明している。

関連論文リスト

• From Code Foundation Models to Agents and Applications: A Practical Guide to Code Intelligence [150.3696990310269]
  大規模言語モデル(LLM)は、自然言語記述を直接関数コードに変換することによって、自動ソフトウェア開発を変革した。 コードLLMに関する総合的な合成と実践的ガイド(一連の解析および探索実験)を提供する。 一般LLM(GPT-4, Claude, LLaMA)とコード特殊化LLM(StarCoder, Code LLaMA, DeepSeek-Coder, QwenCoder)のコード機能の解析を行う。
  論文  参考訳（メタデータ） (2025-11-23T17:09:34Z)
• SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation [5.88623604115872]
  検証可能なコード生成のタスクとして数学的問題解決を再構築する,ニューロシンボリックなフレームワークであるSymCodeを紹介する。 我々は、MATH-500やOlympiadBenchなど、挑戦的なベンチマークでSymCodeを評価し、大幅な精度向上を示した。
  論文  参考訳（メタデータ） (2025-10-29T21:17:57Z)
• Do LLMs Dream of Discrete Algorithms? [0.7646713951724011]
  大規模言語モデル(LLM)は、人工知能の風景を急速に変化させてきた。 確率的推論への依存は、厳密な論理的推論を必要とする領域における有効性を制限する。 本稿では,論理ベースの推論モジュールでLLMを増強するニューロシンボリックアプローチを提案する。
  論文  参考訳（メタデータ） (2025-06-29T22:03:01Z)
• Computational Thinking Reasoning in Large Language Models [69.28428524878885]
  計算思考モデル(CTM)は、計算思考パラダイムを大規模言語モデル(LLM)に組み込んだ新しいフレームワークである。 ライブコード実行は推論プロセスにシームレスに統合され、CTMが計算によって考えることができる。 CTMは、精度、解釈可能性、一般化可能性の観点から、従来の推論モデルとツール拡張ベースラインを上回っている。
  論文  参考訳（メタデータ） (2025-06-03T09:11:15Z)
• Computational Reasoning of Large Language Models [51.629694188014064]
  textbfTuring Machine Benchは,Large Language Models(LLM)による推論プロセスの実行能力を評価するベンチマークである。 TMBenchには、自己完結型および知識に依存しない推論、最小主義的な多段階構造、制御可能な難易度、チューリングマシンに基づく理論的基礎の4つの重要な特徴が組み込まれている。
  論文  参考訳（メタデータ） (2025-04-29T13:52:47Z)
• Evaluating Intermediate Reasoning of Code-Assisted Large Language Models for Mathematics [15.695635219034328]
  我々は,コード支援型LCM生成プログラムを,数理推論タスクに応答して詳細に解析する。 この結果から, モデルの性能が, 問題の解法として実装された論理に大きく影響していることが示唆された。
  論文  参考訳（メタデータ） (2025-04-24T15:34:24Z)
• Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment [21.12989936864145]
  CoT(Chain-of-Thought)のプロンプトによって,大規模言語モデル(LLM)の推論能力の向上が期待できる。 本稿では、生成したプログラムと対応するNL記述との間に論理単位を整列させることにより、より信頼性の高い推論経路を構築するReasoning-as-Logic-Units (RaLU)を提案する。
  論文  参考訳（メタデータ） (2025-02-05T08:23:18Z)
• Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models [56.34029644009297]
  大規模言語モデル(LLM)は、形式的知識表現(KR)システムの様々な制限を克服する能力を示した。 LLMは誘導的推論において最も優れているが、誘導的推論では最も効果が低い。 モデルの性能を評価するため,シングルタスクトレーニング,マルチタスクトレーニング,および「チェーンオブ思考」知識蒸留細調整技術について検討した。
  論文  参考訳（メタデータ） (2023-10-02T01:00:50Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。