論文の概要: Verification Modulo Tested Library Contracts

• arxiv url: http://arxiv.org/abs/2604.15533v1
• Date: Thu, 16 Apr 2026 21:27:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-20 22:00:19.655533
• Title: Verification Modulo Tested Library Contracts
• Title（参考訳）: 検証モデュロ試験ライブラリ契約
• Authors: Abhishek Uppar, Omar Muhammad, Sumanth Prabhu, Deepak D'Souza, Madhusudan P, Adithya Murali,
• Abstract要約: 図書館契約の統一化に関する問題点について考察する。 クライアントが使用するライブラリメソッドのモジュラーコントラクトの合成としてこの問題を定式化する。 また、Emphcontextual Contractと呼ばれるメソッドコントラクトの新しい形式についても検討する。
• 参考スコア（独自算出の注目度）: 1.031361622440068
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We consider the problem of \emph{verification modulo tested library contracts} as a step towards automating the verification of client programs that use complex libraries. We formulate this problem as the synthesis of modular contracts for the library methods used by the client that are adequate to prove the client correct, and that also pass the scrutiny of a testing engine that tests the library against these contracts. We also consider a new form of method contracts called \emph{contextual contracts} that arise in this setting that hold in the context of the client program, and can often be simpler and easier to infer than classical modular contracts. We provide a counterexample-guided learning framework to solve this problem, in which the synthesizer interacts with a constraint solver as well as the testing engine in order to infer adequate modular/contextual method contracts and inductive invariants for the client. The main synthesis engines we use are generalizing CHC solvers that are realized using ICE learning algorithms. We realize this framework in a tool called \vmtlc and show its efficacy on benchmarks where clients call large libraries.
• Abstract（参考訳）: 複雑なライブラリを利用するクライアントプログラムの検証を自動化するためのステップとして, \emph{verification modulo test Library Contract} という問題を考える。 この問題は、クライアントが使用するライブラリメソッドのモジュール化されたコントラクトの合成として定式化し、クライアントが正しいことを証明し、これらのコントラクトに対してライブラリをテストするテストエンジンの精査をパスする。 また、クライアントプログラムのコンテキストに保持されるこの設定で生じる「emph{contextual Contract}」と呼ばれるメソッドコントラクトの新しい形式についても検討しています。 この問題を解決するための逆例誘導学習フレームワークを提供する。このフレームワークでは、シンセサイザーが制約解決器やテストエンジンと相互作用し、適切なモジュール/コンテキストのメソッド契約やクライアントの帰納的不変性を推論する。 私たちが使用している主要な合成エンジンは、ICE学習アルゴリズムを用いて実現されたCHCソルバの一般化です。 このフレームワークを \vmtlc というツールで実現し,クライアントが大規模ライブラリをコールするベンチマークで有効性を示す。

関連論文リスト

• An Agentic Evaluation Framework for AI-Generated Scientific Code in PETSc [7.236134946837382]
  petscagent-benchはエージェント評価エージェントのパラダイムに基づいて構築されたエージェントフレームワークである。 正確性、パフォーマンス、コード品質、アルゴリズムの適切性、ライブラリ固有の規約の5つの評価カテゴリで14評価パイプラインを編成する。 本フレームワークは,HPC用PETScライブラリを用いて,現実的な問題のベンチマークスイート上で実演する。
  論文  参考訳（メタデータ） (2026-03-16T22:46:10Z)
• IMMACULATE: A Practical LLM Auditing Framework via Verifiable Computation [49.796717294455796]
  経済的なモチベーションのある逸脱を検出するための実践的な監査フレームワークIMMACULATEを提案する。 IMMACULATEは、検証可能な計算を用いて少数のリクエストを選択的に監査し、暗号オーバーヘッドを償却しながら強力な検出保証を達成する。
  論文  参考訳（メタデータ） (2026-02-26T07:21:02Z)
• Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
  PACTは、プログラムアセスメントおよび契約順応評価フレームワークである。 契約違反に焦点を当てた包括的なテストスーツコーパスを提供する。 様々なプロンプト条件下でのコード生成の体系的解析を可能にする。
  論文  参考訳（メタデータ） (2025-10-14T01:12:37Z)
• Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
  大言語モデル(LLM)は、単純なテキストジェネレータから、検索強化、ツール呼び出し、マルチターンインタラクションを統合する複雑なソフトウェアシステムへと進化してきた。 その固有の非決定主義、ダイナミズム、文脈依存は品質保証に根本的な課題をもたらす。 本稿では,LLMアプリケーションを3層アーキテクチャに分解する: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, textbftextitLLM Inference Core。
  論文  参考訳（メタデータ） (2025-08-28T13:00:28Z)
• Client--Library Compatibility Testing with API Interaction Snapshots [6.2272693929051295]
  動作の破壊的変更(BBC)は、コンパイル時に検出されることなく、クライアントアプリケーションを静かに破壊することができる。 クライアント側の従来の回帰テストは、しばしばそのようなBBCを検出するのに失敗する。 本稿では,既存のクライアントテストを活用するクライアント-ライブラリ互換性テストに対する新しいアプローチを提案する。
  論文  参考訳（メタデータ） (2025-07-28T13:22:19Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。 ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。 我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。 我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。 本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。 その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
  論文  参考訳（メタデータ） (2025-03-03T01:55:20Z)
• Commit0: Library Generation from Scratch [77.38414688148006]
  Commit0は、AIエージェントにスクラッチからライブラリを書くよう促すベンチマークである。 エージェントには、ライブラリのAPIを概説する仕様文書と、インタラクティブなユニットテストスイートが提供されている。 Commit0はまた、モデルが生成したコードに対して静的解析と実行フィードバックを受け取る、インタラクティブな環境も提供する。
  論文  参考訳（メタデータ） (2024-12-02T18:11:30Z)
• Lightweight Syntactic API Usage Analysis with UCov [0.0]
  本稿では,ライブラリメンテナのAPIによるインタラクション理解を支援するための,新しい概念フレームワークを提案する。 これらのカスタマイズ可能なモデルにより、ライブラリメンテナはリリース前に設計を改善することができ、進化中の摩擦を減らすことができる。 我々は,これらのモデルを新しいツールUCovに実装し,多様なインタラクションスタイルを示す3つのライブラリ上でその能力を実証する。
  論文  参考訳（メタデータ） (2024-02-19T10:33:41Z)
• ConstraintChecker: A Plugin for Large Language Models to Reason on Commonsense Knowledge Bases [53.29427395419317]
  コモンセンス知識ベース(CSKB)に対する推論は,新しいコモンセンス知識を取得する方法として検討されてきた。 我々は**ConstraintChecker*を提案します。
  論文  参考訳（メタデータ） (2024-01-25T08:03:38Z)

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

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