論文の概要: Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications

• arxiv url: http://arxiv.org/abs/2603.13414v1
• Date: Thu, 12 Mar 2026 15:02:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-17 16:19:35.178569
• Title: Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
• Title（参考訳）: 記憶機能仕様のニューロ・シンボリック生成と検証
• Authors: Liao Zhang, Tong Chen, Xiwei Wu, Qi Liu, Xiyu Zhai, Xinqi Wang, Qinxiang Cao,
• Abstract要約: メモリ操作プログラムの形式的検証は、専門家によって書かれたメモリ状態をキャプチャする正確な機能仕様に依存している。 本稿では,Cプログラムのメモリ対応形式関数仕様を自動生成するニューロシンボリックフレームワークを提案する。 我々は,メモリ対応の形式関数仕様を生成するための200Cプログラミング問題のベンチマークであるLeetCode-C-Specを紹介する。
• 参考スコア（独自算出の注目度）: 12.783777562919383
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts. This requirement has become a major bottleneck as large language models (LLMs) increasingly generate low-level systems code whose correctness cannot be assumed. To enable scalable formal verification, we focus exclusively on function specification generation, deliberately avoiding the synthesis of complex loop invariants that are central to traditional verification pipelines. We propose a neuro-symbolic framework for automatically generating memory-aware formal function specifications for C programs from natural language problem descriptions and function signatures. The pipeline first produces candidate specifications via in-context learning, and then iteratively refines them using compiler diagnostics from symbolic provers and the verification toolchain. In particular, we validate candidate specifications by constructing a proof for the negation of the specification with concrete examples, enabling machine-checked rejection of plausible-but-incorrect specifications. To support systematic evaluation, we introduce LeetCode-C-Spec, a new benchmark of 200 C programming problems for generating memory-aware formal function specifications. Experiments show that iterative refinement substantially improves syntactic validity, while symbolic prover-based refutation significantly enhances correctness assessment by filtering false positives that LLM-only judges frequently accept. Our results demonstrate that combining neural generation with symbolic feedback provides an effective approach to formal specification synthesis for memory-safe systems software.
• Abstract（参考訳）: メモリ操作プログラムの形式的検証は、専門家によって書かれたメモリ状態をキャプチャする正確な機能仕様に依存している。 この要件は、大規模言語モデル(LLM)が、正確性を想定できない低レベルのシステムコードを生成するにつれて、大きなボトルネックとなっている。 スケーラブルな形式検証を実現するため,従来の検証パイプラインの中心となる複雑なループ不変量の合成を意図的に回避して,関数仕様生成にのみ焦点をあてる。 自然言語問題記述と関数シグネチャから,C言語プログラムのメモリ対応形式関数仕様を自動生成するニューラルシンボリックフレームワークを提案する。 パイプラインはまず、コンテキスト内学習を通じて候補仕様を生成し、その後、シンボリックプローバーと検証ツールチェーンのコンパイラ診断を使用して繰り返し洗練する。 特に、具体例で仕様の否定の証明を構築することで、候補仕様を検証し、妥当な仕様の機械検査による拒否を可能にする。 本稿では,メモリアウェアな形式関数仕様を生成するための200Cプログラミング問題のベンチマークであるLeetCode-C-Specを紹介する。 実験の結果,反復的改善は構文的妥当性を著しく向上させる一方で,記号的証明に基づく難読化は,LLMのみの判断者が頻繁に受け入れる偽陽性をフィルタリングすることにより,精度を著しく向上させることが示された。 この結果から,ニューラルネットワークとシンボルフィードバックを組み合わせることで,メモリセーフなシステムソフトウェアのための形式的仕様合成に有効なアプローチが得られた。

関連論文リスト

• CodeCircuit: Toward Inferring LLM-Generated Code Correctness via Attribution Graphs [13.488544043942495]
  本研究の目的は、コード生成中に論理的妥当性を予測可能な内部デオード可能な信号が、モデル内のニューラルダイナミクスで符号化されているかどうかを検討することである。 複雑な残留流を分解することにより,音の推論と論理的失敗を区別する構造的シグネチャを同定することを目的とする。 Python、C++、Javaでの分析では、固有の正当性信号が多様な構文で堅牢であることが確認されている。
  論文  参考訳（メタデータ） (2026-02-06T03:49:15Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  投機的復号化は、複数のドラフトトークンを並列に検証することにより、自動回帰言語モデル推論を加速する。 既存のスペーシフィケーション方式は主にトークン・バイ・トーケンの自己回帰復号化のために設計されている。 そこで本研究では,注目度,FFN,MoEを両立させるスパース検証フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-12-26T07:53:41Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  言語モデルの生成能力をプロセス検証器と組み合わせたテストタイムアルゴリズムは、新しい推論能力を引き出すための有望なレバーを提供する。 提案手法は, 理論的に根拠付きバックトラックを用いて, 検証誤差に対して, 確実な堅牢性を実現するための新しいプロセス誘導型テスト時間サンプリングアルゴリズムであるVGBを導入する。
  論文  参考訳（メタデータ） (2025-10-03T16:21:14Z)
• Position: Intelligent Coding Systems Should Write Programs with Justifications [9.304020701255093]
  これらのシステムは、コードを生成するだけでなく、モデル推論とユーザ理解を橋渡しする明確な一貫性のある正当化も生み出すべきだ、と私たちは主張する。 我々は, 正当性生成のためのニューロシンボリックなアプローチを提唱し, トレーニング中の行動とプログラムセマンティクスが神経表現によって豊かになるように, 象徴的制約を導出する。
  論文  参考訳（メタデータ） (2025-08-08T05:04:47Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
  本稿では,VeriFast で検証可能な C プログラムの仕様作成における OpenAI の GPT-4o モデルの有効性について検討する。 以上の結果から,GPT-4oで生成された仕様は機能的挙動を保っているが,検証に苦慮していることが明らかとなった。
  論文  参考訳（メタデータ） (2024-11-04T17:44:11Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。 次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)

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

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