論文の概要: Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterization with ChatGPT-5.2 (Thinking)

• arxiv url: http://arxiv.org/abs/2602.18918v1
• Date: Sat, 21 Feb 2026 17:52:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-24 17:42:02.396278
• Title: Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterization with ChatGPT-5.2 (Thinking)
• Title（参考訳）: 消費者LCMを用いたウイルス生産の早期証拠:ChatGPT-5.2を用いたスペクトル領域解析の事例研究(シンキング)
• Abstract要約: 消費者定期購読型Large Language Models (LLMs) を用いたバイブプロビテーションの証拠を示す。 7つの共有可能なChatGPT-5.2スレッドと4つのバージョン付きの証明ドラフトを分析し、生成、参照、修正の反復パイプラインを文書化する。 このモデルは高いレベルの証明探索には最も有用であるが、人間の専門家は正当性クリティカルなクロージャには不可欠である。
• 参考スコア（独自算出の注目度）: 3.8922083220688393
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Large Language Models (LLMs) are increasingly used as scientific copilots, but evidence on their role in research-level mathematics remains limited, especially for workflows accessible to individual researchers. We present early evidence for vibe-proving with a consumer subscription LLM through an auditable case study that resolves Conjecture 20 of Ran and Teng (2024) on the exact nonreal spectral region of a 4-cycle row-stochastic nonnegative matrix family. We analyze seven shareable ChatGPT-5.2 (Thinking) threads and four versioned proof drafts, documenting an iterative pipeline of generate, referee, and repair. The model is most useful for high-level proof search, while human experts remain essential for correctness-critical closure. The final theorem provides necessary and sufficient region conditions and explicit boundary attainment constructions. Beyond the mathematical result, we contribute a process-level characterization of where LLM assistance materially helps and where verification bottlenecks persist, with implications for evaluation of AI-assisted research workflows and for designing human-in-the-loop theorem proving systems.
• Abstract（参考訳）: 大規模言語モデル (LLMs) は、科学的コパイロットとしてますます使われているが、研究レベルの数学におけるそれらの役割に関する証拠は、特に個々の研究者が利用できるワークフローに対して限られている。 我々は,4サイクルの行確率非負行列系列の正確な非実スペクトル領域について,RanとTeng(2024)の帰納法20を解決した監査可能なケーススタディを通じて,消費者サブスクリプションLLMを用いたバイブプロファイリングの早期証拠を提示する。 7つの共有可能なChatGPT-5.2スレッドと4つのバージョン付きの証明ドラフトを分析し、生成、参照、修正の反復パイプラインを文書化する。 このモデルは高いレベルの証明探索に最も有用であるが、人間の専門家は正確性に批判的なクロージャに不可欠である。 最終的な定理は、必要かつ十分な領域条件と明示的な境界到達構成を提供する。 数学的な結果の他に,LLM 支援が有効な点や,検証ボトルネックが持続する点のプロセスレベルの特徴付けや,AI 支援研究ワークフローの評価,ループ型定理証明システムの設計などにも寄与する。

関連論文リスト

• NovGauge: A Fine-Grained Benchmark for Diagnosing LLMs' Capability in Paper Novelty Assessment [54.4265627247104]
  大規模言語モデル(LLM)は、主要なAIカンファレンスでピアレビューでますます使用されている。 既存のベンチマークでは、ノベルティを1つの総合的なスコアとして評価している。 本報告では,詳細なノベルティアセスメント診断のための人手によるベンチマークであるNovGaugeについて述べる。
  論文  参考訳（メタデータ） (2026-09-10T08:34:56Z)
• Self-prompting and cross-model consensus enable reproducible data extraction from scientific literature with large language models [0.0]
  ブラウザベースの大規模言語モデル(LLM)は、研究論文から高度に文脈化された情報を抽出する。 キュレーションの段階は、専門家によるキュレーションプロンプト、簡単な指示、文献の自律的な発見、新しいデータセットの4つである。 これらの知見は、専門家がエビデンス標準を規定し、モデルが繰り返し抽出を相互チェックし、研究者が紛争の解決を行う、監査可能な労働区分を定義している。
  論文  参考訳（メタデータ） (2026-08-19T15:20:11Z)
• Are LLMs Ready for Scientific Discovery? A Capability-Oriented Benchmark for AI Scientists [5.947663261819682]
  SDABenchは5つの領域(生物、化学、環境、地理、物理)にわたる6つの能力(記述、探索、推論、予測、因果、力学)に関する評価を再編成するベンチマークである。 記述的モデルは解析をうまく処理するが、仮定の選択、潜在プロセスモデリング、あるいは機械的推論を必要とするタスクを著しく分解する。
  論文  参考訳（メタデータ） (2026-07-13T04:39:40Z)
• From Passive Generation to Investigation: A Proactive Scientific Peer Review Agent [52.42081442204093]
  我々は、紙の不審な部分を積極的に調査する柔軟性の欠如が、重要な制限であると主張している。 本稿では,保守的かつ構造化されたレビューログによってガイドされた論文を積極的にレビューする,科学的ピアレビューエージェントであるProReviewerを提案する。 実験の結果,8Bバックボーンを持つProReviewerは教師付き微調整によって訓練され,強化学習によって最適化され,5つの品質次元で最高の平均スコアが得られることがわかった。
  論文  参考訳（メタデータ） (2026-06-11T13:38:23Z)
• Understanding on the Edge: LLM-generated Boundary Test Explanations [4.901543643055091]
  境界値分析とテストは、ソフトウェアの品質保証に不可欠である。 LLMは自然言語の合理性を生み出すのに役立つが、BVTに対するその価値は実証的に評価されていない。 調査では、ソフトウェア専門家が、明確さ、正確性、完全性、有用性に対する20の境界対について、GPT-4.1の説明を評価した。
  論文  参考訳（メタデータ） (2026-01-30T10:11:45Z)
• OpenNovelty: An LLM-powered Agentic System for Verifiable Scholarly Novelty Assessment [63.662126457336534]
  OpenNoveltyは、透明で証拠に基づく新規性分析のためのエージェントシステムである。 回収された実論文のすべての評価を根拠にし、検証可能な判断を確実にする。 OpenNoveltyは、公正で一貫性があり、エビデンスに支えられたピアレビューを促進するスケーラブルなツールで、研究コミュニティに力を与えることを目指している。
  論文  参考訳（メタデータ） (2026-01-04T15:48:51Z)
• Large Language Models in Thematic Analysis: Prompt Engineering, Evaluation, and Guidelines for Qualitative Software Engineering Research [5.0043780915457114]
  大規模言語モデル (LLMs) は定性的な研究に参入しているが、それらを数理解析 (thematic analysis, TA) のような確立されたアプローチに統合するための再現可能な手法は存在しない。 我々はブラウンとクラークの反射性TAの位相2-5のプロンプトを設計・繰り返し改良した。 ブラウンとクラークの品質基準から導出した潤滑剤を応用した4つの専門家評価器を用いてブラインド評価を行った。
  論文  参考訳（メタデータ） (2025-10-21T09:29:18Z)
• FinDeepResearch: Evaluating Deep Research Agents in Rigorous Financial Analysis [110.5695516127813]
  HisRubricは階層的な分析構造ときめ細かいグレーディングルーブリックを備えた新しい評価フレームワークである。 FinDeepResearchは、4つの言語にまたがる8つの金融市場から64の上場企業からなるベンチマークである。 6つのDRエージェント、深い推論能力と探索能力を備えた5つのLLM、深い推論能力を持つ5つのLLMを含む16の代表的な手法を用いてFinDeepResearchに関する広範な実験を行った。
  論文  参考訳（メタデータ） (2025-10-15T17:21:56Z)
• Let's Use ChatGPT To Write Our Paper! Benchmarking LLMs To Write the Introduction of a Research Paper [64.50822834679101]
  SciIGは、タイトル、抽象、および関連する作品からコヒーレントな紹介を生成するLLMの能力を評価するタスクである。 オープンソース (DeepSeek-v3, Gemma-3-12B, LLaMA 4-Maverick, MistralAI Small 3.1) およびクローズドソース GPT-4o システムを含む5つの最先端モデルを評価する。 結果は、特に意味的類似性と忠実性において、ほとんどのメトリクスにおいて、LLaMA-4 Maverickの優れたパフォーマンスを示す。
  論文  参考訳（メタデータ） (2025-08-19T21:11:11Z)
• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)
• Large Language Models for Predictive Analysis: How Far Are They? [6.747160854665847]
  大きな言語モデル(LLM)は、ニュアンスで知識集約的な会話を可能にする強力なツールとして登場した。 我々は,8つの分野からなる44の実世界のデータセットから1130の高度な予測分析クエリを統合する textbfPredictiQ ベンチマークを導入する。 12の有名なLCMが評価され、予測分析における実践的利用に関する洞察を提供する。
  論文  参考訳（メタデータ） (2025-05-22T09:02:15Z)
• CycleResearcher: Improving Automated Research via Automated Review [37.03497673861402]
  本稿では,オープンソースの後学習型大規模言語モデル(LLM)を,自動研究とレビューの全サイクルを遂行する自律エージェントとして活用する可能性について検討する。 これらのモデルをトレーニングするために、現実の機械学習研究とピアレビューダイナミクスを反映した2つの新しいデータセットを開発した。 その結果,CycleReviewerは平均絶対誤差(MAE)を26.89%削減して有望な性能を達成できた。
  論文  参考訳（メタデータ） (2024-10-28T08:10:21Z)
• InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search [65.05674971652776]
  代表的な証明法は、証明手法を戦術によって反復的に構築することであり、典型的には最優先の探索スキームに従う。 本稿では,評価モデルを用いて選好情報を抽出する直感的かつ効果的な手法を提案する。 2万日以上のCPUを持つ大規模なエキスパートイテレーションが、証明者と批判者をさらに微調整するために適用される。
  論文  参考訳（メタデータ） (2024-10-21T07:18:23Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• L-Eval: Instituting Standardized Evaluation for Long Context Language Models [91.05820785008527]
  長い文脈言語モデル(LCLM)のより標準化された評価を行うためにL-Evalを提案する。 20のサブタスク、508の長いドキュメント、2000以上の人間ラベルのクエリ応答対を含む新しい評価スイートを構築した。 その結果、一般的なn-gramマッチングの指標は人間の判断とよく相関しないことがわかった。
  論文  参考訳（メタデータ） (2023-07-20T17:59:41Z)
• Mapping the Challenges of HCI: An Application and Evaluation of ChatGPT and GPT-4 for Mining Insights at Scale [4.6542291555324296]
  テキストコーパスから洞察を抽出する実世界の課題に対して,ChatGPTとGPT-4の組み合わせを評価した。 2023CHI会議の議題100件以上で4,392件の研究課題を抽出した。 また,ChatGPTとGPT-4の組み合わせは,テキストコーパスを大規模に解析するためのコスト効率に優れた手段である,という結論を得た。
  論文  参考訳（メタデータ） (2023-06-08T08:41:30Z)

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

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