論文の概要: PBLean: Pseudo-Boolean Proof Certificates for Lean 4
- arxiv url: http://arxiv.org/abs/2602.08692v1
- Date: Mon, 09 Feb 2026 14:13:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-10 20:26:25.27226
- Title: PBLean: Pseudo-Boolean Proof Certificates for Lean 4
- Title（参考訳）: PBLean: リーン4のPseudo-Boolean証明
- Authors: Stefan Szeider,
- Abstract要約: PBLean は VeriPB pseudo-Boolean (PB) 証明証明書をLean 4 にインポートする手法である。
リーンで完全証明され、コンパイルされたネイティブコードとして実行されるブールチェッカー関数。
我々のチェッカーは、カットプレーンや証明・バイ・コントラディション・サブプロテクションを含む全てのVeriPBカーネルルールをサポートしている。
- 参考スコア（独自算出の注目度）: 27.126691338850254
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present PBLean, a method for importing VeriPB pseudo-Boolean (PB) proof certificates into Lean 4. Key to our approach is reflection: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code. Our method scales to proofs with tens of thousands of steps that would exhaust memory under explicit proof-term construction. Our checker supports all VeriPB kernel rules, including cutting-plane derivations and proof-by-contradiction subproofs. In contrast to external verified checkers that produce verdicts, our integration yields Lean theorems that can serve as composable lemmas in larger formal developments. To derive theorems about the original combinatorial problems rather than about PB constraints alone, we support verified encodings. This closes the trust gap between solver output and problem semantics since the constraint translation and its correctness proof are both formalized in Lean. We demonstrate the approach on various combinatorial problems.
- Abstract（参考訳）: PBLean は VeriPB pseudo-Boolean (PB) 証明証明書をLean 4 にインポートする手法である。
リーンで完全証明され、コンパイルされたネイティブコードとして実行されるブールチェッカー関数。
我々の手法は、明示的な証明期間構成の下でメモリを消費する数万ステップの証明にスケールする。
我々のチェッカーは、カットプレーンの導出や証明・バイ・コントラディションのサブプロテクションを含む全てのVeriPBカーネルルールをサポートしている。
検証を生成する外部の検証チェッカーとは対照的に、私たちの統合は、より大きな形式的な開発において構成可能な補題として機能するリーンの定理を生み出します。
PB制約のみでなく、元の組合せ問題に関する定理を導出するために、検証された符号化をサポートする。
これは、制約翻訳と正当性証明の両方がリーンで形式化されているため、ソルバ出力と問題セマンティクスの信頼ギャップを埋めます。
様々な組合せ問題に対するアプローチを実証する。
関連論文リスト
- BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。
中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。
我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
論文 参考訳（メタデータ） (2025-10-17T14:20:50Z) - Hilbert: Recursively Building Formal Proofs with Informal Reasoning [38.36481253622752]
大規模言語モデル(LLM)は、驚くべき数学的推論能力を示しているが、そのソリューションには自動検証できないエラーが含まれていることが多い。
非公式な推論と形式的検証の相補的な強みを組み合わせたエージェントフレームワークであるHilbertを紹介する。
我々のシステムは4つのコンポーネントを編成する: 数学的推論に優れる非公式のLLM、リーン4の戦術に最適化された特殊なLLM、形式検証器、意味定理検索器。
論文 参考訳（メタデータ） (2025-09-26T18:24:23Z) - What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
論文 参考訳（メタデータ） (2025-08-01T22:16:30Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。