論文の概要: count-catcher: Lean Theorems from Model Counting Certificates

• arxiv url: http://arxiv.org/abs/2610.36196v1
• Date: Mon, 26 Oct 2026 19:34:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-29 04:15:49.196198
• Title: count-catcher: Lean Theorems from Model Counting Certificates
• Title（参考訳）: count-catcher: モデルカウント証明書のリーン理論
• Abstract要約: 正確なモデルカウンタ d4 によるカウントの CPOG 証明書を、リーンで定義された CNF 式が V 変数よりも正確に N モデルを持つというリーンの定理に変換する。 カウントキャッチャーはリーンで、公式が回路と等価性の証明を意味することを確認している。 約8つの証明書から数百個の認証済み数の重み付き和として8のラテン正方形の数を証明する。
• 参考スコア（独自算出の注目度）: 23.019404438086525
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present count-catcher, a tool that turns a CPOG certificate of a count by the exact model counter d4 into a Lean theorem that a CNF formula defined in Lean has exactly N models over V variables. With an encoding lemma, this theorem becomes a theorem about the number of combinatorial objects. A CPOG certificate consists of a Boolean circuit equivalent to the formula and a proof of equivalence. count-catcher checks in Lean that the formula implies the circuit (forward check) and the circuit implies the formula (reverse check). For the forward check, lrat-catcher streams a refutation through the LRAT checker of Lean's standard library. The reverse check and the validity check of the circuit are computations proved correct in Lean. Lean runs all three checks as compiled code, so the theorem depends on Lean's kernel, compiler and runtime, as does CPOG's verified checker. We combine the theorem with results from Mathlib, for instance with Burnside's lemma to count graphs up to isomorphism. We prove the number of Latin squares of order 8 as a weighted sum of hundreds of certified counts from about eight terabytes of certificates. We turn about half of the 2022 Model Counting Competition formulas into theorems, with the three checks taking about a quarter of the time of CPOG's verified checker. We found that CPOG's unverified checker reported wrong counts, and removed its verified checker's dependence on two unproved lemmas. End to end, a theorem costs about the same as a checked count.
• Abstract（参考訳）: これは、正確なモデルカウンタd4によるカウントのCPOG証明書を、Leanで定義されたCNF式がV変数よりも正確にNモデルを持っているというLeanの定理に変換するツールです。 符号化補題を用いて、この定理は組合せ対象の数に関する定理となる。 CPOG証明書は、公式に相当するブール回路と等価性の証明からなる。 count-catcherはLeanで、公式が回路(前方チェック)であり、回路が公式(逆チェック)であることを示す。 フォワードチェックでは、lrat-catcherがLeanの標準ライブラリのLRATチェッカーを通じて、難読化をストリームする。 逆チェックと回路の妥当性チェックは、Leanで証明された計算である。 Leanはコンパイルされたコードとして3つのチェックすべてを実行するので、定理はLeanのカーネル、コンパイラ、ランタイムに依存します。 例えば、定理とMathlibの結果を、バーンサイドの補題と組み合わせて、グラフを同型まで数える。 約8テラバイトの証明書から、数百の認証済み数の重み付けの和として、位数8のラテン正方形の数を証明する。 2022年のモデルカウントコンペティションの式の半分を定理に変換し、CPOGの検証チェッカーの約4分の1の時間でチェックします。 CPOGの未検証チェッカーは不正なカウントを報告し、検証済みチェッカーが2つの未証明レムマに依存していることが判明した。 結局のところ、定理はチェックカウントと同じくらいの費用がかかる。

関連論文リスト

• Lean Graph Search for Formal Theorem Proving [82.31440013289564]
  グラフに基づくLean4の検索手法であるLeanGraphSearchを提案する。 Mathlibのフォワード依存関係からグラフを構築し、それをトラバースして、サポート対象の補題を明らかにする。 3つの定理証明ベンチマークで、LeanGraphSearchは8, 16, 32リフレクションのパスレートをバニラ証明よりも40%向上させる。
  論文  参考訳（メタデータ） (2026-10-15T17:55:21Z)
• Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study [0.20415910628419062]
  大規模言語モデル(LLM)は数学的証明に類似したテキストを生成することができるが、類似性は正確性を確立しない。 Coqのルールは、システムのどの証明ステップが受け入れられるかを定義する論理的フレームワークであるCalculus of Inductive Constructionsに基づいている。 このパイロット研究は、実際のCoqプロジェクトから派生したベンチマークであるCoqStoqから、同じ100の定理で6つのオープンウェイトLSMを評価した。
  論文  参考訳（メタデータ） (2026-08-05T21:29:12Z)
• Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound [0.0]
  mathbbR3$ の最小コシェン=スペクターベクトル系に対する最もよく知られた下界は、半分が DRAT を出力するが、幾何的半分がそうでないような計算証明に依存する。 正則な正則な正則ケースツリー証明を導入し、その分割は分解因子と正則な二乗分解である。 すべての証明書、チェッカー、証明は、単一のビルドから利用可能で、再生可能である。
  論文  参考訳（メタデータ） (2026-07-29T02:53:00Z)
• Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving [13.87786274932945]
  リーンで証明されたLCM支援定理のベンチマークは、すべての解決されたインスタンスがマシンチェックされた証明を持ってくるため、本質的に信頼できるものとして扱われることが多い。 コーパススケールの静的チェッカーを用いて4,833個の結果を得た。 本稿では,フォールト分類法,自動チェッカーとリコール指向のセマンティック監査プロンプト,および公式な数学データセットの作成を導くための標準リリースを提案する。
  論文  参考訳（メタデータ） (2026-06-28T16:46:36Z)
• 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)
• PBLean: Pseudo-Boolean Proof Certificates for Lean 4 [27.126691338850254]
  PBLean は VeriPB pseudo-Boolean (PB) 証明証明書をLean 4 にインポートする手法である。 リーンで完全証明され、コンパイルされたネイティブコードとして実行されるブールチェッカー関数。 我々のチェッカーは、カットプレーンや証明・バイ・コントラディション・サブプロテクションを含む全てのVeriPBカーネルルールをサポートしている。
  論文  参考訳（メタデータ） (2026-02-09T14:13:30Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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