論文の概要: Beyond Basic Specifications? A Systematic Study of Logical Constructs in LLM-based Specification Generation

• arxiv url: http://arxiv.org/abs/2602.00715v1
• Date: Sat, 31 Jan 2026 13:19:40 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-02-03 14:25:44.92175
• Title: Beyond Basic Specifications? A Systematic Study of Logical Constructs in LLM-based Specification Generation
• Title（参考訳）: 基本仕様を超えて : LLM仕様生成における論理的構成の体系的研究
• Authors: Zehan Chen, Long Zhang, Zhiwei Zhang, JingJing Zhang, Ruoyu Zhou, Yulong Shen, JianFeng Ma, Lin Yang,
• Abstract要約: プログラム仕様の自動生成のための大規模言語モデル(LLM)は、検証効率を向上させるための有望な道として登場した。 既存の LLM 仕様生成フレームワークに論理構造を組み込むことを提案する。 我々は,様々な種類の構文構造が仕様生成フレームワークに与える影響について,実証的研究を行った。
• 参考スコア（独自算出の注目度）: 29.231420590756954
• License:
• Abstract: Formal specifications play a pivotal role in accurately characterizing program behaviors and ensuring software correctness. In recent years, leveraging large language models (LLMs) for the automatic generation of program specifications has emerged as a promising avenue for enhancing verification efficiency. However, existing research has been predominantly confined to generating specifications based on basic syntactic constructs, falling short of meeting the demands for high-level abstraction in complex program verification. Consequently, we propose incorporating logical constructs into existing LLM-based specification generation framework. Nevertheless, there remains a lack of systematic investigation into whether LLMs can effectively generate such complex constructs. To this end, we conduct an empirical study aimed at exploring the impact of various types of syntactic constructs on specification generation framework. Specifically, we define four syntactic configurations with varying levels of abstraction and perform extensive evaluations on mainstream program verification datasets, employing a diverse set of representative LLMs. Experimental results first confirm that LLMs are capable of generating valid logical constructs. Further analysis reveals that the synergistic use of logical constructs and basic syntactic constructs leads to improvements in both verification capability and robustness, without significantly increasing verification overhead. Additionally, we uncover the distinct advantages of two refinement paradigms. To the best of our knowledge, this is the first systematic work exploring the feasibility of utilizing LLMs for generating high-level logical constructs, providing an empirical basis and guidance for the future construction of automated program verification framework with enhanced abstraction capabilities.
• Abstract（参考訳）: 形式的な仕様は、プログラムの振る舞いを正確に表現し、ソフトウェアの正しさを保証する上で重要な役割を担います。 近年,プログラム仕様の自動生成に大規模言語モデル(LLM)を活用することが,検証効率向上の道のりとして期待されている。 しかし、既存の研究は主に基本的な構文構造に基づく仕様の作成に限られており、複雑なプログラム検証におけるハイレベルな抽象化の要求を満たすには至っていない。 そこで本稿では,既存の LLM 仕様生成フレームワークに論理構造を組み込むことを提案する。 しかしながら、LLMがそのような複雑な構造を効果的に生成できるかどうかについては、体系的な調査が残っていない。 そこで本研究では,様々な構文構造が仕様生成フレームワークに与える影響について,実証的研究を行った。 具体的には,抽象レベルの異なる4つの統語的構成を定義し,多種多様な代表LSMを用いて,主要なプログラム検証データセット上で広範囲な評価を行う。 実験結果はまず、LLMが有効な論理構造を生成することができることを確認した。 さらに分析したところ、論理的構造と基本的な構文的構成の相乗的利用は、検証のオーバーヘッドを大幅に増大させることなく、検証能力と堅牢性の両方の改善をもたらすことが明らかとなった。 さらに、2つの改良パラダイムの明確な利点を明らかにする。 我々の知る限り、これはLLMを利用して高レベルの論理構造を生成する可能性を探究する最初の体系的な研究であり、抽象化機能を強化した自動プログラム検証フレームワークの構築のための実証的な基礎とガイダンスを提供する。

関連論文リスト

• Closed-Loop LLM Discovery of Non-Standard Channel Priors in Vision Models [48.83701310501069]
  大規模言語モデル(LLM)はニューラルアーキテクチャサーチ(NAS)に対する変換的アプローチを提供する 我々は、LLMが性能テレメトリに基づいてアーキテクチャ仕様を洗練する条件付きコード生成タスクのシーケンスとして検索を定式化する。 AST(Abstract Syntax Tree)変異を用いて,有効かつ整合性のあるアーキテクチャの膨大なコーパスを生成する。 CIFAR-100の実験結果は、この手法の有効性を検証し、精度の統計的に有意な改善をもたらすことを示した。
  論文  参考訳（メタデータ） (2026-01-13T13:00:30Z)
• Discrete Tokenization for Multimodal LLMs: A Comprehensive Survey [69.45421620616486]
  本研究は、大規模言語モデル(LLM)用に設計された離散トークン化手法の最初の構造的分類と解析である。 古典的および近代的なパラダイムにまたがる8つの代表的なVQ変種を分類し、アルゴリズムの原理を分析し、力学を訓練し、LLMパイプラインとの統合に挑戦する。 コードブックの崩壊、不安定な勾配推定、モダリティ固有の符号化制約など、重要な課題を特定する。
  論文  参考訳（メタデータ） (2025-07-21T10:52:14Z)
• Do LLMs Dream of Discrete Algorithms? [0.7646713951724011]
  大規模言語モデル(LLM)は、人工知能の風景を急速に変化させてきた。 確率的推論への依存は、厳密な論理的推論を必要とする領域における有効性を制限する。 本稿では,論理ベースの推論モジュールでLLMを増強するニューロシンボリックアプローチを提案する。
  論文  参考訳（メタデータ） (2025-06-29T22:03:01Z)
• Enhancing Large Language Models through Structured Reasoning [15.472375478049823]
  本稿では,Large Language Models (LLM) を明示的構造化推論により拡張する新しい手法を提案する。 まず、非構造化データを明示的に推論ステップをアノテートすることで構造化形式に変換する。 次に、この構造化データセットを使用して、監視ファインチューニング(SFT)を通してLLMをトレーニングする。
  論文  参考訳（メタデータ） (2025-06-25T08:36:12Z)
• Will Pre-Training Ever End? A First Step Toward Next-Generation Foundation MLLMs via Self-Improving Systematic Cognition [89.50068130832635]
  自己改善認知 (SIcog) は、マルチモーダル知識によって次世代のMLLMを構築するための自己学習フレームワークである。 ステップバイステップの視覚的理解のためのChain-of-Descriptionを提案し、詳細なマルチモーダル推論をサポートするために構造化されたChain-of-Thought(CoT)推論を統合する。 実験は、マルチモーダル認知を増強したMLLMの開発におけるSIcogの有効性を示す。
  論文  参考訳（メタデータ） (2025-03-16T00:25:13Z)
• Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning [1.3003982724617653]
  大規模言語モデル(LLM)は自然言語処理に革命をもたらしたが、一貫性のない推論に苦戦している。 本研究では,LLM出力の信頼性と透明性を高めるフレームワークであるProof of Thoughtを紹介する。 主な貢献は、論理的整合性を高めるためのソート管理を備えた堅牢な型システム、事実的知識と推論的知識を明確に区別するための規則の明示である。
  論文  参考訳（メタデータ） (2024-09-25T18:35:45Z)
• Designing Algorithms Empowered by Language Models: An Analytical Framework, Case Studies, and Insights [86.06371692309972]
  本研究では,大規模言語モデル(LLM)に基づくアルゴリズムの設計と解析のための分析フレームワークを提案する。 提案する枠組みは頭痛を緩和する試みとして機能する。
  論文  参考訳（メタデータ） (2024-07-20T07:39:07Z)
• Generative transformations and patterns in LLM-native approaches for software verification and falsification [1.4595796095047369]
  より規律のあるエンジニアリングプラクティスに向けた基本的なステップは、コア機能単位生成変換の体系的な理解である、と我々は主張する。 まず、素早い相互作用を概念的シグネチャに抽象化する、生成変換のきめ細かい分類法を提案する。 我々の分析は分類学の有用性を検証するだけでなく、戦略的ギャップや相互関係も明らかにする。
  論文  参考訳（メタデータ） (2024-04-14T23:45:23Z)

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

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