論文の概要: HoldSpec: A Machine-Checked Model and Conformance Suite for the Payment Authorization Hold Lifecycle

• arxiv url: http://arxiv.org/abs/2610.14419v1
• Date: Sat, 10 Oct 2026 00:34:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-20 21:42:10.300631
• Title: HoldSpec: A Machine-Checked Model and Conformance Suite for the Payment Authorization Hold Lifecycle
• Title（参考訳）: HoldSpec: Payment Authorization Hold Lifecycleのための機械学習モデルとコンフォーマンススイート
• Abstract要約: 私たちは、すべての支払いサービスプロバイダがわずかに異なる実装をしており、いずれのサービスも正式な仕様を定めていない、というビジネスロジックに注目します。 StripeとAdyenが公開したドキュメントから構築した8つのセーフティ不変性と6つのプロファイル上の3つのライブ性特性を確認します。 2つのプロバイダ間で同じスイートを実行すると、比較は検索に変わり、2つのドキュメントセットを分離するために短い実行可能証人を返す。
• 参考スコア（独自算出の注目度）: 1.350933217151331
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: When a merchant authorizes a card and captures the funds later, the money sits in a state that neither party fully controls: held on the cardholder's account, not yet taken, and due to lapse on a deadline set by the card network. What a merchant may do to that hold, capture part of it, capture again, void it, raise it, let it expire, is business logic that every payment service provider implements slightly differently and none of them specifies formally. We give the lifecycle a state machine in TLA+, parameterized by a provider capability profile, and check eight safety invariants and three liveness properties over 6 profiles, five of them built from Stripe's and Adyen's published documentation. From the same machine we generate a conformance suite that runs black-box against a provider API. Against 61 seeded defects that are distinguishishable from a correct implementation, the generated suite detects 100%, where random sequences with the same call budget reach 56% and a hand-written integration suite reaches 69%; random sequences given ten times the budget still reach only 67%. Running the same suite between two providers turns the comparison into a search, and it returns short executable witnesses for divergences the two documentation sets imply but neither states, including one that breaks the common assumption that a single adapter interface can sit over both, because closing a hold and releasing its remainder is a capture on one provider and a cancel on the other. We report what we could not do: no provider sandbox credentials were available, so every result here concerns documented behavior, and the suite that would test the providers themselves is part of what we release.
• Abstract（参考訳）: 商人がカードを許可し、後に資金を掴むと、その金は、カード所有者の口座に保持され、カードネットワークが設定した期限が経過した状態に置かれる。 そのホールドに対して商人がやるべきことは、そのホールドをキャプチャし、その一部をキャプチャし、再びキャプチャし、それを無効にし、それを無効にし、期限切れにすることです。 TLA+のステートマシンをライフサイクルに提供し、プロバイダの機能プロファイルによってパラメータ化され、StripeとAdyenが公開したドキュメントから構築された8つの安全不変性と3つのライブプロパティをチェックします。 同じマシンから、プロバイダAPIに対してブラックボックスを実行するコンフォーマンススイートを生成します。 正しい実装と区別可能な61個のシードされた欠陥に対して、生成されたスイートは100%を検出し、同じ呼び出し予算を持つランダムシーケンスが56%に達し、手書きの統合スイートが69%に達した。 2つのプロバイダ間で同じスイートを実行すると、比較結果が検索に変わり、2つのドキュメントセットを分離するための短い実行可能証人を返すが、どちらの状態も、ひとつのアダプタインターフェースが両方に置かれるという一般的な仮定を破るものではない。 プロバイダのサンドボックス認証が利用できなかったため、すべての結果はドキュメント化された振る舞いに関するもので、プロバイダ自体をテストするスイートは、当社のリリースの一部です。

関連論文リスト

• SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs? [39.004582663385364]
  Benchprooferは、既知の正しいパッチでコーディングタスクを正式に認証されたパイプラインに変換するパイプラインです。 SWE-bench Verified に適用すると SWE-Proof が得られる。
  論文  参考訳（メタデータ） (2026-09-18T01:16:53Z)
• IBIB: A Protocol for Measuring Enterprise AI Systems by Serving Route, Not Model Identifier [0.0]
  監査された18のベンチマークはすべて、広告付きモデルの識別子をスコア付けする。 ゴールドブラインド機能バインディングプレフライトは、どのタスクが到達する前に、ルートが評価契約を実行可能であることを確認する。 信頼性非包括的なファーストパススコアリングルールは、有効性を保ちながらスコアの失敗を維持する。
  論文  参考訳（メタデータ） (2026-09-09T17:31:29Z)
• AgentProv: Auditing Agentic LLM API Providers via Tool-use Policy Probes [38.37599802008238]
  商用LLM APIは特定の基盤モデルを宣伝するが、提供されたバックボーンは静かに代用され、定量化され、あるいはラップされることがある。 既存の監査はすべて、テキスト出力チャネルからバックボーンアイデンティティを決定する。 本稿では,AgentProv(AgentProv)について紹介する。
  論文  参考訳（メタデータ） (2026-08-30T08:22:12Z)
• From Traceability to Justifiability: Accountability Structures in Agentic Software Engineering [0.0]
  公開資料のみから、AIレコードがクレームを表現できるかどうか、宣言された場所を保持できるかどうかを測定する。 188個の二重グレード細胞で、デフォルトレコードが行動システムのコンテンツアイデンティティを出力するプラットフォームは見つからなかった。 計器は、パイプラインが発行した排気のみからの保証深度を計算し、宣言された深さと比較する。
  論文  参考訳（メタデータ） (2026-08-21T16:45:00Z)
• KeyPooling: Measuring Where LLM API Relay Paths Collapse Prompt Cache Isolation [53.952294884822955]
  大規模言語モデル(LLM)APIは、顧客の認証を別々に行うが、多くの場合、共有プロバイダ認証を通じて要求を転送する。 KeyPoolingは、キャッシュのルックアップと書き込みを通じて顧客のアイデンティティをトレースする測定方法である。 すべての顧客がプロバイダ強化されたドメインに入る必要があります。
  論文  参考訳（メタデータ） (2026-08-18T08:12:34Z)
• Where Accountability Lives: Mapping Human Responsibility to Workflow Artifacts in Agentic Software Development [0.0]
  コーディングエージェントの作者、プルリクエストのオープン、プロダクションリポジトリ内のプッシュコード。 アーティファクトを残すワークフローイベント、エージェントによるコーディングツール4つ、および7つのプロバイダによるポリシー文書18つについて、それぞれについて読んでいます。 あるプロバイダは、タスクを割り当てた開発者が結果のプルリクエストを承認することを禁じる。別のプロバイダは、設定されたリスクしきい値以下でプルリクエストを承認し、レビューを無効にできるエージェントを文書化する。 我々は、強制的、助言的、欠落した検証の通常の3方向の区別をグリッドに置き換え、メカニズムがチェックを誰が実行したかで補完するかどうかを区別する。
  論文  参考訳（メタデータ） (2026-08-16T11:11:04Z)
• Coding Agents as Test-Suite Auditors: Finding What Official Suites Miss While Approaching What They Catch [47.836680625916266]
  テストスイート監査官として機能する市販のコーディングエージェントは、どちらも、公式スイートが見逃すものを公開するために、敵対的なテストスイートを構築します。 認証チェーンは、各エージェントフラッグされた申請が、公式の裁判官に頼らずに、真にバグだらけであるか否かを判定する。 Codeforceは、利用可能なオフィシャルスイートを持たない問題に対して、同じテストビルディングメソッドを使用して、テストされた入力予算毎に5つの再生ベースラインを導出する。
  論文  参考訳（メタデータ） (2026-08-03T05:24:03Z)
• Turning Interaction History into Execution State: A Runtime Layer for Long-Horizon Coding Agents [48.967927222079965]
  Ledgerは、エージェントの完了したインタラクションを明示的な実行状態に蒸留するランタイム層である。 Ledgerはこの状態をオンライン実行台帳に保持し、各ステップの2つのバウンダリに適用される。 500のSWE-bench検証インスタンス全体で、LedgerはPass@1を56.2%から64.2%に、GPT-5 miniを75.8%から81.0%に、MiniMax M2.5を81.0%に引き上げている。
  論文  参考訳（メタデータ） (2026-08-01T18:25:00Z)
• A Decision-Centered Reference Architecture for Trustworthy Agentic Commerce [0.0]
  エージェントコマースは、エージェントショッピングを、ポリシーを解釈し、チェックアウトを準備し、トランザクション対応言語を生成し、委譲された支払い権限の下で行動するソフトウェアエージェントに拡張する。 本研究では,標準エンベロープを中心に構築されたプロトコルに依存しないアーキテクチャ,保護された依存性と結果,Ed25519あるいはHMAC認証,ライブ要求リバインド,7軸生成ゲート,実行時依存性再検証,セマンティック不変量について述べる。
  論文  参考訳（メタデータ） (2026-07-20T08:33:31Z)
• Lingering Authority: Revocable Resource-and-Effect Capabilities for Coding Agents [0.0]
  PortICOは、プランナーに露出する機能のリファレンスモニターである。 明示的なタスクコントラクトを初期機能にコンパイルし、ルールを付与し、信頼できるクロージャ述語、グローバルな否定ルールを付与する。
  論文  参考訳（メタデータ） (2026-06-21T13:52:37Z)

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

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