論文の概要: TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System
- arxiv url: http://arxiv.org/abs/2611.02849v1
- Date: Mon, 02 Nov 2026 09:51:18 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-11-06 14:53:30.994928
- Title: TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System
- Title（参考訳）: TLAPS-Bench:TLA+証明システムを用いた実世界のシステム仕様の形式的正当性証明
- Abstract要約: TLAPS-Benchは、エージェントAIを使用したTLA+の現実世界のシステム仕様に対するマシンチェックされた証明を構築するためのベンチマークである。
我々はAIエージェントを使用して、これまで証明されなかった重要なシステム仕様の望ましい特性を証明しました。
- 参考スコア（独自算出の注目度）: 5.935618599526175
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI. Proving correctness of complex system specifications requires discovering inductive invariants, reasoning about intricate state transitions, and decomposing proofs into tractable obligations. TLAPS-Bench provides a proof harness that supports iterative proof development atop the TLA+ Proof System (TLAPS), where agents are equipped with proof tools and libraries, with safeguards against reward hacking. Using the harness, we have employed AI agents to prove desired properties for important system specifications that were not proved before, spanning cache coherence, Byzantine consensus, and write-ahead logs. TLAPS-Bench contains 265 proof targets (each encodes a property to prove) from 95 TLA+ specifications of real-world systems. We evaluated frontier AI agents, represented by Codex with GPT models, on a subset of 70 proof targets across 12 specifications. The highest-scoring model, GPT-6.1 Sol (max), proved 31 (44.3%) proof targets. The results show challenges and opportunities in end-to-end proof development.
- Abstract（参考訳）: TLAPS-Benchは、エージェントAIを用いてTLA+の現実世界のシステム仕様に対するマシンチェックされた証明を構築するためのベンチマークと実行ハーネスである。
複雑なシステム仕様の正しさを証明するには、帰納的不変性を発見し、複雑な状態遷移を推論し、証明を抽出可能な義務に分解する必要がある。
TLAPS-Bench は TLA+ Proof System (TLAPS) 上で反復的証明開発をサポートする証明ハーネスを提供する。
このハーネスを使用することで、キャッシュコヒーレンス、ビザンチンのコンセンサス、書き込みアヘッドログなど、これまで証明されていなかった重要なシステム仕様に対する望ましい特性を証明するために、AIエージェントを使用しました。
TLAPS-Bench には、現実世界のシステムの 95 TLA+ 仕様から、265の証明対象(それぞれが証明するプロパティを符号化する)が含まれている。
我々は、12の仕様にわたる70の証明目標のサブセットに基づいて、Codexで表現されたフロンティアAIエージェントをGPTモデルで評価した。
最も高いスコア付けモデルである GPT-6.1 Sol (max) は31 (44.3%) の証明目標を証明した。
その結果、エンドツーエンドの証明開発における課題と機会が示された。
関連論文リスト
- Scaling Lean Theorem Proving for Real-World Code Verification [2.4869619439800723]
EasyProverは、669/672 PutnamBench問題と6つのIMO 2026の形式化を証明している。
Aegisは競合するプログラミング問題を実際の実装よりもはるかに難しい検証タスクに変換する。
2,045の差分検証されたRust-Leanプログラムペアと11,533の候補仕様を生成する。
論文 参考訳（メタデータ） (2026-10-28T02:23:25Z) - TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents [3.18543759301646]
VerusはRust用に構築された自動アクティブ検証ツールで、TLA+仕様の証明義務を大規模に生成する。
我々の研究は価値ある評価データセットをもたらし、Verusの定理証明における現在の世代モデル能力のマッピングに使用しています。
論文 参考訳（メタデータ） (2026-10-10T13:53:29Z) - AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness [10.0330160351666]
本稿では,自律的証明自動形式化と証明合成のためのエージェントフレームワークであるAIProverを提案する。
119Bのオープンウェイト言語モデルを共同で訓練し、HarnessEvolveとのエージェント的ツールコールハーネスを進化させた。
研究レベルのトレーニングと評価のために,RoCoBench,Mathlib,CSLib,Mizar Math Libraryの58.9kインスタンス,および有界算術教科書を紹介する。
論文 参考訳（メタデータ） (2026-10-04T16:48:12Z) - TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability [59.079078796751496]
我々は,研究レベルの理論計算機科学(TCS)証明生成において,Large Language Models(LLMs)を評価するためのベンチマークであるTCS-Benchを紹介する。
TCS-Benchは、理論計算機科学の会場で発表された論文の定理証明タスクで構成されている。
論文 参考訳（メタデータ） (2026-08-10T12:36:16Z) - Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems [100.24694338574402]
本稿では,インダクティブ・デダクティブ・シンセシス(IDS)について述べる。
IDSは約6.8時間で7/7を達成し、1仕様あたり106ドル、専門家の努力の約200倍、SOTAエージェントの約17%を達成している。
IDSはパフォーマンスフィードバックを同じループに組み込んでおり、検証されたシステムよりも最大3倍高速な実装を実現している。
論文 参考訳（メタデータ） (2026-05-22T00:05:36Z) - NANOZK: Layerwise Zero-Knowledge Proofs for Verifiable Large Language Model Inference [0.0]
LLM推論を検証可能なゼロ知識証明システムであるメソッドを提案する。
我々のアプローチは、トランスフォーマー推論が自然に独立した層計算に分解されるという事実を生かしている。
EZKLと比較して、EZKLは70倍小さい証明と5.7倍速い証明時間をd=128で達成し、形式的な音質保証を維持している。
論文 参考訳（メタデータ） (2026-03-17T04:14:45Z) - Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。
多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。
自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
論文 参考訳（メタデータ） (2026-02-02T17:42:53Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。