論文の概要: Evaluation of LLMs for Mathematical Formalization in Lean
- arxiv url: http://arxiv.org/abs/2606.05632v1
- Date: Thu, 04 Jun 2026 02:59:39 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-05 22:39:44.510602
- Title: Evaluation of LLMs for Mathematical Formalization in Lean
- Title（参考訳）: リーンにおける数学的形式化のためのLCMの評価
- Authors: Tyson Klingner, Drew Bladek, Escher Crawford, Bohao Chen, Ariel Fu, Kaira Nair, Jarod Alper, Giovanni Inchiostro, Vasily Ilin,
- Abstract要約: リーン4.1では、さまざまな大規模言語モデルの有効性を公式な証明で比較しています。
総合的には、Gemini 3.1 ProとClaude Opus 4.7が最高である。
コストを考慮すると、NVIDIA Nemotron 3 SuperとGPT-OSS 120Bが最も効率的だった。
- 参考スコア（独自算出の注目度）: 5.016022722613884
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@$k$ and refine@$k$ metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92\% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86\% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of $<\$0.01$ per correct proof.
- Abstract（参考訳）: 過去数年間の間に、公式な数学的証明を生成する大規模言語モデル(LLM)の能力は大幅に向上した。
リーン4で公式な証明を生成する上で,さまざまなLLMの有効性と,自身のプロジェクトをサポートするためにLLMを使用する人々を支援することの目標を比較した。
pass@$k$ と refine@$k$ の両方を比較のためのベンチマークとして使用し、miniF2F と miniCTX のデータセットのサブセットを評価します。
我々のテストでは、Gemini 3.1 ProとClaude Opus 4.7が最高のパフォーマンスを示している。
Gemini 3.1 Pro は refine@32 で miniF2F で 92 % の成功率を達成したが、 Opus 4.7 は refine@32 で miniCTX で 86 % の成功率を達成した。
コストを考慮すると、NVIDIA Nemotron 3 SuperとGPT-OSS 120Bが最も効率的で、競争力のある精度と平均コストは正しい証明1つあたり$<\$0.01$であった。
関連論文リスト
- MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification [0.5753241925582828]
数学的推論ベンチマーク miniF2F の最初の翻訳である miniF2F-Dafny を自動定理証明器に提示する。
Dafnyの自動化はテストセットの99/244 (40.6%) と検証セットの109/244 (44.7%) を空の証明で検証する。
論文 参考訳（メタデータ） (2025-12-11T00:52:19Z) - Dr. SoW: Density Ratio of Strong-over-weak LLMs for Reducing the Cost of Human Annotation in Preference Tuning [15.776175440446414]
本稿では,人間のアノテーションへの依存を解消するコスト効率の高い方法であるDr.SoW(Density Ratio of Strong over Weak)を紹介する。
Dr.SoW は報奨信号として、より整列した LLM と低整列の LLM の対数密度比を用いる。
Dr.SoWによるデータを用いたLlama-3-8B-インストラクタを選好する。
論文 参考訳（メタデータ） (2024-11-04T18:54:39Z) - Closing the gap between open-source and commercial large language models for medical evidence summarization [20.60798771155072]
大規模言語モデル(LLM)は、医学的証拠の要約において大きな可能性を秘めている。
最近の研究は、プロプライエタリなLLMの応用に焦点を当てている。
オープンソースのLLMは透明性とカスタマイズを向上するが、そのパフォーマンスはプロプライエタリなものに比べて低下する。
論文 参考訳（メタデータ） (2024-07-25T05:03:01Z) - Inference-Time Decontamination: Reusing Leaked Benchmarks for Large Language Model Evaluation [61.350306618479365]
ベンチマークの漏洩は、大規模言語モデルの真のパフォーマンスの正確な評価を防ぐことができる。
この問題に対処するため,ITD(Inference-Time Decontamination)を提案する。
ITDは、GSM8Kで22.9%、MMLUで19.0%の膨張精度を低下させる。
論文 参考訳（メタデータ） (2024-06-20T04:35:59Z) - How Far Are We on the Decision-Making of LLMs? Evaluating LLMs' Gaming Ability in Multi-Agent Environments [83.78240828340681]
GAMA($gamma$)-Benchは、マルチエージェント環境における大規模言語モデルのゲーム能力を評価するための新しいフレームワークである。
$gamma$-Benchは8つの古典ゲーム理論シナリオと、LSMの性能を評価するために特別に設計された動的スコアリングスキームを含んでいる。
以上の結果から, GPT-3.5は強い強靭性を示すが, 一般化性は限定的であり, Chain-of-Thoughtのような手法で拡張可能であることが示唆された。
論文 参考訳（メタデータ） (2024-03-18T14:04:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。