論文の概要: CAPRI: Contract-Aware Proof Repair for Isabelle

• arxiv url: http://arxiv.org/abs/2608.13459v1
• Date: Thu, 13 Aug 2026 16:43:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-14 18:29:38.606862
• Title: CAPRI: Contract-Aware Proof Repair for Isabelle
• Title（参考訳）: CAPRI:Isabelleの契約保証
• Abstract要約: イザベルのビルドは、提出された理論が受け入れられていることを保証するが、LLMが開発者によって承認されたものだけを変更したわけではない。 本稿では,Isabelleが証明を確認し,独立したチェッカーが機械可読編集契約を強制する,契約対応の修復ワークフローであるCAPRIを紹介する。
• 参考スコア（独自算出の注目度）: 5.286470899048593
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM changed only what the developer authorised. We present CAPRI, a contract-aware repair workflow in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract. Prompts, proposals, candidate repositories, diagnostics, verdicts, and hashes are retained for audit. We evaluate five workflows on twelve failed proofs from four developments, with three replicates per task and condition, giving 180 runs and 138 valid repairs. Of 144 terminal candidates accepted by Isabelle, six had modified protected text; all arose in iterative workflows that could edit a complete theory. A proof-body-only interface produced 29/36 valid repairs and no contract violations, compared with 31/36 for the corresponding full-theory workflow. One-shot repair produced 22/36, while a later prospectively frozen iterative workflow produced 32/36; these figures compare complete workflows rather than individual mechanisms. A separate post hoc OpenRouter campaign found no improvement in the designated Luna comparisons. A Sol configuration with matched demonstrations produced 33/36 repairs, compared with 29/36 in the frozen OpenAI Responses condition, but the difference was not statistically significant in a one-sided exact McNemar test ($p=0.0625$).
• Abstract（参考訳）: 我々は,Isabelle証明の発見を支援するために,大規模言語モデル (LLM) の利用に対処する。 イザベルのビルドは、提出された理論が受け入れられていることを保証するが、LLMが開発者によって承認されたものだけを変更したわけではない。 本稿では,Isabelleが証明を確認し,独立したチェッカーが機械可読編集契約を強制する,契約対応の修復ワークフローであるCAPRIを紹介する。 プロンプト、提案、候補リポジトリ、診断、評決、ハッシュは監査のために保持される。 我々は4つの開発から得られた12の証明に対して5つのワークフローを評価し、タスクと条件ごとに3つの複製を行い、180回の実行と138回の有効な修復を行った。 イザベルが受け入れた144人の端末候補のうち、6人は保護されたテキストを修正しており、全ては完全な理論を編集できる反復的なワークフローで発生した。 証明ボディのみのインタフェースは29/36の有効な修復を行い、契約違反は発生しなかった。 1発の修理は22/36で、後に凍結した反復ワークフローは32/36で、これらの数字は個々のメカニズムではなく完全なワークフローを比較した。 別のポストホックなOpenRouterキャンペーンでは、指定されたLuna比較の改善は見つからなかった。 一致するデモを行ったゾルの構成は、凍ったOpenAI反応条件の29/36と比較すると33/36の修理をおこなったが、片面の正確なマクネマール試験(p=0.0625$)では統計的に有意な差はなかった。

関連論文リスト

• NovaFabric: Tamper-Evident, Replayable Evidence for Autonomous AI Agent Runs [0.0]
  我々はNovaFabricを紹介し、監査グレードの実行証拠を作成している。 エージェントロジックを変更することなく実行中のエージェントを、ポータブルなRun Capsuleに記録する。 シードランは4モードのリプレイプロトコルで再実行可能である。 我々は8つの研究課題を測定範囲で評価した。
  論文  参考訳（メタデータ） (2026-09-11T08:35:43Z)
• From Traceability to Justifiability: Accountability Structures in Agentic Software Engineering [0.0]
  公開資料のみから、AIレコードがクレームを表現できるかどうか、宣言された場所を保持できるかどうかを測定する。 188個の二重グレード細胞で、デフォルトレコードが行動システムのコンテンツアイデンティティを出力するプラットフォームは見つからなかった。 計器は、パイプラインが発行した排気のみからの保証深度を計算し、宣言された深さと比較する。
  論文  参考訳（メタデータ） (2026-08-21T16:45:00Z)
• Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study [5.286470899048593]
  大規模言語モデルは対話型定理証明器を提案することができるが、成功したビルドは、周囲の検証タスクが保存されていることを示すものではない。 サンプルデータ二重タンクコントローラのイザベル開発においてこの問題について検討する。 作業は9つの理論と10の未完成の義務から始まり、謝罪なしに16の理論的な構築へと成長し、オープ、公理化、またはオラクルの使用を追加し、23の安定状態と36の壊れた証明状態を蓄積した。
  論文  参考訳（メタデータ） (2026-08-19T11:23:33Z)
• ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction [39.15744753769387]
  ALPS (Austin-Law Proof-Synthesis) は、有効な創造性を測定するためのタスクを設計するベンチマークである。 それぞれの例は単一の方程式法則であり、法則を満たす無限の数学的構造の構築を必要とするか、そのような構造が存在しないという証明を必要とする。 先行する自動プローバーの8つの構成のポートフォリオは、4,141の法則評価プールの2.2%を解決している。
  論文  参考訳（メタデータ） (2026-08-17T00:14:53Z)
• Judging Is Not Enumerating: Silent Omissions in LLM-Authored Acceptable Sets [13.85834524293015]
  私たちは、ロールが想定する能力を測定し、通常、ロールが配置されるプロトコルの下でそれを欠いていることを見つけます。 モデルは、その候補がセット自体の作者よりもはるかに優れているかどうかを判断する。
  論文  参考訳（メタデータ） (2026-08-02T05:00:44Z)
• Visual Credit Audit for Multimodal Spatial Reasoning [70.16915309526443]
  Visual Credit Auditは、ベンチマーク画像がテキストのみとブランクコントロールよりもモデルの宣言された決定をもっとサポートするかどうか、モデルが関係性固有の視覚的エビデンスに反応するかどうかの2つの評価を分離する。 ラベルを適用すれば依存性認定正当性(D-CC)が得られる 4つのオープンMLLMと2つの空間ベンチマーク、12.73-26.25%の判定は正確であるが、証明されていない。
  論文  参考訳（メタデータ） (2026-07-29T15:55:31Z)
• Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair [36.56438114281786]
  正しいパッチの発見と保持、検証、提出のギャップについて検討する。 我々はエビデンスバウンド型ループ契約を導出し、その機械的に強制可能なサブセットを参照実装でインスタンス化する。
  論文  参考訳（メタデータ） (2026-07-27T16:05:23Z)
• The Checking Problem: What must be true before AI ships in a regulated firm [0.0]
  規制金融サービスにおいて毎日実施される6種類の文書は、4つのモデルファミリーと3つのツールファミリーにまたがって実行された。 筆者らは、各構成が課すレビューの負担を、後見ではなく、サンプルから見積もっている。 現実的な意味は、AIワークフローの価値は、人間がチェックしなければならない頻度よりも、正しい頻度で設定されていることです。
  論文  参考訳（メタデータ） (2026-07-25T02:35:12Z)
• Can Code Specify a System Precisely Enough to Formally Verify It? [0.0]
  本報告では,業務用レストラン・ポイント・オブ・セールシステムの支払ワークフローを実運用ソフトウェアで評価する。 コアプロトコルは、正確に定義された障害モデルの下で手作りのラインアクティベートされたモデルに対して正しい。 生産用サンドボックスの1つのプローブは、全リカバリはしごを到達不能にする応答形状のばらつきを露呈した。
  論文  参考訳（メタデータ） (2026-07-06T13:39:00Z)
• CEPO: RLVR Self-Distillation using Contrastive Evidence Policy Optimization [50.59956036193097]
  検証可能な報酬(RLVR)を用いた強化学習における正しい解を生成するモデル 各トークンは、決定的な推論ステップであれ、文法的なフィラーであれ、同じ報酬信号を受信する。 コントラストエビデンスポリシー最適化(CEPO)を提案する。 CEPOは、全てのトークンに対してよりシャープな質問をする:「正しい答えは、このトークンを好むか?」が、「正しい答えは、正しい答えは、それを好む一方で、間違った答えはそれを好まないか?」。
  論文  参考訳（メタデータ） (2026-05-19T06:46:19Z)
• Inferring multiple helper Dafny assertions with LLMs [47.33158055894705]
  本研究では,Dafnyプログラムにおけるヘルパーアサーションの欠落を自動的に推測するために,Large Language Modelsの使用について検討する。 推論の難易度を分析するために,アサーション型の分類を導入した。 その結果、自動アサーション推論は証明工学の労力を大幅に削減できることが示された。
  論文  参考訳（メタデータ） (2025-10-31T09:45:39Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Lyra: Orchestrating Dual Correction in Automated Theorem Proving [63.115422781158934]
  Lyraは新しいフレームワークで、ツール補正とConjecture Correctionという2つの異なる補正メカニズムを採用している。 ツール補正は幻覚の緩和に寄与し、それによって証明の全体的な精度が向上する。 Conjecture Correctionは命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。
  論文  参考訳（メタデータ） (2023-09-27T17:29:41Z)

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

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