Fugu-MT 論文翻訳(概要): Bolzano: Case Studies in LLM-Assisted Mathematical Research

論文の概要: Bolzano: Case Studies in LLM-Assisted Mathematical Research

arxiv url: http://arxiv.org/abs/2604.16989v2
Date: Fri, 24 Apr 2026 09:39:57 GMT
ステータス: 翻訳完了
システム内更新日: 2026-04-27 15:36:26.189255
Title: Bolzano: Case Studies in LLM-Assisted Mathematical Research
Title（参考訳）: ボルザーノ : LLM支援数学研究の事例研究
Abstract要約: Bolzano はオープンソースのマルチエージェント LLM システムである。 Bolzanoは、永続的な知識ベースを維持しながら、並列証明エージェントと検証エージェントの間の相互作用のラウンドをオーケストレーションする。 8つのうち6つが出版可能な研究水準に達し、8つのうち5つがボルザーノによって事実上自律的に生産された。
参考スコア（独自算出の注目度）: 0.9495929024167086
License: http://creativecommons.org/licenses/by-sa/4.0/
Abstract: We report new results on eight problems in mathematics and theoretical computer science, produced with the assistance of Bolzano, an open-source multi-agent LLM system. Bolzano orchestrates rounds of interaction between parallel prover agents and a verifier agent while maintaining a persistent knowledge base that is carried across rounds. Classified using the significance-autonomy taxonomy of Feng et al., six of the eight results reach the level of publishable research, and five of the eight were produced essentially autonomously by Bolzano. Our results provide evidence that LLMs can contribute meaningfully to mathematical research, complementing recent reports by Bubeck et al., Woodruff et al., and others.
Abstract（参考訳）: 我々は,オープンソースのマルチエージェントLLMシステムであるBolzanoの助けを借りて,数学と理論計算機科学の8つの問題に関する新たな結果を報告する。ボルザーノは、並列証明エージェントと検証エージェントとの相互作用のラウンドを編成し、ラウンドにまたがる永続的な知識ベースを維持している。 Feng et al の意義・自律性分類を用いて分類され、8つのうち6つが出版可能な研究水準に達し、8つのうち5つがボルザーノによって本質的に自律的に生産された。この結果は, ブベックらによる最近の報告, Woodruffらによる報告を補完し, LLMsが数学的研究に有意義に寄与することを示すものである。

関連論文リスト

LAMP: Lean-based Agentic framework with MCP and Proof Repair [0.0]
LAMPは、推論時に明示的に構造化されたドメイン知識を提供することで、カーネル検証されたLean 4証明を合成するフレームワークです。 LAMPは96.7%の定理の証明証明を合成し、未スケールのベースラインと既存の特殊プローバーをほぼ超えている。
論文参考訳（メタデータ） (2026-06-27T09:58:09Z)
ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。 ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
論文参考訳（メタデータ） (2026-06-09T06:50:15Z)
Can LLM generate interesting mathematical research problems? [5.836029794016965]
我々は未知の問題を発生させるエージェントを開発し、微分幾何学における665の研究問題を発生させる。人間の検証により、これらの数学的問題の多くは専門家には未知であり、独自の研究価値を持っていることが判明した。
論文参考訳（メタデータ） (2026-03-19T12:02:42Z)
Towards Autonomous Mathematics Research [48.29504087871558]
Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
論文参考訳（メタデータ） (2026-02-10T18:50:15Z)
Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving [14.569345246475509]
大規模言語モデル(LLM)は、有望な一階述語論理(FOL)推論能力を示している。しかし、多段階のFOL還元を含む複雑な数学的推論におけるそれらの効果はいまだ研究されていない。 LLMの生成戦略の多様性と再現性を向上する自己適応型ソリューションであるDREAMを提案する。
論文参考訳（メタデータ） (2025-06-20T16:09:56Z)
REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning [12.343823629674368]
私たちはREAL-Proverという,Lean 4.0用の新たなオープンソースステップワイドな定理証明ツールを紹介します。我々の証明者は、特に大学レベルの数学問題の解法における性能を高める。実験では、教師付き微チューン定理のみを用いた証明器は23.7%の成功率で競合する結果が得られる。
論文参考訳（メタデータ） (2025-05-27T01:26:11Z)
MLRC-Bench: Can Language Agents Solve Machine Learning Research Challenges? [66.87201770167012]
MLRC-Benchは、機械学習(ML)リサーチコンペティションの挑戦において、言語エージェントがいかに効果的に対処できるかを定量化するために設計されたベンチマークである。 MLRC-Benchは以前の研究とは異なり、新しい研究手法を提案し、実装する上で重要なステップを計測する。最も優れた試験薬でさえ、ベースラインとトップヒューマンのスコアの差の9.3%しか閉じていない。
論文参考訳（メタデータ） (2025-04-13T19:35:43Z)
Multi-LLM Collaborative Search for Complex Problem Solving [54.194370845153784]
そこで我々は,Mixture-of-Search-Agents(MoSA)パラダイムを提案する。 MoSAは、独立した探索とLCM間の反復的精錬を組み合わせることで、様々な推論経路を統合する。モンテカルロ木探索(MCTS)をバックボーンとして使用することにより、複数のエージェントが推論ステップを提案して集約することが可能となり、精度が向上する。
論文参考訳（メタデータ） (2025-02-26T06:31:04Z)
Accessing GPT-4 level Mathematical Olympiad Solutions via Monte Carlo Tree Self-refine with LLaMa-3 8B [48.45472563225202]
本稿では,大規模言語モデル (LLM) とモンテカルロ木探索 (MCTS) を革新的に統合した MCT Self-Refine (MCTSr) アルゴリズムを提案する。このアルゴリズムは、セレクション、自己定義、自己評価、バックプロパゲーションの反復的なプロセスを通じてモンテカルロ探索木を構築する。大規模な実験は、オリンピアードレベルの数学問題の解法におけるMCTSrの有効性を示す。
論文参考訳（メタデータ） (2024-06-11T16:01:07Z)
GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
大規模言語モデル (LLM) は、様々な数学的推論ベンチマークで顕著な性能を達成している。 1つの必須かつ頻繁な証拠は、数学の質問がわずかに変更されたとき、LLMは誤って振る舞うことができることである。このことは, LLMの数学推論能力の頑健性を評価するために, 幅広い質問のバリエーションを試すことによるものである。
論文参考訳（メタデータ） (2024-02-29T15:26:14Z)
math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
論文参考訳（メタデータ） (2023-10-25T23:54:04Z)
SciBench: Evaluating College-Level Scientific Problem-Solving Abilities of Large Language Models [70.5763210869525]
拡張ベンチマークスイートSciBench for Large Language Model (LLM)を導入する。 SciBenchには、数学、化学、物理学の分野から、さまざまな大学レベルの科学的問題を含むデータセットが含まれている。その結果、現在のLLMは満足のいく性能を達成できないことが判明し、全体のスコアは43.22%に過ぎなかった。
論文参考訳（メタデータ） (2023-07-20T07:01:57Z)

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