論文の概要: Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models
- arxiv url: http://arxiv.org/abs/2506.08171v1
- Date: Mon, 09 Jun 2025 19:33:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-11 15:11:40.559497
- Title: Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models
- Title(参考訳): 大規模言語モデルを用いた最悪ケースシンボリック制約解析と一般化
- Authors: Daniel Koh, Yannic Noller, Corina S. Pasareanu, Adrians Skapars, Youcheng Sun,
- Abstract要約: 大規模言語モデル(LLM)は、コード生成、補完、修復など、様々なコーディングタスクにうまく適用されている。
本稿では,プログラムにおける最悪のケース実行をシンボリック制約解析により推論するLLMの能力について検討する。
- 参考スコア(独自算出の注目度): 11.612762531670212
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models (LLMs) have been successfully applied to a variety of coding tasks, including code generation, completion, and repair. However, more complex symbolic reasoning tasks remain largely unexplored by LLMs. This paper investigates the capacity of LLMs to reason about worst-case executions in programs through symbolic constraints analysis, aiming to connect LLMs and symbolic reasoning approaches. Specifically, we define and address the problem of worst-case symbolic constraints analysis as a measure to assess the comprehension of LLMs. We evaluate the performance of existing LLMs on this novel task and further improve their capabilities through symbolic reasoning-guided fine-tuning, grounded in SMT (Satisfiability Modulo Theories) constraint solving and supported by a specially designed dataset of symbolic constraints. Experimental results show that our solver-aligned model, WARP-1.0-3B, consistently surpasses size-matched and even much larger baselines, demonstrating that a 3B LLM can recover the very constraints that pin down an algorithm's worst-case behaviour through reinforcement learning methods. These findings suggest that LLMs are capable of engaging in deeper symbolic reasoning, supporting a closer integration between neural network-based learning and formal methods for rigorous program analysis.
- Abstract(参考訳): 大規模言語モデル(LLM)は、コード生成、補完、修復など、様々なコーディングタスクにうまく適用されている。
しかし、より複雑なシンボリック推論タスクは、LLMによってほとんど探索されていない。
本稿では,LLM と記号的推論手法を結びつけることを目的として,LLM のプログラムにおける最悪のケース実行をシンボリック制約解析により推論する能力について検討する。
具体的には,LLMの理解度を評価する尺度として,最悪のケースのシンボリック制約解析の問題を定義・解決する。
本研究は,SMT(Satisfiability Modulo Theories)制約の解法と,特別に設計されたシンボリック制約のデータセットを用いて,既存のLLMの性能を評価し,その性能を向上させることを目的とする。
その結果、3B LLM はアルゴリズムの最悪の動作を補強学習法によって抑えることができることを示した。
これらの結果から,LLMはより深い記号的推論を行うことができ,ニューラルネットワークに基づく学習と厳密なプログラム分析のための形式的手法との密接な統合を支援することが示唆された。
関連論文リスト
- Computational Thinking Reasoning in Large Language Models [69.28428524878885]
計算思考モデル(CTM)は、計算思考パラダイムを大規模言語モデル(LLM)に組み込んだ新しいフレームワークである。
ライブコード実行は推論プロセスにシームレスに統合され、CTMが計算によって考えることができる。
CTMは、精度、解釈可能性、一般化可能性の観点から、従来の推論モデルとツール拡張ベースラインを上回っている。
論文 参考訳(メタデータ) (2025-06-03T09:11:15Z) - CrossWordBench: Evaluating the Reasoning Capabilities of LLMs and LVLMs with Controllable Puzzle Generation [53.452699232071495]
CrossWordBenchは、大きな言語モデル(LLM)とLVLM(Large Vision-Language Models)の推論能力を評価するために設計されたベンチマークである。
評価の結果,LLMの推論は,クロスレター制約を効果的に活用することにより,非推論モデルよりも大幅に優れていることがわかった。
本研究は,現在のLLMとLVLMの推論能力の限界について考察し,今後の評価のために,マルチモーダル制約タスクを作成するための効果的なアプローチを提供する。
論文 参考訳(メタデータ) (2025-03-30T20:03:36Z) - ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning [92.76959707441954]
我々はLLM推論性能を評価するための総合的な評価フレームワークであるZebraLogicを紹介した。
ZebraLogicは、制御可能で定量化可能な複雑さを持つパズルの生成を可能にする。
その結果,複雑性が増大するにつれて,精度が著しく低下することが明らかとなった。
論文 参考訳(メタデータ) (2025-02-03T06:44:49Z) - Inductive Learning of Logical Theories with LLMs: An Expressivity-Graded Analysis [9.865771016218549]
本研究は,Large Language Models(LLM)の機能と限界を分析するための,新しい体系的方法論を提案する。
この分析は、LLM性能に関する特定の推論課題の定量化を可能にする、複雑性グレードのw.r.t.ルール依存構造である。
論文 参考訳(メタデータ) (2024-08-15T16:41:00Z) - Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planning [53.6472920229013]
大規模言語モデル(LLM)は多くの自然言語タスクにおいて印象的な能力を示している。
LLMは多段階推論を行う際にエラー、幻覚、矛盾する文を生成する傾向がある。
本稿では,LLMの復号化過程を検討計画で導くためのフレームワークであるQ*を紹介する。
論文 参考訳(メタデータ) (2024-06-20T13:08:09Z) - Investigating Symbolic Capabilities of Large Language Models [16.88906206735967]
本研究の目的は,一連の記号的タスクにおいて,LLM(Large Language Models)を厳格に評価することにより,ギャップを埋めることである。
我々の分析では、エンタープライズグレードの4つのモデルとオープンソースの4つのモデルを含む8つのLCMを含み、そのうち3つは数学的なタスクで事前訓練されている。
その結果,記号数で表される複雑性が増大するにつれて,LLMの文脈自由かつ文脈依存的な記号処理における性能が著しく低下することが明らかとなった。
論文 参考訳(メタデータ) (2024-05-21T21:24:34Z) - DiLA: Enhancing LLM Tool Learning with Differential Logic Layer [11.810200077863172]
本稿では,ネットワーク層の前方・後方通過に論理的制約を組み込むディファレンシャル・ロジック・レイヤ支援言語モデリング(DiLA)手法を提案する。
2つの古典的推論問題に対するDiLAの性能評価を行い、既存のプロンプトベースおよびソルバ支援アプローチに対する一貫した性能を実証した。
論文 参考訳(メタデータ) (2024-02-19T07:38:57Z) - Evaluating LLMs' Mathematical and Coding Competency through Ontology-guided Interventions [47.83142414018448]
算術的推論とコード生成という,2つの一般的な推論タスクに注目します。
i) 数学やコーディング問題に対する摂動の一般的なオントロジー, (ii) 摂動を応用するための半自動手法, (iii) 2つのデータセットを紹介する。
混乱した質問に対して、すべてのモデルで大幅なパフォーマンス低下を示します。
論文 参考訳(メタデータ) (2024-01-17T18:13:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。