論文の概要: The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK
- arxiv url: http://arxiv.org/abs/2607.14340v1
- Date: Wed, 15 Jul 2026 20:09:05 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-17 17:01:32.910977
- Title: The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK
- Title（参考訳）: Ada/SPARKのAIコーディングエージェントによる検証済みのセキュリティソフトウェア
- Authors: Tobias Philipp,
- Abstract要約: 検証者主導のループにおいて、AIエージェントは古典的および後量子暗号、TLS 1.3、IKEv2、X.509、マトリックスクライアントにまたがるAda/SPARKのベアメタルセキュリティソフトウェアを書いて検証した。
GNATproveは49,280の証明義務を解除し、選択されたプリミティブに対して機能的正当性を確立し、残りのプリミティブに対して実行時のエラーがないことを証明した。
それぞれのレイヤが障害をキャッチし,中心的な教訓を引き出す方法を報告します。エージェントが確立するために信頼できるものは,そのフィードバックの強さに縛られているのです。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: AI coding agents produce code faster than humans can review it. In our approach, the prover is the judge of whether the code is correct. Under a verifier-driven loop, AI agents wrote and verified bare-metal security software in Ada/SPARK spanning classical and post-quantum cryptography, TLS 1.3, IKEv2, X.509, and a Matrix client. GNATprove discharged 49,280 proof obligations, established functional correctness for selected primitives, and proved the absence of run-time errors for the rest, at roughly 20-40 times lower supervision cost than comparable hand verification. GNATprove alone was insufficient: some defects could not be detected and were resolved using known-answer tests, interoperability, or human review of specifications. Given weak checks, the agent tried to bypass them and reported success. We report where each layer caught faults and draw the central lesson: what an agent can be trusted to establish is bounded by the strength of its feedback.
- Abstract（参考訳）: AIコーディングエージェントは、人間がレビューできるよりも早くコードを生成する。
我々のアプローチでは、証明者はコードが正しいかどうかを判断する。
検証者主導のループの下で、AIエージェントは古典的および後量子暗号、TLS 1.3、IKEv2、X.509、マトリックスクライアントにまたがるAda/SPARKのベアメタルセキュリティソフトウェアを書いて検証した。
GNATproveは49,280の証明義務を解除し、選択されたプリミティブに対して機能的正当性を確立し、残りのプリミティブに対して実行時のエラーがないことを証明した。
GNATproveだけでは不十分で、いくつかの欠陥は検出できず、既知の回答テスト、相互運用性、仕様の人為的レビューを使用して解決された。
弱めのチェックを受け、エージェントは彼らをバイパスしようと試み、成功を報告した。
それぞれのレイヤが障害をキャッチし,中心的な教訓を引き出す方法を報告します。エージェントが確立するために信頼できるものは,そのフィードバックの強さに縛られているのです。
関連論文リスト
- Is Agent Code Less Maintainable Than Human Code? [17.226150835020146]
保守環境において,エージェントコードがヒューマンコードとどのように比較されるかを検討する。
エージェントは人的コードに比べてエージェントコード構築時のタスクの解決に効果が低いことがわかった。
論文 参考訳（メタデータ） (2026-06-19T23:56:14Z) - Code-Augur: Agentic Vulnerability Detection via Specification Inference [8.217845898392293]
自律的なLLMエージェントによる監査が、ソフトウェアの重大な脆弱性を明らかにしている。
本稿では,エージェントの暗黙的な仮定をセキュリティ仕様として明示的に公開する,セキュリティ仕様優先のパラダイムを提案する。
エージェント脆弱性検出のための新しいハーネスであるCode-Augurにおける我々のアプローチを実現する。
論文 参考訳（メタデータ） (2026-06-17T02:32:45Z) - Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization [26.123396123145415]
LLMエージェントが非公式なプログラミング問題を忠実な形式仕様に変換することができるかどうか、仕様自動書式化について検討する。
Codeforces問題から派生した581の仕様記述タスクのベンチマークであるVerus-SpecBenchを紹介する。
フェールモードの解析は、モデル生成仕様が重要な入力仮定を受け入れ、誤った出力を受け入れ、有効な仕様を拒否できることを示している。
論文 参考訳（メタデータ） (2026-05-26T02:12:48Z) - Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。
個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。
構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
論文 参考訳（メタデータ） (2026-05-15T17:08:27Z) - SecureForge: Finding and Preventing Vulnerabilities in LLM-Generated Code via Prompt Optimization [61.91729298584227]
SecureForgeは、フロンティアモデルのセキュリティリスクを監査し、監査インフォームされたセキュアなシステムプロンプトを生成する自動化パイプラインである。
SecureForgeは、まず静的に検出可能な脆弱性を生成する良性プロンプトを特定し、その後、さまざまなシナリオの大規模な合成プロンプトコーパスに増幅する。
フロンティアモデルでは、SecureForgeは、ユニットテストの成功と出力セキュリティの両方において統計的に有意な改善をもたらし、出力脆弱性は最大48%削減された。
論文 参考訳（メタデータ） (2026-05-08T18:40:47Z) - Synthesizing Multi-Agent Harnesses for Vulnerability Discovery [8.518689779459974]
LLMエージェントは、人間の監査官や自動ファジッターが何十年も見逃していた、真のセキュリティ脆弱性を見つけ始めている。
実際には、作業は複数のエージェントに分割され、ハーネスによってワイヤリングされる。どの役割が存在するかを修正するプログラム、どのように情報を渡すか、どのツールを呼び出すか、リトライがどのように調整されるかである。
AgentFlowは、エージェントの役割、プロンプト、ツール、通信トポロジ、調整プロトコルを共同でカバーする型付きグラフDSLで、両方の制限に対処する。
論文 参考訳（メタデータ） (2026-04-22T17:27:40Z) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。
我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
論文 参考訳（メタデータ） (2026-01-30T08:29:01Z) - Holistic Agent Leaderboard: The Missing Infrastructure for AI Agent Evaluation [87.47155146067962]
数百のタスクで並列評価をオーケストレーションする,標準化された評価ハーネスを提供する。
モデル、足場、ベンチマークにまたがる3次元解析を行う。
私たちの分析では、ほとんどのランで精度を低下させる高い推論努力など、驚くべき洞察が示されています。
論文 参考訳（メタデータ） (2025-10-13T22:22:28Z) - VulAgent: Hypothesis-Validation based Multi-Agent Vulnerability Detection [55.957275374847484]
VulAgentは仮説検証に基づくマルチエージェント脆弱性検出フレームワークである。
セマンティクスに敏感なマルチビュー検出パイプラインを実装しており、それぞれが特定の分析の観点から一致している。
平均して、VulAgentは全体的な精度を6.6%改善し、脆弱性のある固定されたコードペアの正確な識別率を最大450%向上させ、偽陽性率を約36%削減する。
論文 参考訳（メタデータ） (2025-09-15T02:25:38Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z) - CodeAgent: Autonomous Communicative Agents for Code Review [12.163258651539236]
コードレビュー自動化のための新しいマルチエージェント大規模言語モデル(LLM)システムであるツールを紹介する。
CodeAgentは、すべてのエージェントのコントリビューションが初期レビュー問題に対処するように、監督エージェントであるQA-Checkerを組み込んでいる。
結果はCodeAgentの有効性を実証し、コードレビュー自動化の新たな最先端に寄与している。
論文 参考訳（メタデータ） (2024-02-03T14:43:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。