論文の概要: Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study
- arxiv url: http://arxiv.org/abs/2608.05420v1
- Date: Wed, 05 Aug 2026 21:29:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-07 15:25:20.78792
- Title: Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study
- Title（参考訳）: オープンウェイトLLMはカーネル認証コーク証明を生成できるか? : 実験的検討
- Abstract要約: 大規模言語モデル(LLM)は数学的証明に類似したテキストを生成することができるが、類似性は正確性を確立しない。
Coqのルールは、システムのどの証明ステップが受け入れられるかを定義する論理的フレームワークであるCalculus of Inductive Constructionsに基づいている。
このパイロット研究は、実際のCoqプロジェクトから派生したベンチマークであるCoqStoqから、同じ100の定理で6つのオープンウェイトLSMを評価した。
- 参考スコア（独自算出の注目度）: 0.20415910628419062
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models (LLMs) can generate text that resembles a mathematical proof, but resemblance does not establish correctness. A formal proof checker verifies whether each proof step follows established logical rules. Coq bases its rules on the Calculus of Inductive Constructions, a logical framework that defines which proof steps the system may accept. This pilot study evaluated six open-weight LLMs on the same 100 theorems from CoqStoq, a benchmark derived from real Coq projects. Each LLM received one attempt per theorem with the temperature set to 0, and Coq checked every proposed proof in the theorem's original project environment. We counted a proof as successful only if the Coq kernel accepted it. Gemma 4 verified 12 of 100 theorems, Llama 3.3 verified 8, and DeepSeek Coder V2 Lite verified 1. Qwen 3.5, Mistral Small 3.1, and GPT-OSS verified none. The 21 successful model-theorem results covered 15 distinct theorems, 11 of which were not solved by a baseline of standard Coq tactics. All verified theorems had short or medium human-written reference proofs; no model verified a theorem with a long reference proof. Because the proof-length analysis was exploratory, this pattern does not establish that proof length caused the difference. For the three models with at least one success, the total generation cost per verified proof ranged from 741 to 36,193 output tokens, 14.9 to 178.0 seconds, and 0.0167 to 0.2000 aggregate GPU hours. We could not calculate these ratios for models with no verified proofs. Across 600 attempts, the models produced 21 kernel-verified proofs, giving an overall success rate of 3.5%. The study reports descriptive differences among the models but does not statistically test whether one model outperforms another. Therefore, the results do not establish a universal ranking of the six models.
- Abstract（参考訳）: 大規模言語モデル(LLM)は数学的証明に類似したテキストを生成することができるが、類似性は正確性を確立しない。
形式的証明チェッカーは、各証明ステップが確立された論理規則に従うか否かを検証する。
Coqのルールは、システムのどの証明ステップが受け入れられるかを定義する論理的フレームワークであるCalculus of Inductive Constructionsに基づいている。
このパイロット研究は、実際のCoqプロジェクトから派生したベンチマークであるCoqStoqから、同じ100の定理で6つのオープンウェイトLSMを評価した。
各 LLM は、温度を 0 に設定した1つの定理の試行を受け、コークは、定理の元々のプロジェクト環境における全ての提案された証明を確認した。
証明が成功したのは、Coqカーネルがそれを受け入れた時だけです。
Gemma 4は100の定理のうち12を、Llama 3.3は8を、DeepSeek Coder V2 Liteは1を検証した。
Qwen 3.5, Mistral Small 3.1, GPT-OSSは確認されなかった。
21個のモデル理論の結果は15個の異なる定理をカバーし、そのうち11個は標準の Coq 戦術のベースラインでは解けなかった。
検証されたすべての定理は、短いあるいは中程度の人間の記述された参照証明を持ち、長い参照証明を持つ定理を検証したモデルはない。
証明長解析は探索的であったため、このパターンは証明長が差を引き起こしたことを証明していない。
少なくとも1つの成功を収めた3つのモデルでは、検証された証明当たりの総生成コストは741から36,193の出力トークン、14.9から178.0秒、0.0167から0.2000のGPU時間であった。
確証のないモデルでは、これらの比率を計算できなかった。
600回の試験で21個のカーネル検証証明が作成され、全体の成功率は3.5%となった。
この研究は、モデル間で記述的差異を報告しているが、あるモデルが他のモデルより優れているかどうか統計的に検証していない。
したがって、結果は6つのモデルの普遍的なランキングを定めていない。
関連論文リスト
- Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
大規模言語モデル(LLM)は、自動的に証明を生成することを約束するが、既存のアプローチは、固定された人間設計の証明戦略をシステムに結び付ける。
このような戦略を課すことは不要で制限的であることを示す。
レムマ全体を一般的なコードエージェントに手渡して、独自のアプローチを自由に選択し、検証ハーネスにラップすることは、シンプルでより効果的です。
論文 参考訳（メタデータ） (2026-07-07T14:39:59Z) - MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving [0.0]
MerLean-Proverは、残念な宣言をカーネルチェック可能な証明に置き換える、エンドツーエンドのLean4定理証明器である。
23のPhD-qualification-exam定理のベンチマークであるFormalQualBenchでは、MerLean-Proverは10/23を解く。
Sonnetは4つのテストされたFormalQualBench問題を全てクローズし、Haikuは2つの短い問題をクローズする。
論文 参考訳（メタデータ） (2026-05-26T12:49:49Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - Mathematics with large language models as provers and verifiers [1.1029146548022293]
ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数理論の予想の約3分の1を閉じる。
論文 参考訳（メタデータ） (2025-10-11T20:35:25Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。
我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。
我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
論文 参考訳（メタデータ） (2024-11-04T05:57:40Z) - Proof Automation with Large Language Models [6.587933406842906]
大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。
本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。
その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
論文 参考訳（メタデータ） (2024-09-22T00:19:27Z) - DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。
この合成データセットでDeepSeekMath 7Bモデルを微調整します。
我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文 参考訳（メタデータ） (2024-05-23T09:03:42Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。