論文の概要: Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL

• arxiv url: http://arxiv.org/abs/2608.01965v1
• Date: Mon, 03 Aug 2026 09:33:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-04 15:07:25.470707
• Title: Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL
• Title（参考訳）: Isabelle/STARK: Isabelle/HOLにおけるzk-STARKの形式化
• Abstract要約: 本報告では,STARK方式の透過的証明プロトコルのIsabelle/HOL形式化について述べる。 プロトコルを説明するのに十分な暗号的コンテキストを提供するが、その主な重点は形式的モデルである。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This report describes an Isabelle/HOL formalization of a STARK-style transparent proof protocol. The development contains an executable model of the prover and verifier, a finite probabilistic state monad with a weakest-precondition calculus, a zero-failure honestcompleteness theorem, and a staged soundness theorem with an explicit probability bound. The report is written for readers with a formal-methods background. It gives enough cryptographic context to explain the protocol, but its main emphasis is the formal model, the decomposition of the proofs, and the Isabelle source locations of the principal definitions and theorems.
• Abstract（参考訳）: 本報告では,STARK方式の透過的証明プロトコルのIsabelle/HOL形式化について述べる。 この開発には、証明器と検証器の実行可能なモデル、最も弱い前提計算を持つ有限確率状態モナド、ゼロ欠陥完全性定理、明示的な確率境界を持つステージド音響性定理が含まれる。 レポートは、形式的な背景を持つ読者向けに書かれています。 プロトコルを説明するのに十分な暗号的文脈を提供するが、その主な重点は形式的モデル、証明の分解、および主定義と定理のイザベル元の位置である。

関連論文リスト

• ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning [0.0]
  大規模言語モデル(LLMs)は、数学的および論理的分野における説得的議論を生み出す可能性がある。 LeanとCoqは、構文的および意味的ステートメントがプログラム内のすべての構文的および意味的ステップをパスできるステートメントのみを受け入れることを保証することで、厳格な信頼性を持つ。 本稿では,LLMがコンパクトDSLの型付き証明スケッチを生成し,軽量な信頼できるカーネルがスケッチを明示的な証明義務に拡張するハイブリッドパイプラインを提案する。
  論文  参考訳（メタデータ） (2026-04-07T19:33:54Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。 我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。 我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-13T01:33:20Z)
• Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem [0.2599882743586163]
  我々はシグモイド関数の形式化を示し、その単調性、滑らか性、高階微分を証明した。 本稿では、シグモダルアクティベーション関数を持つニューラルネットワークが、任意の連続関数をコンパクトな間隔で近似できることを示すユニバーサル近似定理の構成的証明を提案する。 我々の研究はニューラルネットワークの信頼性を高め、検証され信頼性の高い機械学習というより広い目標に貢献する。
  論文  参考訳（メタデータ） (2025-12-03T10:16:02Z)
• Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
  CoT(Chain-of-Thought)は、大規模言語モデルの推論能力を高める。 本稿では、カリー・ホワード対応に基づく新しい理論レンズを提案する。 我々はこの類似を運用し、CoTの非公式な自然言語ステップを形式化された型付き証明構造に抽出し、マッピングする方法を提供する。
  論文  参考訳（メタデータ） (2025-10-01T16:06:40Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
  トークン化は、NLPパイプラインにおける重要なステップである。 NLPにおける標準表現法としての重要性は認識されているが、トークン化の理論的基盤はまだ完全には理解されていない。 本稿では,トークン化モデルの表現と解析のための統一的な形式的枠組みを提案することによって,この理論的ギャップに対処することに貢献している。
  論文  参考訳（メタデータ） (2024-07-16T11:12:28Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)
• Isabelle Formalisation of Original Representation Theorems [0.0]
  明らかに無関係な数学的対象をリンクする新しい定理は、巨大なデータベース上のクロスサイトデータマイニングによって発見された。 そのような定理の起源と新しさを考えると、それらの形式的検証は特に望ましい。 本稿では、Isabelle/HOL定義と定理による検証を行い、そのプロセスで見られる技術的課題を明らかにする。
  論文  参考訳（メタデータ） (2023-06-18T13:43:21Z)

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

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