論文の概要: IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus
- arxiv url: http://arxiv.org/abs/2606.18098v1
- Date: Tue, 16 Jun 2026 16:00:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-17 17:15:32.532667
- Title: IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus
- Title（参考訳）: IsabeLLM: コンセンサスを形式的に検証する自動理論
- Authors: Elliot Jones, William Knottenbelt,
- Abstract要約: We improve on IsabeLLM, the automated proving tool in Isabelle。
Retrieval-Augmented Generation framework, Error Trace と counterexample generation を実装した。
IsabeLLMの2つのバージョンのパフォーマンスを、BitcoinのProof of Workコンセンサスの検証を完了する能力と比較する。
- 参考スコア（独自算出の注目度）: 1.9336815376402718
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Advances in Artificial Intelligence (AI) have led AI for Theorem Proving to become a promising means of formally verifying computer systems. Whilst formal verification is traditionally reserved for safety-critical systems due to the required amount of expertise and effort, AI can help to automate a large amount of this workload and make it far more accessible. Blockchain-based systems are becoming increasingly popular and are frequently targeted by malicious actors, often resulting in huge financial losses, highlighting the need to better verify these systems and mitigate vulnerabilities. Arguably the most important component of these systems is the consensus protocol, which allows nodes to agree on decisions in a potentially adversarial environment. In this paper, we improve upon IsabeLLM, the automated theorem proving tool in Isabelle. Namely, we implement a Retrieval-Augmented Generation framework, Error tracing and counterexample generation for improved context supplied to the Large Language Model. Compatibility with the latest version of Isabelle and Sledgehammer is also implemented for improved efficiency. We compare the performance of the two versions of IsabeLLM in their ability to complete the verification of Bitcoin's Proof of Work consensus.
- Abstract（参考訳）: 人工知能(AI)の進歩は、Theorem ProvingのAIを、コンピュータシステムを正式に検証する有望な手段に導いた。
フォーマルな検証は、必要な専門知識と努力のために伝統的に安全クリティカルなシステムに限られているが、AIは大量のワークロードを自動化し、はるかにアクセスしやすいものにする。
ブロックチェーンベースのシステムはますます人気を博し、悪意あるアクターに狙われ、しばしば大きな損失をもたらし、これらのシステムを検証することや脆弱性を軽減する必要性を強調している。
これらのシステムの最も重要なコンポーネントはコンセンサスプロトコルであり、ノードは潜在的に敵対的な環境における決定に合意することができる。
本稿では,イザベルにおける自動定理証明ツールであるIsabeLLMを改良する。
すなわち、大規模言語モデルに供給された文脈を改善するために、検索型拡張生成フレームワーク、エラートレースおよび反例生成を実装した。
IsabelleとSledgehammerの最新バージョンとの互換性も改善のために実装されている。
IsabeLLMの2つのバージョンのパフォーマンスを、BitcoinのProof of Workコンセンサスの検証を完了する能力と比較する。
関連論文リスト
- 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) - Provably Secure Agent Guardrail [89.79561918065122]
既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。
本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
論文 参考訳（メタデータ） (2026-05-28T02:12:41Z) - Trustworthy AI Suffers from Invariance Conflicts and Causality is The Solution [80.98492754957466]
公正性、堅牢性、プライバシ、説明可能性といった、信頼性の高いAI目標を同時に達成することは難しい。
本稿では、パフォーマンスにおけるトレードオフを理解しバランスをとるためには因果性が必要であると論じ、信頼できるAIの複数の目的について論じる。
論文 参考訳（メタデータ） (2026-05-04T14:26:28Z) - Reasoning-Aware AIGC Detection via Alignment and Reinforcement [55.09684020007737]
REVEALは、分類の前に解釈可能な推論チェーンを生成するフレームワークである。
複数のベンチマークで最先端のパフォーマンスを実現する。
論文 参考訳（メタデータ） (2026-04-21T07:29:55Z) - CREDIT: Certified Ownership Verification of Deep Neural Networks Against Model Extraction Attacks [54.04030169323115]
我々は、モデル抽出攻撃(MEA)に対する認証された所有権検証であるCREDITを紹介する。
DNNモデル間の類似性を定量化し、実用的な検証しきい値を提案し、このしきい値に基づいてオーナシップ検証を行うための厳密な理論的保証を提供する。
我々は、さまざまなドメインやタスクにまたがるいくつかの主流データセットに対するアプローチを広範囲に評価し、最先端のパフォーマンスを実現した。
論文 参考訳（メタデータ） (2026-02-23T23:36:25Z) - Towards Automating Blockchain Consensus Verification with IsabeLLM [1.9336815376402718]
本稿では,IsabeLLMを提案する。IsabeLLMは,IsabelleとLarge Language Modelを統合して,証明を支援し,自動化するツールである。
我々は、IsabeLLMの有効性を、BitcoinのProof of Workコンセンサスプロトコルの新しいモデルの開発に利用し、その正確性を検証する。
論文 参考訳（メタデータ） (2026-01-12T15:35:08Z) - Agentic Program Verification [14.684859166069012]
本稿では,プログラム検証を行うための最初の大規模言語モデルエージェントであるAutoRocqを提案する。
LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。
このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。
論文 参考訳（メタデータ） (2025-11-21T15:51:48Z) - SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems [12.181911851729614]
我々は、AIが大規模で複雑なシステムを正式にモデル化する能力を評価するベンチマークであるSysMoBenchを紹介する。
私たちは、今日の重要なコンピューティングインフラストラクチャのキーストーンである、並列および分散システムに重点を置いています。
論文 参考訳（メタデータ） (2025-09-27T05:24:54Z) - A Hashgraph-Inspired Consensus Mechanism for Reliable Multi-Model Reasoning [0.0]
大規模言語モデル(LLM)からの一貫性のない出力と幻覚は、信頼できるAIシステムにとって大きな障害となる。
本稿では,分散台帳技術に触発された新たなコンセンサス機構を提案する。
論文 参考訳（メタデータ） (2025-05-06T14:05:12Z) - Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
多くの言語モデル推論コールからなる複合AIシステムは、ますます採用されている。
本研究では,提案した回答の生成と正当性検証の区別を中心に,ネットワークネットワーク(NoN)と呼ばれるシステムを構築した。
我々は,Kジェネレータを備えた検証器ベースの判定器NoNを導入し,"Best-of-K"あるいは"judge-based"複合AIシステムのインスタンス化を行う。
論文 参考訳（メタデータ） (2024-07-23T20:40:37Z) - Auto.gov: Learning-based Governance for Decentralized Finance (DeFi) [14.697580721893809]
Auto$.$gov"は学習ベースのガバナンスフレームワークで、深いQnetwork強化学習(RL)戦略を用いて、半自動化されたデータ駆動パラメータ調整を実行する。
実世界のデータを用いたテストでは、Auto$.$govはベンチマークアプローチを少なくとも14%上回り、静的ベースラインモデルは10倍に向上する。
論文 参考訳（メタデータ） (2023-02-19T12:11:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。