論文の概要: Learning to Discover Interesting Mathematics

• arxiv url: http://arxiv.org/abs/2609.28603v1
• Date: Wed, 23 Sep 2026 16:06:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-25 21:10:09.439089
• Title: Learning to Discover Interesting Mathematics
• Title（参考訳）: 興味をそそる数学の学習
• Abstract要約: 定理の本質的な面白さを、その証明の長さと主張の長さの比として定義する。 我々は、フロンティア汎用モデルよりも正確な証明困難を予測できる27Bモデルを訓練する。 提案システムでは, 仮説の候補を生成でき, その中の最も興味深いものを選択し, 自己拡張型数学的ライブラリ上に反復的に構築できることが示される。
• 参考スコア（独自算出の注目度）: 14.533761950304246
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including many that have been open for decades. This opens the door to expansion of mathematical knowledge at unprecedented scale. Yet, while LLMs may be able to conjecture and prove more and more theorems, it remains open whether this new mathematical knowledge is interesting or useful. We define intrinsic interestingness of a theorem as the ratio between the length of its proof and the length of its statement. We show that this correlates strongly with an extrinsic measure of the downstream utility of a theorem. We identify the difficulty of a proof conditioned on a set of premises as a useful primitive for computing these metrics, and train a 27B model that predicts proof difficulty more accurately than frontier general-purpose models. Optimizing for our metric creates a model capable of producing more interesting theorems, while also reducing substantial or full overlap with Mathlib from 91.9% to 30.6%, showcasing the creation of more out-of-distribution math. We show that our system can generate candidate theorems, select the most interesting among them, and iteratively build on a self-expanding mathematical library. These metrics provide a practical and quantifiable signal for ranking conjectures and guiding proof search within formal mathematical libraries. Our framework provides a path towards self-expanding, machine-verified mathematical libraries that can choose worthwhile statements without relying on human-supplied targets.
• Abstract（参考訳）: 近年、Large Language Models (LLMs) は、何十年にもわたって開かれているものを含め、高度な数学的問題を解くことができるようになっている。 これは前例のない規模の数学的知識の拡大への扉を開く。 しかし、LSMは予想し、より多くの定理を証明できるかもしれないが、この新しい数学的知識が興味深いか有用かは明らかではない。 定理の本質的な面白さを、その証明の長さと主張の長さの比として定義する。 これは定理の下流効用に関する外生測度と強く相関していることを示す。 本研究では,これらの指標の計算に有用なプリミティブとして,一組の前提で条件を定めている証明の難しさを特定し,フロンティア汎用モデルよりも正確な証明難度を予測する27Bモデルを訓練する。 我々の計量の最適化は、より興味深い定理を生成できるモデルを作成すると同時に、Mathlibとの実質的あるいは完全な重複を91.9%から30.6%に減らし、よりアウト・オブ・ディストリビューションな数学の創出を示す。 提案システムでは, 仮説の候補を生成でき, そのうち最も興味深いものを選択し, 自己拡張数学ライブラリ上に反復的に構築できることが示される。 これらの測度は、予想をランク付けし、公式な数学的ライブラリー内の証明探索を導くための実用的で定量的な信号を提供する。 我々のフレームワークは、人間に供給された目標に頼らずに価値ある文を選択できる、自己拡張的でマシン検証された数学的ライブラリへの道を提供する。

関連論文リスト

• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  AI4Mathシステムの次の飛躍は、事前に定義された問題解決者から研究エージェントへの決定的なシフトを必要とする。 この分野の体系的なレビューを行い、データセット、自動形式化、証明合成について紹介する。
  論文  参考訳（メタデータ） (2026-07-08T17:46:36Z)
• Self-Supervised Theorem Discovery in a Formal Axiomatic System [44.603295025494674]
  エージェントが、そのような先入観のない有用な定理を自律的に発見できるかどうかを考察する。 本稿では,証明探索と有用な定理抽出を交互に行う自己教師付き定理発見アルゴリズムを提案する。 本結果は,人為的な定理ライブラリに頼らずに,有用な定理が証明探索から現れることを示すものである。
  論文  参考訳（メタデータ） (2026-06-27T05:55:18Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [75.95179490687018]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
  ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。 制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。 我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
  論文  参考訳（メタデータ） (2024-06-30T13:34:54Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Machine learning and information theory concepts towards an AI Mathematician [77.63761356203105]
  人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。 このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。 興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
  論文  参考訳（メタデータ） (2024-03-07T15:12:06Z)
• MathScale: Scaling Instruction Tuning for Mathematical Reasoning [70.89605383298331]
  大規模言語モデル(LLM)は問題解決において顕著な能力を示した。 しかし、数学的な問題を解く能力は依然として不十分である。 高品質な数学的推論データを作成するためのシンプルでスケーラブルな方法であるMathScaleを提案する。
  論文  参考訳（メタデータ） (2024-03-05T11:42:59Z)
• Automated Search for Conjectures on Mathematical Constants using Analysis of Integer Sequences [0.0]
  基本的な数学的定数を含む公式は、科学と数学の様々な分野に大きな影響を与えた。 ラマヌジャン機械計画のような数学定数の公式の発見を自動化しようとする最近の試みは、徹底的な探索に依存していた。 ここでは、整数列の解析を通して、数学的定数の予想を探索する根本的に異なる方法を提案する。
  論文  参考訳（メタデータ） (2022-12-13T18:01:21Z)

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

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