論文の概要: 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（参考訳）: 記憶機能仕様のニューロ・シンボリック生成と検証
- 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のみの判断者が頻繁に受け入れる偽陽性をフィルタリングすることにより,精度を著しく向上させることが示された。
この結果から,ニューラルネットワークとシンボルフィードバックを組み合わせることで,メモリセーフなシステムソフトウェアのための形式的仕様合成に有効なアプローチが得られた。
関連論文リスト
- ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。
ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。
1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
論文 参考訳（メタデータ） (2026-07-01T09:58:59Z) - Weave of Formal Thought [51.56484100374058]
WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。
本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。
Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
論文 参考訳（メタデータ） (2026-06-24T15:58:11Z) - Agentic Separation Logic Specification Synthesis [4.177196802192322]
Spec-Agentは、大規模なC++で表現力のある、よく検証された仕様を合成するためのエージェントシステムである。
それぞれの関数に対して、Spec-Agentは静的解析とランタイムヒープトレースを使用して、適切なターゲット仕様言語を選択する。
数百万行のコードからなるオープンソースのC++上でSpec-Agentを評価する。
論文 参考訳（メタデータ） (2026-05-26T18:05:42Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Autoformalizing Memory Specifications with Agents [3.897906533095668]
本稿では,メモリチップ仕様をDRAMPyMLという形式表現にする方法を示す。
これはSystemVerilogアサーション、刺激、機能カバレッジの生成に使用できる。
ベンチマークデータセットであるDRAMBenchもリリースしています。
論文 参考訳（メタデータ） (2026-04-30T02:01:48Z) - How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
我々は,認知理論に触発された問題解決性に基づく新しい誤り分類法を導入する。
我々の分類学は、障害を構文、意味、解決可能な機能、解決不可能な機能タイプに分類する。
論文 参考訳（メタデータ） (2026-04-26T14:34:49Z) - Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study [0.0]
本稿では, 集団適応システム(CAS)におけるLCM生成適応マネージャのフィードバックに基づく自動検証について検討する。
ループにおける検証の主な課題は、実行時に生成されたコードの障害を検出する方法と、それをレポートする方法である。
この結果から,プログラムスキルを持たないドメインエキスパートが設計したシステムにおいて,フィードバック精度が信頼性の高いビブ符号化の主要な要因であることが示唆された。
論文 参考訳（メタデータ） (2026-04-16T10:58:03Z) - VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
自動JML仕様合成における古典的手法と急進的手法を比較した。
提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。
本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
論文 参考訳（メタデータ） (2026-03-31T22:12:15Z) - Understanding Contextual Recall in Transformers: How Finetuning Enables In-Context Reasoning over Pretraining Knowledge [50.009682083079205]
我々は,文脈的リコールが単独で事前学習から生じるかどうかを検討する。
ICL評価とは異なる暗黙的推論を必要とするタスクの微調整は、文脈的リコールの出現を誘発することを示す。
メカニカル・インサイト(メカニカル・インサイト)では,現実から文脈への遷移を再現するアテンションオンリー・トランスフォーマーの構成を導出する。
論文 参考訳（メタデータ） (2026-03-21T22:46:55Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。