論文の概要: Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation

• arxiv url: http://arxiv.org/abs/2609.31687v1
• Date: Wed, 16 Sep 2026 19:01:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-08 13:49:08.920202
• Title: Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation
• Title（参考訳）: LLM生成ACSL契約と決定論的ドライバ生成を用いたPETScとCIVLの検証
• Abstract要約: PETScのような数値ライブラリは、間違った結果にコストがかかる科学や工学のアプリケーションで広く使われている。 課題の1つは、専門家が仕様を手書きし、手動で検証ツールを適用する必要があることである。 本稿では,LLMを限定的な設定で使用して,関数のドキュメントから人間に認識可能なACSL契約を生成する手法を提案する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Parallel numerical libraries such as PETSc are widely used in science and engineering applications where wrong results can have costly consequences. Despite this, numerical libraries are rarely formally verified. One of the challenges is the need for an expert to hand-write a specification and manually apply a verification tool, often requiring the development of a harness or driver, all of which can contain additional bugs that lead to false positives or false negatives during verification. With recent advancements in large language models (LLMs), it is tempting to generate such drivers and reference models automatically, but one-shot generation based on a simple prompt is brittle and leads to additional unverified code that needs to be audited. In this paper, we present an approach to use LLMs in a limited setting to generate a small, human-certifiable ACSL contract from the function's documentation, combined with a deterministic toolchain that supports a restricted ACSL profile and generates a driver that uses the CIVL verifier to check the implementation against the contract and, when available, an existing reference model. We demonstrate the pipeline end-to-end on three PETSc functions: MatAXPY (reference model already exists), MatAYPX (no reference model, so the certified contract is the sole oracle), and the non-compressing mode of MatFilter (no reference model, with more complex, conditional behavior). With this pipeline, we were able to discover a bug in PETSc's MatAYPX function that was previously undiscovered and had been present in the code since 1997.
• Abstract（参考訳）: PETScのような並列数値ライブラリは、間違った結果にコストがかかる科学や工学のアプリケーションで広く使われている。 それにもかかわらず、数値ライブラリーが正式に認証されることはめったにない。 課題の1つは、専門家が仕様を手書きし、手動で検証ツールを適用する必要があることである。 近年の大規模言語モデル(LLM)の進歩により、そのようなドライバや参照モデルを自動的に生成する傾向にあるが、単純なプロンプトに基づいたワンショット生成は不安定であり、監査が必要な不確実なコードに繋がる。 本稿では,制限されたACSLプロファイルをサポートする決定論的ツールチェーンと組み合わせ,CIVL検証器を用いて契約に対する実装を確認し,利用可能であれば既存の参照モデルを生成する。 MatAXPY(参照モデルはすでに存在する)、MtAYPX(参照モデルがないので、認定契約は唯一のオラクルである)、MtFilter(参照モデルがなく、より複雑な条件付き動作)の非圧縮モードである。 このパイプラインでPETScのMateAYPX関数のバグを発見しました。

関連論文リスト

• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMは、オフチェーン実行の正しさを保証するゼロ知識を生成する。 微妙な実装上のバグは、意味的に欠陥のある状態を証明する有効な証明につながる可能性がある。 SMTソルバによる形式検証は、これを防止できるが、仕様によってボトルネックとなる。 Rustから実行可能なPython/Z3検証モデルを合成するフレームワークであるVeri Synthを提案する。
  論文  参考訳（メタデータ） (2026-07-22T06:20:36Z)
• LM2Alloy: Investigating LLM-Generated Formal Specifications for Automated Test Derivation in Production Software [0.9023847175654603]
  本稿では,Large Language Models (LLMs) を用いた合金仕様作成のための探索的研究について述べる。 Flipperは機能フラグ管理システムであり、Cerberusはデータ検証ライブラリである。
  論文  参考訳（メタデータ） (2026-07-20T22:41:55Z)
• Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering [40.048798975817924]
  バイブコーディングは高速で、低臨界のコンシューマソフトウェアには適しています。 DO-178C、IEC 61508、ISO 26262によって管理される安全クリティカルなシステムでは、認証への道は提供されない。 フォーマルな検証を通じてビブコーディングをガイドするクローズドループパイプラインであるForgeを紹介します。
  論文  参考訳（メタデータ） (2026-06-21T10:01:45Z)
• ChipMATE: Multi-Agent Training via Reinforcement Learning for Enhanced RTL Generation [55.947962672433675]
  ChipMATEは、RTL生成のための最初の自己学習型マルチエージェントフレームワークである。 ChipMATEは産業的な実践に触発され、VerilogエージェントとPythonのリファレンスモデルエージェントをペアにし、相互に出力を検証する。 ChipMATEは、VerilogEval V2で75.0%と80.1%パス@1を4Bと9Bベースモデルで達成している。
  論文  参考訳（メタデータ） (2026-05-13T01:04:21Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• SpecPylot: Python Specification Generation using Large Language Models [1.0026496861838448]
  SpecPylotは、Pythonプログラムの実行可能な仕様をアイコン抽出アノテーションとして合成するPythonツールである。 このツールはLSMに頼って候補契約を提案し、クロスヘアを使って検証する。 全体としては、SpecPylotはほとんどのプログラムでクロスヘア互換のコントラクトを生成することができることを示している。
  論文  参考訳（メタデータ） (2026-04-17T08:53:02Z)
• Can Large Language Models Implement Agent-Based Models? An ODD-based Replication Study [0.6821122205224714]
  大規模言語モデル(LLM)は、テキスト記述から非自明な実行可能なコードを合成できるようになった。 LLMは、複製、検証、検証をサポートする方法で、標準化された仕様からエージェントベースのモデルを確実に実装できますか? 制御されたODD-to-code翻訳タスクにおいて17の現代LLMを評価する。
  論文  参考訳（メタデータ） (2026-02-08T19:56:20Z)
• Get my drift? Catching LLM Task Drift with Activation Deltas [55.75645403965326]
  タスクドリフトは攻撃者がデータを流出させたり、LLMの出力に影響を与えたりすることを可能にする。 そこで, 簡易線形分類器は, 分布外テストセット上で, ほぼ完全なLOC AUCでドリフトを検出することができることを示す。 このアプローチは、プロンプトインジェクション、ジェイルブレイク、悪意のある指示など、目に見えないタスクドメインに対して驚くほどうまく一般化する。
  論文  参考訳（メタデータ） (2024-06-02T16:53:21Z)

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

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