論文の概要: Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound
- arxiv url: http://arxiv.org/abs/2607.26413v1
- Date: Wed, 29 Jul 2026 02:53:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-30 21:06:25.528235
- Title: Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound
- Title（参考訳）: 最小Kochen-Specker境界の幾何半に対する機械チャック認証
- Abstract要約: mathbbR3$ の最小コシェン=スペクターベクトル系に対する最もよく知られた下界は、半分が DRAT を出力するが、幾何的半分がそうでないような計算証明に依存する。
正則な正則な正則ケースツリー証明を導入し、その分割は分解因子と正則な二乗分解である。
すべての証明書、チェッカー、証明は、単一のビルドから利用可能で、再生可能である。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The best known lower bound for the minimum Kochen-Specker vector system in $\mathbb{R}^3$ -- 24 vectors -- rests on a computational proof whose combinatorial half emits DRAT proofs but whose geometric half does not: the non-embeddability of thousands of candidate graphs is established by Z3's nonlinear real arithmetic, which produces no checkable proof objects. We close this gap for the proof's blocking database. We introduce exact rational case-tree certificates of real non-embeddability, whose splits are polynomial factorizations and rational sum-of-squares decompositions and whose leaves are discharged by injectivity, ideal-membership, or Positivstellensatz-shaped positivity arguments, and we certify all 291 source lines (180 distinct graphs) of the published pipeline's order-10 to order-13 blocking lists. Certificates are replayed by two independent checkers that share no code with the generator: a pure-Python replay over exact fractions, and a total checker implemented and proved sound in Lean 4. The soundness theorem -- acceptance implies that no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph -- is kernel-checked with axiom closure {propext, Classical.choice, Quot.sound}, and a gcd-free rational arithmetic layer makes the entire verdict computation kernel-reducible, so each per-graph non-embeddability result is a closed kernel theorem proved by decide. The formalization surfaced findings about the published pipeline, including a load-bearing injectivity side condition in its embeddability notion, hidden WLOG case obligations invisible to Z3-based workflows, and an unreproducible candidate count that we resolve against the published artifacts. All certificates, checkers, and proofs are available and replayable from a single build.
- Abstract（参考訳）: 最小のKochen-Speckerベクトル系に対する最もよく知られた下界は、$\mathbb{R}^3$ -- 24 ベクトルは、組合せの半分が DRAT 証明を出力するが幾何半は出力しない計算証明に基づいている: 数千のグラフの非埋め込み性は、Z3 の非線形実算術によって確立され、チェック可能な証明オブジェクトは生成されない。
証明のブロッキングデータベースのこのギャップを埋めます。
実非埋め込み可能性の正則なケースツリー証明を導入し、その分割は多項式分解と正則二乗分解であり、葉は射影率、イデアル-メンバーシップ、ポシチブステレンサッツ型の肯定的議論によって放出され、我々は、出版されたパイプラインのオーダー10の291のソースライン(180個のグラフ)全てを、順序-13のブロッキングリストに認定する。
証明書は、ジェネレータとコードを共有しない2つの独立したチェッカーによって再生される。
音性定理(英語版) -- 受理すると、射影-対線、非零実ベクトルの直交-無視代入はグラフを認識せず、公理閉包 {propext, Classical.choice, Quot.sound} でカーネルチェックされる。
この形式化は、その組込み可能性の概念における負荷を含む射出性側の条件、Z3ベースのワークフローには見えない隠されたWLOGケース義務、そして、我々が公表されたアーティファクトに対して解決する再現不可能な候補数を含む、公表されたパイプラインに関する発見を表面化した。
すべての証明書、チェッカー、証明は、単一のビルドから利用可能で、再生可能である。
関連論文リスト
- AutoGraphForge: Towards Automated Graph Theory Discovery [0.0]
AutoGraphForgeは、自動グラフ理論の導出-拡散-ホルマライゼーション-自明なシステムである。
新規性フィルタは、既知の結果によって既に候補が示唆されているか否かを線形プログラムを介して決定する。
HPCクラスタ上で数ラウンド実行されると、リフューテーションデータセットを生き残った6,522ドルの予想が生成される。
論文 参考訳（メタデータ） (2026-09-03T07:35:29Z) - ProofPulse: Interactive Proof Coverage Analysis for Dafny [47.23158426199152]
帰納的検証は、実装がその仕様を満たすことを保証しますが、成功した検証は仕様の品質を保証しません。
本稿では,3値の証明カバレッジモデルを用いて,仕様品質を診断するDafny用ツールであるProgrampulseを提案する。
論文 参考訳（メタデータ） (2026-08-31T14:00:31Z) - Formalizing Flag Algebras in Lean [8.924529562496874]
ラズボロフのフラッグ代数法は、極端グラフ理論の不等式を証明する強力なツールである。
本手法の機械チェックによる形式化と,証明から保護までのコンパイラについて述べる。
ケーススタディは7つのターン型上界の形式的証明を与える。
論文 参考訳（メタデータ） (2026-07-26T07:07:29Z) - Byzantine Accountability Without Consensus: Strong Eventual Consistency for Non-Associative, Stochastic, Robust Aggregation [0.0]
ACFAは、署名されたコントリビューションのコンテンツ適応OR-Setと、自己認証等式証明の成長のみのセットを複製する。
プロトタイプ(10ノード、3ビザンティン)は16/16のファルシフィケーションチェックをパスします。
論文 参考訳（メタデータ） (2026-07-11T13:23:06Z) - Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
大規模言語モデル(LLM)は、自動的に証明を生成することを約束するが、既存のアプローチは、固定された人間設計の証明戦略をシステムに結び付ける。
このような戦略を課すことは不要で制限的であることを示す。
レムマ全体を一般的なコードエージェントに手渡して、独自のアプローチを自由に選択し、検証ハーネスにラップすることは、シンプルでより効果的です。
論文 参考訳（メタデータ） (2026-07-07T14:39:59Z) - ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics [3.848983210046659]
我々は Martin-Lof Dependent Type (MLTT) の保守的な拡張である ZX-Calculus (Knowledge Evolution Calculus) を提案する。
これは、トレースインデクシングされたタイプ、プレシーフ非モノトーン意味論、建設的なAGM信条修正を統合している。
Coq の機械化は論文に付随する(34の完全証明、0は2つの中心的な結果を認めている)。
論文 参考訳（メタデータ） (2026-06-02T02:51:41Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
システムはマドリブの27の上位領域の戦術的利用分布を抽出する。
zスコアを計算して、ソースエリアで多用されるが、ターゲットエリアで稀または欠落している戦術を特定する。
これは、GPUアクセラレーションされたNPハードアナログを用いて、ソースとターゲットの証明状態と一致する。
論文 参考訳（メタデータ） (2026-04-19T03:27:16Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。
我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
論文 参考訳（メタデータ） (2026-02-26T05:11:44Z) - General Cutting Planes for Bound-Propagation-Based Neural Network
Verification [144.7290035694459]
任意の切削平面制約を加えることができるような境界伝搬手順を一般化する。
MIPソルバは、境界プロパゲーションベースの検証器を強化するために高品質な切削面を生成することができる。
本手法は,oval20ベンチマークを完全解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器である。
論文 参考訳（メタデータ） (2022-08-11T10:31:28Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - Scalable Sampling for Nonsymmetric Determinantal Point Processes [47.18450267217498]
M$アイテムの集合上の決定点過程(DPP)は、対称的なカーネル行列によってパラメータ化されるモデルである。
最近の研究は、非対称DPP(NDPPs)を生じるカーネル対称性の制約を取り除くことで、機械学習アプリケーションにおいて大幅な性能向上が期待できることを示している。
コールスキー分解に基づくDPPサンプリングアルゴリズムは1つしか知られておらず、NDPPにも直接適用できる。
NDPPカーネルに特定の構造的制約を課すことで、カーネルのランクに依存する方法で拒絶率を制限できることが示される。
論文 参考訳（メタデータ） (2022-01-20T19:21:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。