論文の概要: VeriPy Source-Preserving Verification and Compatibility Checking for Python Components

• arxiv url: http://arxiv.org/abs/2610.02814v1
• Date: Fri, 02 Oct 2026 05:02:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-06 09:54:32.233862
• Title: VeriPy Source-Preserving Verification and Compatibility Checking for Python Components
• Title（参考訳）: PythonコンポーネントのVeriPyソースコード保存検証と互換性チェック
• Abstract要約: VeriPyは、ソースレベルの証明開発と機能検証と後方互換性を結びつける。 コードはhttps://github.com/astrio-labs/veripy.comで公開されている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Keeping a Python program and its formal guarantees aligned is a continuing maintenance problem. Specifications must describe the implementation that actually runs, and updates must preserve the behavior on which existing callers depend. VeriPy brings these obligations into a common workflow for annotated Python components. Developers and agents express contracts, invariants, and proof hooks as Python comments, then refine checked auxiliary lemmas using source-located diagnostics. Direct encoders produce Dafny or Lean artifacts while retaining admitted executable bodies and explicit models of their dependencies. A relational product checks whether an updated component still admits old inputs and preserves returned values and modeled exceptions. The resulting workflow connects source-level proof development with functional verification and backward compatibility, recording the assumptions under which each guarantee applies. The code is available at https://github.com/astrio-labs/veripy.
• Abstract（参考訳）: Pythonプログラムとその正式な保証を維持することは、継続的なメンテナンス問題である。 仕様は実際に実行される実装を記述する必要があり、更新は既存の呼び出し元が依存する振る舞いを保存する必要がある。 VeriPyは、アノテーション付きPythonコンポーネントの共通ワークフローにこれらの義務をもたらす。 開発者とエージェントは、Pythonコメントとしてコントラクト、不変性、証明フックを表現し、ソース位置診断を使用してチェックされた補助レムマを精査する。 直接エンコーダはDafnyやLeanのアーティファクトを生成し、承認された実行可能なボディと依存関係の明示的なモデルを保持します。 リレーショナル製品は、更新されたコンポーネントが古い入力をまだ受け入れているかどうかを確認し、返却された値とモデル化された例外を保存する。 結果として得られるワークフローは、ソースレベルの証明開発と機能検証と後方互換性を結びつけ、それぞれの保証が適用される仮定を記録する。 コードはhttps://github.com/astrio-labs/veripy.comで公開されている。

関連論文リスト

• Zero2Repo: Can Coding Agents Build Repositories from Scratch? [33.79367580283551]
  コーディングエージェントは、パッチをパッチするのではなく、ソフトウェアを構築するように求められている。 エージェントが製品要求文書、インターフェース契約、空のワークスペースを受信するベンチマークであるZero2Repoを紹介する。 タスクは言語に依存しないオーサリングパイプラインによって生成されます。
  論文  参考訳（メタデータ） (2026-09-29T14:10:23Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。 Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。 ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
  論文  参考訳（メタデータ） (2026-08-13T17:41:27Z)
• Kani: A Model Checker for Rust [3.019677299390329]
  KaniはRustのオープンソースモデルチェッカーである。 バグフィニング以外のバウンドモデルチェックをプッシュして、正確性を保証する。 KaniはプロダクションCIで大規模に運用されており、コード変更毎に16,000以上のハーネスが検証されている。
  論文  参考訳（メタデータ） (2026-07-01T22:05:33Z)
• Visual-to-Code Authoring, Tensor-Network Debugging, and Quantum-Circuit Inspection Tools in Python [51.892236819637354]
  ネットワークと量子回路は、接続性、指標、収縮順序、ゲート配置、測定、関連する設計選択に依存する構造体である。 コードよりも視覚的に推論しやすいことが多いが、Pythonでは頻繁に構築され、変換され、バックエンド固有のオブジェクトやコンパクトなシンボル式を通してチェックされる。 本稿では、サポート対象ネットワークの視覚的および構造的検査とトレーサム等価性を示すネットワークワーク・ビジュアライゼーション、ビジュアル・ツー・コードオーサリング、バックエンドコード生成、エクスポート、設計レベルの分析のための量子ネットワークワーク・エディター、クリアな回路レンダリング、検査および設計のための量子回路描画の3つの補完パッケージを提案する。
  論文  参考訳（メタデータ） (2026-06-07T18:01:31Z)
• The Path Matters: Learning a Token-Commitment Policy for Diffusion Language Models [52.93186090124315]
  トークンのコミットメントは、再利用可能なトレースステートポリシとして学ぶことができる、と私たちは主張する。 凍結拡散言語モデルのためにこのポリシーをインスタンス化する軽量プラグインコントローラであるTraceLockを紹介する。
  論文  参考訳（メタデータ） (2026-05-23T18:23:46Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。 本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。 その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
  論文  参考訳（メタデータ） (2025-03-03T01:55:20Z)
• UQpy v4.1: Uncertainty Quantification with Python [4.6405927770229]
  本稿では、UQpyのバージョン4で導入された最新の改善、Pythonによる不確実性定量化、ライブラリについて述べる。 最新バージョンでは、コードは最新のPythonコーディング規約に従って再構成された。 UQpyの堅牢性を改善するために、ソフトウェアエンジニアリングのベストプラクティスが採用された。
  論文  参考訳（メタデータ） (2023-05-16T16:11:04Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。 我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2022-03-15T08:25:08Z)
• Latte: Cross-framework Python Package for Evaluation of Latent-Based Generative Models [65.51757376525798]
  Latteは、潜伏型生成モデルを評価するためのPythonライブラリである。 LatteはPyTorchと/Kerasの両方と互換性があり、関数型APIとモジュール型APIの両方を提供する。
  論文  参考訳（メタデータ） (2021-12-20T16:00:28Z)

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

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