論文の概要: Towards Automating Blockchain Consensus Verification with IsabeLLM
- arxiv url: http://arxiv.org/abs/2601.07654v1
- Date: Mon, 12 Jan 2026 15:35:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-01-13 19:08:01.516985
- Title: Towards Automating Blockchain Consensus Verification with IsabeLLM
- Title（参考訳）: IsabeLLMによるブロックチェーン合意検証の自動化に向けて
- Authors: Elliot Jones, William Knottenbelt,
- Abstract要約: 本稿では,IsabeLLMを提案する。IsabeLLMは,IsabelleとLarge Language Modelを統合して,証明を支援し,自動化するツールである。
我々は、IsabeLLMの有効性を、BitcoinのProof of Workコンセンサスプロトコルの新しいモデルの開発に利用し、その正確性を検証する。
- 参考スコア（独自算出の注目度）: 1.9336815376402718
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Consensus protocols are crucial for a blockchain system as they are what allow agreement between the system's nodes in a potentially adversarial environment. For this reason, it is paramount to ensure their correct design and implementation to prevent such adversaries from carrying out malicious behaviour. Formal verification allows us to ensure the correctness of such protocols, but requires high levels of effort and expertise to carry out and thus is often omitted in the development process. In this paper, we present IsabeLLM, a tool that integrates the proof assistant Isabelle with a Large Language Model to assist and automate proofs. We demonstrate the effectiveness of IsabeLLM by using it to develop a novel model of Bitcoin's Proof of Work consensus protocol and verify its correctness. We use the DeepSeek R1 API for this demonstration and found that we were able to generate correct proofs for each of the non-trivial lemmas present in the verification.
- Abstract（参考訳）: コンセンサスプロトコルは、潜在的に敵対的な環境でシステムのノード間の合意を可能にするため、ブロックチェーンシステムにとって不可欠である。
そのため、このような敵が悪意ある行動を起こすのを防ぐために、正しい設計と実装を確実にすることが最重要である。
形式的検証により、そのようなプロトコルの正確性を保証することができるが、実行には高いレベルの労力と専門知識が必要であるため、開発プロセスでは省略されることが多い。
本稿では,IsabeLLMを提案する。IsabeLLMは,IsabelleとLarge Language Modelを統合して,証明を支援し,自動化するツールである。
我々は、IsabeLLMの有効性を、BitcoinのProof of Workコンセンサスプロトコルの新しいモデルの開発に利用し、その正確性を検証する。
このデモにはDeepSeek R1 APIを使用し、検証に存在する非自明な補題のそれぞれに対して、正しい証明を生成できることが分かった。
関連論文リスト
- Proof of Trusted Execution: A Consensus Paradigm for Deterministic Blockchain Finality [0.391985484065646]
本稿では,再実行を再現するのではなく,合意が検証実行から生じる合意パラダイムとして,信頼された実行の証明(PoTE)を提案する。
実行は決定論的であり、プロポーサは公開ランダム性から一意に派生しているため、PoTEはフォークを避け、スロット・タイムのボトルネックを排除し、1ラウンドの検証でブロックをコミットする。
論文 参考訳（メタデータ） (2025-12-10T08:04:38Z) - Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
Etherscanの78,047,845のスマートコントラクトがデプロイされているにも関わらず(2025年5月26日現在)、わずか767,520 (1%)がオープンソースである。
この不透明さは、オンチェーンスマートコントラクトバイトコードの自動意味解析を必要とする。
バイトコードを可読でセマンティックに忠実なSolidityコードに変換する,先駆的な逆コンパイルパイプラインを導入する。
論文 参考訳（メタデータ） (2025-06-24T13:42:59Z) - Think Before You Accept: Semantic Reflective Verification for Faster Speculative Decoding [48.52389201779425]
投機的復号化は、軽量モデルを使用して複数のドラフトトークンを生成し、それらを並列に検証することで推論を加速する。
既存の検証手法は、意味的正確性を見越しながら、分布の整合性に大きく依存している。
我々は,学習自由でセマンティックなアプローチであるリフレクティブ検証を提案し,正確性と効率のトレードオフを改善する。
論文 参考訳（メタデータ） (2025-05-24T10:26:27Z) - Formal Model Guided Conformance Testing for Blockchains [1.4838910416636741]
本稿では,プロトコルの形式モデルを用いたプロトコル適合性テストを行うフレームワークを提案する。
私たちのフレームワークは、トレースジェネレータとチェッカーとしてコンポーネントを使用する2つの補完的なコンポーネントで構成されています。
論文 参考訳（メタデータ） (2025-01-15T03:20:13Z) - BlockScan: Detecting Anomalies in Blockchain Transactions [16.73896087813861]
BlockScanはブロックチェーントランザクションの異常検出用にカスタマイズされたTransformerである。
この研究は、ブロックチェーンデータ分析にTransformerベースのアプローチを適用するための新しいベンチマークを設定する。
論文 参考訳（メタデータ） (2024-10-05T05:11:34Z) - Scalable Zero-Knowledge Proofs for Verifying Cryptographic Hashing in Blockchain Applications [16.72979347045808]
ゼロ知識証明(ZKP)は、現代のブロックチェーンシステムのスケーラビリティ問題に対処するための、有望なソリューションとして登場した。
本研究では,暗号ハッシュの計算完全性を保証するため,ZKPの生成と検証を行う手法を提案する。
論文 参考訳（メタデータ） (2024-07-03T21:19:01Z) - CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。
主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。
理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
論文 参考訳（メタデータ） (2023-05-20T11:26:51Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。