論文の概要: FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory

• arxiv url: http://arxiv.org/abs/2510.02335v1
• Date: Fri, 26 Sep 2025 14:40:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-06 16:35:52.009306
• Title: FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
• Title（参考訳）: FormalML: 機械学習理論における形式的サブゴナル補完の評価ベンチマーク
• Authors: Xiao-Wen Yang, Zihao Zhang, Jianuo Cao, Zhi Zhou, Zenan Li, Lan-Zhe Guo, Yuan Yao, Taolue Chen, Yu-Feng Li, Xiaoxing Ma,
• Abstract要約: 大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。 しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。 機械学習の基礎理論に基づいて構築された、リーン4ベンチマークであるFormalMLを紹介します。
• 参考スコア（独自算出の注目度）: 44.64175433092553
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have recently demonstrated remarkable progress in formal theorem proving. Yet their ability to serve as practical assistants for mathematicians, filling in missing steps within complex proofs, remains underexplored. We identify this challenge as the task of subgoal completion, where an LLM must discharge short but nontrivial proof obligations left unresolved in a human-provided sketch. To study this problem, we introduce FormalML, a Lean 4 benchmark built from foundational theories of machine learning. Using a translation tactic that converts procedural proofs into declarative form, we extract 4937 problems spanning optimization and probability inequalities, with varying levels of difficulty. FormalML is the first subgoal completion benchmark to combine premise retrieval and complex research-level contexts. Evaluation of state-of-the-art provers highlights persistent limitations in accuracy and efficiency, underscoring the need for more capable LLM-based theorem provers for effective subgoal completion,
• Abstract（参考訳）: 大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。 しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。 我々はこの課題を,人為的なスケッチに残されている未解決の証明義務を,LLMが短時間で退避しなければならないサブゴール完了の課題とみなす。 この問題を解決するために,機械学習の基礎理論に基づいて構築された,リーン4ベンチマークであるFormalMLを紹介した。 手続き的証明を宣言形式に変換する翻訳手法を用いて、最適化と確率不等式にまたがる4937の問題を、様々な難易度で抽出する。 FormalMLは、前提検索と複雑な研究レベルのコンテキストを組み合わせた最初のサブゴール補完ベンチマークである。 最先端のプローバーの評価では、精度と効率の持続的な制限が強調され、より有能なLLMベースの定理プローバーが効果的なサブゴール完備のために必要であることを示す。

関連論文リスト

• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• InductionBench: LLMs Fail in the Simplest Complexity Class [53.70978746199222]
  大規模言語モデル(LLM)は推論において顕著に改善されている。 帰納的推論(inductive reasoning)は、観測されたデータから基礎となるルールを推測するものであり、まだ探索されていない。 本稿では, LLMの帰納的推論能力を評価するための新しいベンチマークであるインジェクションベンチを紹介する。
  論文  参考訳（メタデータ） (2025-02-20T03:48:00Z)
• SubgoalXL: Subgoal-based Expert Learning for Theorem Proving [37.115856591703974]
  SubgoalXLは、正規の定理証明を強化するために、専門家の学習とサブゴールベースの証明を相乗化する新しいアプローチである。 SubgoalXLは、標準のminiF2Fデータセット上で、Isabelleで56.1%の最先端パフォーマンスを実現する。
  論文  参考訳（メタデータ） (2024-08-20T20:10:53Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。