論文の概要: Conjecturing: An Overlooked Step in Formal Mathematical Reasoning

• arxiv url: http://arxiv.org/abs/2510.11986v1
• Date: Mon, 13 Oct 2025 22:29:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-15 19:02:32.108997
• Title: Conjecturing: An Overlooked Step in Formal Mathematical Reasoning
• Title（参考訳）: 推論:形式的数学的推論における見過ごされたステップ
• Authors: Jasivan Alex Sivakumar, Philipp Borchert, Ronald Cardenas, Gerasimos Lampouras,
• Abstract要約: 結論を導かない限り、多くの数学的問題は直接形式化できない。 本研究では,大規模言語モデルの導出能力を測定するためにConjectureBenchを開発した。 提案手法は,GPT-4.1と7とDeepSeek-V3.1の13のPutnamBench問題において,最初のエンドツーエンドの自動形式化を実現する。
• 参考スコア（独自算出の注目度）: 10.398167568549924
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalisation, the task of expressing informal mathematical statements in formal language, is often viewed as a direct translation process. This, however, disregards a critical preceding step: conjecturing. Many mathematical problems cannot be formalised directly without first conjecturing a conclusion such as an explicit answer, or a specific bound. Since Large Language Models (LLMs) already struggle with autoformalisation, and the evaluation of their conjecturing ability is limited and often entangled within autoformalisation or proof, it is particularly challenging to understand its effect. To address this gap, we augment existing datasets to create ConjectureBench, and redesign the evaluation framework and metric specifically to measure the conjecturing capabilities of LLMs both as a distinct task and within the autoformalisation pipeline. Our evaluation of foundational models, including GPT-4.1 and DeepSeek-V3.1, reveals that their autoformalisation performance is substantially overestimated when the conjecture is accounted for during evaluation. However, the conjecture should not be assumed to be provided. We design an inference-time method, Lean-FIRe to improve conjecturing and autoformalisation, which, to the best of our knowledge, achieves the first successful end-to-end autoformalisation of 13 PutnamBench problems with GPT-4.1 and 7 with DeepSeek-V3.1. We demonstrate that while LLMs possess the requisite knowledge to generate accurate conjectures, improving autoformalisation performance requires treating conjecturing as an independent task, and investigating further how to correctly integrate it within autoformalisation. Finally, we provide forward-looking guidance to steer future research toward improving conjecturing, an overlooked step of formal mathematical reasoning.
• Abstract（参考訳）: 形式言語で非公式な数学的ステートメントを表現するタスクであるオートフォーマル化は、直接翻訳プロセスと見なされることが多い。 しかし、これは批判的な先行ステップを無視している。 多くの数学的問題は、明示的な答えや特定の境界といった結論を導出しない限り、直接形式化することはできない。 大規模言語モデル(LLM)は自己形式化にすでに苦労しており、その導出能力の評価は限定的であり、しばしば自己形式化や証明に絡み合っているため、その効果を理解することは特に困難である。 このギャップに対処するため、既存のデータセットを拡張してConjectureBenchを作成し、評価フレームワークとメトリクスを再設計し、異なるタスクと自動形式化パイプラインの両方でLLMの導出能力を測定する。 GPT-4.1 や DeepSeek-V3.1 を含む基礎モデルの評価は,評価中に予想が考慮された場合,その自己形式化性能が著しく過大評価されていることを示す。 しかし、この予想は提示されるべきではない。 GPT-4.1とDeepSeek-V3.1で13のPatnamBench問題の最初のエンドツーエンドのオートフォーマル化を実現した、推論時メソッドであるLean-FIREを設計しました。 LLMは正確な予想を生成するために必要な知識を持っているが、自己形式化性能を向上させるには、導出処理を独立したタスクとして扱うことが必要であり、自動形式化において正しく統合する方法をさらに検討する必要がある。 最後に,フォーマルな数学的推論の見過ごされたステップである導出性向上に向けた今後の研究を支援するために,先進的なガイダンスを提供する。

関連論文リスト

• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
  大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。 しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。 機械学習の基礎理論に基づいて構築された、リーン4ベンチマークであるFormalMLを紹介します。
  論文  参考訳（メタデータ） (2025-09-26T14:40:14Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。 最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。 本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
  論文  参考訳（メタデータ） (2025-09-02T14:16:02Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning [8.135142928659546]
  自動形式化タスクを評価するための,体系的かつ自動的な手法を提案する。 提案手法は,論理的保存(LP),数学的整合性(MC),形式的妥当性(FV),形式的品質(FQ)を基準とした審査員のアンサンブルに基づく。 全体としては,LLM審査員のEFGアンサンブルが評価に好適であることを示す。
  論文  参考訳（メタデータ） (2025-06-12T17:09:51Z)
• CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
  我々は,系統的かつ包括的な推論プロセスを実行するためのモデルを導くことで,モデルがよりきめ細やかで正確な絞り込み決定を実行できることを提案する。 我々は,(i)クレームの分解,(ii)サブクレームの属性と包含分類,および(iii)集約分類から成る3段階の推論プロセスを定義し,そのような導出推論が実際に幻覚検出の改善をもたらすことを示す。
  論文  参考訳（メタデータ） (2025-06-05T17:02:52Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Improving Autoformalization using Type Checking [15.58948808529849]
  我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• Autoformalization with Large Language Models [22.86710743804944]
  自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。 大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。 我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
  論文  参考訳（メタデータ） (2022-05-25T09:53:30Z)

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

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