論文の概要: Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4

• arxiv url: http://arxiv.org/abs/2602.08384v1
• Date: Mon, 09 Feb 2026 08:35:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-10 20:26:25.128907
• Title: Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4
• Title（参考訳）: 実世界の産業規模検証に向けて: seL4 を用いた LLM 駆動定理証明
• Authors: Jianyu Zhang, Fuyuan Zhang, Jiayi Lu, Jilin Hu, Xiaoyi Yin, Long Zhang, Feng Yang, Yongwang Zhao,
• Abstract要約: 形式的手法(FM)は信頼性が高いが、適用にはコストがかかる。 大規模言語モデル(LLM)の最近の進歩により、自動定理はますます実現可能になっている。 実世界の産業規模のシステムにおけるLCMによる定理証明手法であるAutoRealを提案する。
• 参考スコア（独自算出の注目度）: 14.340488105076062
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal methods (FM) are reliable but costly to apply, often requiring years of expert effort in industrial-scale projects such as seL4, especially for theorem proving. Recent advances in large language models (LLMs) have made automated theorem proving increasingly feasible. However, most prior work focuses on mathematics-oriented benchmarks such as miniF2F, with limited evaluation on real-world verification projects. The few studies that consider industrial-scale verification mostly rely on closed-source models with hundreds of billions of parameters, which cannot be locally deployed and incur substantial usage costs. In this paper, we propose AutoReal, an LLM-driven theorem proving method for real-world industrial-scale systems with support for lightweight local deployment. We evaluate AutoReal on the seL4-Isabelle verification project as a representative and challenging case study. AutoReal incorporates two key improvements: (1) chain-of-thought (CoT)-based proof training, which teaches the LLM the reasoning behind proof steps and enables step-wise explanations alongside proofs, and (2) context augmentation, which leverages proof context from the project to enhance LLM-driven proving. Based on the AutoReal methodology, we fine-tune a base model to obtain AutoReal-Prover, a compact 7B-scale prover for industrial-scale theorem proving. AutoReal-Prover achieves a 51.67% proof success rate on 660 theorems from seL4-designated Important Theories across all 10 seL4 proof categories, substantially outperforming prior attempts on seL4 (27.06%). To evaluate generalization, we further apply AutoReal-Prover to three security-related projects from the Archive of Formal Proofs (AFP), covering all 451 theorems and achieving a proof success rate of 53.88%. Overall, this work advances the application of LLM-driven theorem proving in real-world industrial-scale verification.
• Abstract（参考訳）: 形式的手法(FM)は信頼性があるが、適用にはコストがかかるため、特に定理証明のためには、SeL4のような産業規模のプロジェクトにおいて長年の専門的な努力を必要とすることが多い。 大規模言語モデル(LLM)の最近の進歩により、自動定理はますます実現可能になっている。 しかし、これまでのほとんどの研究は、MiniF2Fのような数学指向のベンチマークに焦点を当てており、実際の検証プロジェクトでは評価が限られていた。 産業規模の検証を検討する数少ない研究は、数十億のパラメータを持つクローズドソースモデルに大きく依存している。 本稿では,軽量なローカルデプロイメントをサポートする実世界の産業規模のシステムを対象とした,LLMによる定理証明手法であるAutoRealを提案する。 我々は,SeL4-Isabelle検証プロジェクトのAutoRealを代表的かつ挑戦的なケーススタディとして評価した。 AutoRealには,(1)実証ステップの背後にある推論をLLMに教えるチェーン・オブ・シント(CoT)ベースの証明トレーニングと,(2)プロジェクトからの証明コンテキストを活用してLLM駆動の証明を強化するコンテキスト拡張という,2つの重要な改善が含まれている。 産業規模の定理証明のためのコンパクトな 7B スケール証明器である AutoReal-Prover を得るための基礎モデルを微調整する。 AutoReal-Proverは、seL4に割り当てられた重要な理論から660の定理に対する51.67%の証明成功率を達成した。 一般化を評価するために、AutoReal-Proverは、公式証明アーカイブ(AFP)の3つのセキュリティ関連プロジェクトに適用し、451の定理をすべてカバーし、53.88%の証明成功率を達成する。 全体として、この研究は、実世界の産業規模の検証において証明されたLLM駆動の定理の適用を推し進めている。

関連論文リスト

• Neural Theorem Proving for Verification Conditions: A Real-World Benchmark [9.350519191460018]
  この研究は、NTP4VC(Neural Theorem Proving for Verification Conditions)を導入し、このタスクのための最初の実世界のマルチ言語ベンチマークを示す。 NTP4VC を用いて,大言語モデル (LLM) の評価を行った。
  論文  参考訳（メタデータ） (2026-01-26T20:37:11Z)
• RLMEval: Evaluating Research-Level Neural Theorem Proving [18.42453100491575]
  本稿では,実世界のリーン形式化プロジェクトによる研究レベルの数学評価スイートRLMEvalを紹介する。 リーンプロジェクトの613の定理を含むRLMEvalの最先端モデルの評価では、大きなギャップが明らかになりました。 RLMEvalは、形式数学の自動推論の進歩をガイドし、加速するために設計された、新しい挑戦的なベンチマークを提供する。
  論文  参考訳（メタデータ） (2025-10-29T11:49:49Z)
• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)
• 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)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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