論文の概要: Advancing Mathematical Research via Human-AI Interactive Theorem Proving

• arxiv url: http://arxiv.org/abs/2512.09443v2
• Date: Thu, 11 Dec 2025 13:10:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-12 14:11:15.287639
• Title: Advancing Mathematical Research via Human-AI Interactive Theorem Proving
• Title（参考訳）: 人間-AIインタラクティブな理論証明による数学的研究の促進
• Authors: Chenyi Li, Zhijian Lai, Dong An, Jiang Hu, Zaiwen Wen,
• Abstract要約: LLMを用いた対話型定理証明と発見のためのヒューマン・イン・ザ・ループ・ワークフローを提案する。 人間の専門家は問題定式化と許容可能な仮定の制御を維持し、モデルは証明や矛盾を探索する。 このワークフローを、多様体最適化とグロバーの量子探索アルゴリズムの接続に関するケーススタディでインスタンス化する。
• 参考スコア（独自算出の注目度）: 16.40852561664514
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We investigate how large language models can be used as research tools in scientific computing while preserving mathematical rigor. We propose a human-in-the-loop workflow for interactive theorem proving and discovery with LLMs. Human experts retain control over problem formulation and admissible assumptions, while the model searches for proofs or contradictions, proposes candidate properties and theorems, and helps construct structures and parameters that satisfy explicit constraints, supported by numerical experiments and simple verification checks. Experts treat these outputs as raw material, further refine them, and organize the results into precise statements and rigorous proofs. We instantiate this workflow in a case study on the connection between manifold optimization and Grover's quantum search algorithm, where the pipeline helps identify invariant subspaces, explore Grover-compatible retractions, and obtain convergence guarantees for the retraction-based gradient method. The framework provides a practical template for integrating large language models into frontier mathematical research, enabling faster exploration of proof space and algorithm design while maintaining transparent reasoning responsibilities. Although illustrated on manifold optimization problems in quantum computing, the principles extend to other core areas of scientific computing.
• Abstract（参考訳）: 数学的厳密さを保ちながら,科学計算における研究ツールとして大規模言語モデルをどのように利用できるかを検討する。 LLMを用いた対話型定理証明と発見のためのヒューマン・イン・ザ・ループ・ワークフローを提案する。 人間の専門家は問題定式化と許容可能な仮定の制御を維持し、モデルは証明や矛盾を探索し、候補となる性質と定理を提案し、数値実験と単純な検証チェックによって支持される明示的な制約を満たす構造とパラメータの構築を支援する。 専門家はこれらのアウトプットを原料として扱い、さらに精製し、結果を正確なステートメントと厳密な証明に整理する。 このワークフローは、多様体最適化とGroverの量子探索アルゴリズムの接続に関するケーススタディでインスタンス化され、パイプラインは不変部分空間の同定を支援し、Grover互換のリトラクションを探索し、リトラクションに基づく勾配法に対する収束保証を得る。 このフレームワークは、大きな言語モデルをフロンティア数学の研究に統合するための実用的なテンプレートを提供し、透明な推論責任を維持しつつ、証明空間とアルゴリズム設計の迅速な探索を可能にする。 量子コンピューティングにおける多様体最適化問題について説明されているが、原理は科学計算の他の中心領域にまで及んでいる。

関連論文リスト

• Where to Search: Measure the Prior-Structured Search Space of LLM Agents [0.8249180979158818]
  本稿では、LLM支援反復探索をドメイン先導で記述し、評価するコンパクトな形式理論を提案する。 エージェントをファジィ関係演算子として入力と出力を表現し、実現可能な遷移をキャプチャする。 最も単純なテスト可能な推論を提供し、それらを2つのインスタンス化によって検証する。
  論文  参考訳（メタデータ） (2025-10-16T16:18:37Z)
• The Computational Complexity of Circuit Discovery for Inner Interpretability [0.30723404270319693]
  我々は古典的およびパラメータ化された計算複雑性理論を用いて回路発見を研究する。 私たちの発見は、難しい複雑さの風景を明らかにします。 このフレームワークは、解釈可能性クエリの範囲と限界を理解するのに役立ちます。
  論文  参考訳（メタデータ） (2024-10-10T15:22:48Z)
• Token-Supervised Value Models for Enhancing Mathematical Problem-Solving Capabilities of Large Language Models [56.32800938317095]
  既存の検証器はテスト時の木探索技術に準最適である。 トークン制御値モデル(TVM)を提案する。 TVMは各トークンに、正しい最終回答に達する確率を反映した確率を割り当てる。
  論文  参考訳（メタデータ） (2024-07-12T13:16:50Z)
• Efficient Model-Free Exploration in Low-Rank MDPs [76.87340323826945]
  低ランクマルコフ決定プロセスは、関数近似を持つRLに対して単純だが表現力のあるフレームワークを提供する。 既存のアルゴリズムは、(1)計算的に抽出可能であるか、または(2)制限的な統計的仮定に依存している。 提案手法は,低ランクMPPの探索のための最初の実証可能なサンプル効率アルゴリズムである。
  論文  参考訳（メタデータ） (2023-07-08T15:41:48Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  本研究は,NFに基づく多次元条件(後)密度推定器の検証診断を容易にすることを提案する。 また、局所的な一貫性の結果に基づいた理論的保証も提供する。 この作業は、より良い特定モデルの設計を支援したり、新しいSBIアルゴリズムの開発を促進するのに役立つだろう。
  論文  参考訳（メタデータ） (2022-11-17T15:48:06Z)
• Amortized Inference for Causal Structure Learning [72.84105256353801]
  因果構造を学習することは、通常、スコアまたは独立テストを使用して構造を評価することを伴う探索問題を引き起こす。 本研究では,観測・干渉データから因果構造を予測するため,変分推論モデルを訓練する。 我々のモデルは、実質的な分布シフトの下で頑健な一般化能力を示す。
  論文  参考訳（メタデータ） (2022-05-25T17:37:08Z)
• Partial Counterfactual Identification from Observational and Experimental Data [83.798237968683]
  観測データと実験データの任意の組み合わせから最適境界を近似する有効なモンテカルロアルゴリズムを開発した。 我々のアルゴリズムは、合成および実世界のデータセットに基づいて広範囲に検証されている。
  論文  参考訳（メタデータ） (2021-10-12T02:21:30Z)
• Fractal Structure and Generalization Properties of Stochastic Optimization Algorithms [71.62575565990502]
  最適化アルゴリズムの一般化誤差は、その一般化尺度の根底にあるフラクタル構造の複雑性'にバウンドできることを示す。 さらに、特定の問題(リニア/ロジスティックレグレッション、隠れ/層ニューラルネットワークなど)とアルゴリズムに対して、結果をさらに専門化します。
  論文  参考訳（メタデータ） (2021-06-09T08:05:36Z)

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

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