論文の概要: LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection
- arxiv url: http://arxiv.org/abs/2607.00815v1
- Date: Wed, 01 Jul 2026 11:41:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-02 19:56:07.875098
- Title: LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection
- Title（参考訳）: LRAT-Catcher: SATソルバー証明書をレフレクションでLean4にインポート
- Abstract要約: LRAT-Catcherは、LRAT証明書とともにDIMACS式をLean 4に定理としてインポートする。
LRAT-Catcherは、Leanコアから公式に認証されたLRATチェッカーをリフレクション経由でコンパイルされたネイティブコードとして実行する。
キューブ毎の難読化はカバー完全性証明と組み合わされ、LRAT証明は単一の不満足な定理となる。
- 参考スコア（独自算出の注目度）: 27.126691338850254
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: SAT solvers settle combinatorial problems beyond the reach of interactive theorem provers and produce LRAT certificates for independent verification. We present LRAT-Catcher, a standalone, general-purpose tool that imports a DIMACS formula together with an LRAT certificate into Lean 4 as a theorem. LRAT-Catcher runs the formally verified LRAT checker from Lean core as compiled native code via reflection. This scales to instances where Mathlib's explicit proof-term import exhausts memory. LRAT-Catcher also composes cube-and-conquer solving runs entirely inside Lean. Per-cube refutations are combined with a cover-completeness certificate, itself an LRAT proof, into a single unsatisfiability theorem. Verified encodings connect CNF-level results to the original combinatorial problems. We evaluate the tool against Mathlib's proof-term import and the external checker cake_lpr on establishing the Schur number S(4) = 44 and the Ramsey number R(4,4) = 18 as Lean theorems.
- Abstract（参考訳）: SATソルバは、対話的定理証明の到達範囲を超えて組合せ問題を解決し、独立検証のためのLRAT証明書を生成する。
本稿では、LRAT証明とともにDIMACS式をLean 4にインポートするスタンドアロン汎用ツールLRAT-Catcherを紹介する。
LRAT-Catcherは、Leanコアから公式に認証されたLRATチェッカーをリフレクション経由でコンパイルされたネイティブコードとして実行する。
これは、Mathlibの明示的な証明期間のインポートがメモリを消費するインスタンスにスケールする。
LRAT-Catcherはまた、Lean内で完全にキューブ・アンド・コンカレンスを実行する。
キューブ毎の難読化はカバー完全性証明と組み合わされ、LRAT証明は単一の不満足な定理となる。
検証されたエンコーディングは、CNFレベルの結果と元の組合せ問題とを結びつける。
我々は、Schur数 S(4) = 44 と Ramsey数 R(4,4) = 18 をリーン定理として確立する際の、Mathlib の証明項インポートと外部チェッカーの cake_lpr に対するツールを評価する。
関連論文リスト
- Decomposed Entailment for Factuality Checking and Hallucination Detection [0.3602004729891047]
HallDetectは、幻覚検出のための軽量で、参照不要で、ブラックボックスのフレームワークである。
生成されたコンテンツは原子クレームに分解され、コンパクトエンコーダベースのエンテーメントモデルによって検証される。
制御されたプロトコルでは、すべてのメソッドは同じ4ビットの量子化バックボーンとコンシューマグレードのハードウェア予算を共有している。
論文 参考訳（メタデータ） (2026-08-06T09:52:09Z) - SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers [55.39407031861402]
本稿では,スマートコントラクトデコンパイルのためのデータセットとベンチマーク手法であるSCDBenchを紹介する。
データセットには600の現実のSolidityコントラクトと、ペア化されたバイトコード入力、地味なソースコード、再生可能なセマンティックチェックポイントが含まれている。
我々は,GLM-5の変種を含むゼロショット逆コンパイル設定において,Claude Opus 4.7,GPT-5.3-Codex,GLM-5を評価した。
論文 参考訳（メタデータ） (2026-05-27T20:08:47Z) - Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture [0.0]
本稿では,大規模言語モデルを取り巻く決定論的構造化計算を検証するためのフレームワークを提案する。
リーン4の信頼境界アーキテクチャを,現代的なLLMパイプラインの汎用インターフェースに拡張しています。
論文 参考訳（メタデータ） (2026-05-13T12:01: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) - VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean [34.16542476896347]
オープンソースのフォーマルメソッド開発から引き出された500リーン4の証明義務のベンチマークを導入します。
我々は、Mathlib型数学用に調整されたプローバーが、このリポジトリ中心の設定に不十分に移行していることを発見した。
証明の依存性のクロージャに制限されたキュレートされたコンテキストを提供することで、完全なリポジトリを公開することでパフォーマンスが向上する。
論文 参考訳（メタデータ） (2026-02-20T16:05:06Z) - PBLean: Pseudo-Boolean Proof Certificates for Lean 4 [27.126691338850254]
PBLean は VeriPB pseudo-Boolean (PB) 証明証明書をLean 4 にインポートする手法である。
リーンで完全証明され、コンパイルされたネイティブコードとして実行されるブールチェッカー関数。
我々のチェッカーは、カットプレーンや証明・バイ・コントラディション・サブプロテクションを含む全てのVeriPBカーネルルールをサポートしている。
論文 参考訳（メタデータ） (2026-02-09T14:13:30Z) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。
我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
論文 参考訳（メタデータ） (2026-01-30T08:29:01Z) - CARE What Fails: Contrastive Anchored-REflection for Verifiable Multimodal [84.71254539482369]
検証可能な報酬を伴うグループ相対的強化学習(RLVR)は、しばしば、すでに失敗している最も情報に富むデータを浪費する。
エラーを監督するマルチモーダル推論のための,障害中心のポストトレーニングフレームワークであるCAREを提案する。
CAREは正確さを改善し、スムーズさをトレーニングすると同時に、障害からの学習信号のシェアを明示的に増やします。
論文 参考訳（メタデータ） (2025-12-22T16:34:21Z) - Long-Form Information Alignment Evaluation Beyond Atomic Facts [60.25969380388974]
明示的な幻覚を導入することなく、真理のステートメントを"モンテージ"することで、偽りの物語を構築するベンチマークであるMontageLieを紹介します。
本稿では,事実の正確性とイベント順序の整合性を共同で検証する新しいフレームワークであるDoveScoreを提案する。
論文 参考訳（メタデータ） (2025-05-21T17:46:38Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - FactCHD: Benchmarking Fact-Conflicting Hallucination Detection [64.4610684475899]
FactCHD は LLM からファクトコンフリクトの幻覚を検出するために設計されたベンチマークである。
FactCHDは、バニラ、マルチホップ、比較、セット操作など、さまざまな事実パターンにまたがる多様なデータセットを備えている。
Llama2 に基づくツール強化 ChatGPT と LoRA-tuning による反射的考察を合成する Truth-Triangulator を提案する。
論文 参考訳（メタデータ） (2023-10-18T16:27:49Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳（メタデータ） (2023-06-27T17:05:32Z) - Prolog Technology Reinforcement Learning Prover [0.6445605125467572]
ツールキットの中核はコンパクトで容易にPrologベースの自動定理証明であるplCoPである。
plCoPは、LeadCoP Prologの実装に基づいて構築されており、rlCoPシステムで実施された学習誘導のMonte-Carlo Tree Searchを追加している。
その他のコンポーネントには、plCoPとマシン学習者のPythonインターフェース、plCoP証明の有効性を検証する外部証明チェッカーなどがある。
論文 参考訳（メタデータ） (2020-04-15T10:52:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。