論文の概要: Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study
- arxiv url: http://arxiv.org/abs/2608.18822v1
- Date: Wed, 19 Aug 2026 11:23:33 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-20 20:13:55.38402
- Title: Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study
- Title（参考訳）: ドリフトイザベル開発における契約レスキュー : ダブルタンクケーススタディ
- Abstract要約: 大規模言語モデルは対話型定理証明器を提案することができるが、成功したビルドは、周囲の検証タスクが保存されていることを示すものではない。
サンプルデータ二重タンクコントローラのイザベル開発においてこの問題について検討する。
作業は9つの理論と10の未完成の義務から始まり、謝罪なしに16の理論的な構築へと成長し、オープ、公理化、またはオラクルの使用を追加し、23の安定状態と36の壊れた証明状態を蓄積した。
- 参考スコア（独自算出の注目度）: 5.286470899048593
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models can propose proofs for interactive theorem provers, but a successful build does not show the surrounding verification task was preserved. We study this problem in an Isabelle development of a sampled-data double-tank controller. The work began with nine theories and ten unfinished obligations, grew to a 16-theory build without sorry, oops, added axiomatisation, or oracle use, and accumulated 23 stable and 36 broken proof states. A retrospective audit found material changes in 16 of the 100 original declarations, including a weakened end-to-end assurance theorem that assumed three of the four requirements in its conclusion. We used CAPRI, a contract-aware proof-repair tool, to govern a reconstruction by combining Isabelle acceptance with an independent check of repository changes against machine-readable edit contracts. The reconstruction discharged all ten scoped obligations within the original nine-theory structure. A secondary replay by a co-author reproduced the R10 build, contract checks, control tests, and principal audit findings; independent replication remains future work. Operational end-to-end verification remains incomplete: we still need to connect operational executions to the reconstructed quantitative trace contract, a task requiring an extended contract.
- Abstract（参考訳）: 大規模言語モデルは、対話型定理証明器の証明を提案できるが、成功したビルドは、周囲の検証タスクが保存されたことを示すものではない。
サンプルデータ二重タンクコントローラのイザベル開発においてこの問題について検討する。
研究は9つの理論と10の未完成の義務から始まり、謝罪なしに16の理論的な構築へと成長し、オープ、公理化、またはオラクルの使用を追加し、23の安定状態と36の壊れた証明状態が蓄積された。
ふりかえりの監査では、100の宣言のうち16の物質的変化が発見され、その中には、その結論の4つの要件のうち3つを前提とした、エンドツーエンドの保証定理の弱体化が含まれていた。
我々は、Isabelleの受け入れと、マシン可読な編集契約に対するリポジトリ変更の独立したチェックを組み合わせることで、再構築を管理するために、コントラクト対応の証明修復ツールであるCAPRIを使用した。
再建は、元々の9つの理論構造の中で10の範囲の義務を全て解除した。
共著者による2度目のリプレイでは、R10ビルド、コントラクトチェック、コントロールテスト、主要な監査結果が再現されている。
運用実行を、拡張されたコントラクトを必要とするタスクである、再構築された量的トレースコントラクトに接続する必要があります。
関連論文リスト
- Recoverability as a System Primitive for Long-Horizon AI Agents [5.008310199603767]
再利用を明示的な決定とするシステムプリミティブとして,リカバリビリティを導入する。
4つの決定論的ファイルと20のペアファイルの課題は、正確な復元と完了が許可されていない開始点を隠蔽できることを示している。
論文 参考訳（メタデータ） (2026-09-12T02:54:33Z) - CAPRI: Contract-Aware Proof Repair for Isabelle [5.286470899048593]
イザベルのビルドは、提出された理論が受け入れられていることを保証するが、LLMが開発者によって承認されたものだけを変更したわけではない。
本稿では,Isabelleが証明を確認し,独立したチェッカーが機械可読編集契約を強制する,契約対応の修復ワークフローであるCAPRIを紹介する。
論文 参考訳（メタデータ） (2026-08-13T16:43:44Z) - Independent Patch Verification for Coding Agents with a Bidirectional Reconstruct-and-Verify Framework [49.16055123488827]
大規模言語モデルを利用したコーディングエージェントは、バグレポートから直接コードパッチを生成することができる。
報告された問題を真に解決するかどうかを独立に検証するメカニズムは存在しない。
本稿では,RETRACE をトレーニング不要なポストジェネレーション検証フレームワークとして提案する。
論文 参考訳（メタデータ） (2026-08-09T22:59:13Z) - From Trajectories to Evidence: Auditable Experimental Records for Industrial Research Agents [47.678562263387214]
研究エージェントは、産業レコメンデーション設定において、多段階の機械学習実験をますます実施している。
生成されたアーティファクトは、サポートされないか、不完全かもしれないし、実行されたラウンドは無効かもしれないし、あるいは廃止されるかもしれないし、後の修正は、以前の発見を曖昧にするかもしれない。
本稿では,連続的アーティファクトのバウンダリ検証と実行後のクレーム資格を結合するエビデンス・グラウンド・フレームワークを提案する。
論文 参考訳（メタデータ） (2026-08-05T13:37:38Z) - Change2Task: From Repository Changes to Executable Coding Agent Tasks and Environments [46.958911818255565]
Change2Taskは、統合されたプルリクエストを、同じリポジトリの健全なモダンなリビジョンに関する検証されたタスクに変換する。
歴史的証拠を進化したコードと整合させ、パッチリバーサル、コードマッピング、エージェント再構築を通じてタスク状態を再構築する。
本システムは,バグフィックス,機能追加,テスト生成,アプリケーションプログラミングインタフェースのマイグレーション,セキュリティ修復という,広く普及している5つのプログラミングエージェントタスクファミリを通じて評価する。
論文 参考訳（メタデータ） (2026-07-30T17:44:31Z) - Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair [36.56438114281786]
正しいパッチの発見と保持、検証、提出のギャップについて検討する。
我々はエビデンスバウンド型ループ契約を導出し、その機械的に強制可能なサブセットを参照実装でインスタンス化する。
論文 参考訳（メタデータ） (2026-07-27T16:05:23Z) - From Prompts to Contracts: Harness Engineering for Auditable Enterprise LLM Agents [0.24554686192257424]
製品化は、ソースバウンダリ、エンティティルーティング、回答コントラクト、再現可能なトレースの要件を追加します。
本稿では,このパターンをトレース可能な監査可能なLLMエージェントアーキテクチャに再構成するハーネスエンジニアリング手法を提案する。
韓国の5つの企業グループの公開データスライスでインスタンス化し、3つの研究課題を評価する。
論文 参考訳（メタデータ） (2026-07-09T01:08:33Z) - AuditWeave: A Tamper-Evident, Auditor-Navigable Evidence Layer for AI-Assisted and Data-Transformation Workflows [0.0]
AuditWeaveは、AIアシストとデータ変換のステップを1つのハッシュチェーンの台帳に記録する軽量Pythonライブラリである。
本稿では,参照実装におけるオーバヘッド,拡張性,タンパー検出の正確さを設計し,評価する。
論文 参考訳（メタデータ） (2026-06-14T21:46:04Z) - VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。
VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。
Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文 参考訳（メタデータ） (2026-06-03T20:02:35Z) - RepoMirage: Probing Repository Context Reasoning in Code Agents with Perturbations [51.43574078961796]
本稿では,SWE-Bench Verified上に構築された2段階評価スイートRepoMirageを紹介する。
RepoMirage-Perturbは、リポジトリレベルの摂動を保存する3つのタイプのセマンティクスを適用している。
RepoAnchorは、下流の問題解決からリポジトリの探索を分離する構造第一のプロトタイプワークフローである。
論文 参考訳（メタデータ） (2026-05-25T06:26:43Z) - Affordance Agent Harness: Verification-Gated Skill Orchestration [45.231685718099264]
Affordance groundingは、オープンワールドのシーンでエージェントがどこでどのように対話すべきかを特定する必要がある。
本稿では,エビデンスストアとコストコントロールを備えたクローズドループランタイムであるAffordance Agent Harnessを提案する。
論文 参考訳（メタデータ） (2026-05-01T13:45:16Z) - Zero-shot Fact Verification by Claim Generation [85.27523983027471]
我々は,堅牢な事実検証モデルをトレーニングするフレームワークであるQACGを開発した。
われわれは自動的に生成されたクレームを使って、Wikipediaのエビデンスからサポートしたり、反論したり、検証したりできる。
ゼロショットシナリオでは、QACGはRoBERTaモデルのF1を50%から77%に改善し、パフォーマンスは2K以上の手作業による例に相当する。
論文 参考訳（メタデータ） (2021-05-31T03:13:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。