論文の概要: Synthesizing Proofs Using Proof Sharding and Exploration

• arxiv url: http://arxiv.org/abs/2609.28535v1
• Date: Tue, 22 Sep 2026 20:07:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-25 21:10:09.384515
• Title: Synthesizing Proofs Using Proof Sharding and Exploration
• Title（参考訳）: 証明シャーディングと探索による証明の合成
• Abstract要約: ProofSaXは、大規模な検証タスクをシャード化し、各シャードに対する証明検索空間を独立に探索し、正当性証明を合成する自動ツールである。 ProofSaXは103の証明補完タスクのうち86で最後の証明アノテーションを見つけることができ、実行時間は1分から2時間である。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Distributed systems are hard to implement correctly, and subtle bugs can go undetected using traditional testing. Formal verification offers an alternative for proving the correctness of complex distributed systems. Despite previous efforts to automate and facilitate formal verification, it is still hard to integrate formal verification in software development. Programmers need to query the theorem prover repeatedly to find the correct proof of their system. This cycle of going back and forth with the theorem prover involves a lot of human intervention and is a barrier to adopting formal verification in software development. In this paper, we address the challenges of scaling formal verification in practice by reducing the human intervention required to find the correctness proof of a distributed system. We propose ProofSaX, an automated tool that shards large verification tasks and explores the proof search space for each shard independently to synthesize correctness proofs. We use controlled exploration when adding possible proof annotations to handle the search-space explosion problem. We evaluate ProofSaX on a variety of safety proofs for distributed systems. We show that ProofSaX can find the last proof annotation in 86 out of 103 proof-completion tasks, with runtimes ranging from one minute to two hours.
• Abstract（参考訳）: 分散システムは正しく実装することは困難で、微妙なバグは従来のテストでは検出できない。 形式的検証は、複雑な分散システムの正しさを証明する代替手段を提供する。 形式的検証を自動化し、促進する以前の取り組みにもかかわらず、ソフトウェア開発に形式的検証を統合することは依然として困難である。 プログラマは、自身のシステムの正しい証明を見つけるために、定理証明器を何度も問い合わせる必要がある。 定理証明と行き来するこのサイクルは、多くの人間の介入を伴い、ソフトウェア開発で正式な検証を採用する上で障壁となります。 本稿では,分散システムの正当性証明を見つけるのに必要な人的介入を減らすことで,形式的検証を実践的にスケールアップする上での課題に対処する。 ProofSaXは、大規模な検証タスクをシャード化し、各シャードに対する証明検索空間を独立に探索し、正当性証明を合成する自動ツールである。 我々は,探索空間の爆発問題に対処するために,可能な証明アノテーションを追加する際に,制御探索を利用する。 ProofSaXを分散システムの安全性証明として評価する。 ProofSaXは103の証明補完タスクのうち86で最後の証明アノテーションを見つけることができ、実行時間は1分から2時間である。

関連論文リスト

• Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization [20.22828310618122]
  ToMapは、Decomposer-Formalizer-Proverパイプラインとして自動形式化の証明を構築するフレームワークである。 ToMapは,構文的正当性と意味的忠実性の両方で評価すると,最善前の手法よりも19.0%向上することを示す。
  論文  参考訳（メタデータ） (2026-07-13T09:21:15Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。 ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。 タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
  論文  参考訳（メタデータ） (2026-04-07T01:19:41Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。 我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。 我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-13T01:33:20Z)
• StepProof: Step-by-step verification of natural language mathematical proofs [16.150265021594088]
  本稿では,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。 StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。 StepProofは従来の手法に比べて証明成功率と効率を著しく改善することを示す。
  論文  参考訳（メタデータ） (2025-06-12T10:31:23Z)
• ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction [0.0]
  本稿では,自動定理証明を強化するニューロシンボリックフレームワークProofNet++を提案する。 ProofNet++は,従来のモデルよりも検証精度,正確性,形式的妥当性を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-05-30T05:44:34Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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