Fugu-MT 論文翻訳(概要): Evaluation of LLMs for Mathematical Formalization in Lean

論文の概要: 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の評価
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$であった。

関連論文リスト

The Embedder's Dilemma: LLMs Are Better, but at What Cost? [18.755750863102232]
10のテキスト埋め込みモデルと26の埋め込みモデルを比較した。最良のLLM(Gemini 3.1 Pro)と最高の埋め込みモデル(77.2)は0.4ポイント異なる。本研究は, 類似性, 分類, クラスタリングのための埋め込みモデルと, 推論集約検索のための予備LLMを用いて, 作業の分割を支援する。
論文参考訳（メタデータ） (2026-08-13T06:39:45Z)
MentorCollab: Selective Large-to-Small Inference-Time Guidance for Efficient Reasoning [85.05204262206296]
大きな推論モデル(LRM)は、長い思考の連鎖を生成することによって、強い性能を達成するが、その推論コストは高い。小型言語モデル(SLM)はより効率的であるが、多段階推論タスクでは困難である。本研究では, LRM が SLM を選択的かつ簡潔にガイドする推論時協調手法である MentorCollab を提案する。
論文参考訳（メタデータ） (2026-02-05T04:58:16Z)
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)
MiniCPM-V 4.5: Cooking Efficient MLLMs via Architecture, Data, and Training Recipe [68.04078852416248]
MiniCPM-V 4.5は8Bパラメータモデルであり、高効率で高性能に設計されている。本稿では,モデルアーキテクチャ,データストラテジー,トレーニング手法の3つの改良点を紹介する。 MiniCPM-V 4.5は30B以下のモデル間で最先端の性能を達成する。
論文参考訳（メタデータ） (2025-09-16T19:41:48Z)
ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文参考訳（メタデータ） (2025-01-30T12:37:06Z)
Control LLM: Controlled Evolution for Intelligence Retention in LLM [4.67235851066221]
並列事前学習および拡張トランスブロックを利用した新しいアプローチである textbfControl LLM を提案する。 CPT(Continuous Pre-Training)とCSFT(Continuous Supervised Fine-Tuning)における制御LDMの有効性を示す実験既存の手法を超越し、同じベースモデルからチューニングされたオープンソースモデルの中でSOTAを実現する。
論文参考訳（メタデータ） (2025-01-19T08:06:06Z)
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)
CPM-2: Large-scale Cost-effective Pre-trained Language Models [71.59893315671997]
本稿では, PLM を用いた事前学習, 微調整, 推論の効率性問題に対処するための費用対効果技術について述べる。我々は,既存のPLMをスクラッチからトレーニングする代わりに活用することで,事前学習プロセスの促進を目的とした知識継承を導入する。計算資源が限られている大規模PLMに対して,新しい推論ツールキット,すなわちInfMoEを実装した。
論文参考訳（メタデータ） (2021-06-20T15:43:54Z)

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