論文の概要: Bolzano: From Expert-Guided Proof Search to Automated Open-Problem Solving

• arxiv url: http://arxiv.org/abs/2610.09769v2
• Date: Fri, 09 Oct 2026 13:27:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-13 04:06:29.17977
• Title: Bolzano: From Expert-Guided Proof Search to Automated Open-Problem Solving
• Title（参考訳）: Bolzano: エキスパートガイドによる証明から、オープンソースの問題解決まで
• Abstract要約: 検証エージェントを用いた並列証明エージェントを用いたマルチエージェントオープンソースシステムであるBolzanoについて述べる。 4組の論文から抽出した約3,800のオープン問題に対して,問題固有の人為的なガイダンスを使わずにBolzanoを実行し,約200のオープン問題を解決した。
• 参考スコア（独自算出の注目度）: 0.9495929024167086
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Large language models are increasingly contributing to mathematical research, where progress often depends on efficient proof search, incremental improvements and careful verification. We describe Bolzano, a multi-agent open-source system that uses parallel prover agents with a verifier agent and maintains a human-readable research state. Initial manual use on expert-selected problems yielded 8 results whose proofs were checked by domain experts. Motivated by these case studies, we ran Bolzano without problem-specific human guidance on about 3,800 open problems extracted from four sets of papers, solving about 200 open problems. One experiment used papers accepted to STOC 2026, a top conference in theoretical computer science. There, we answered four questions raised in the papers, as confirmed by their authors.
• Abstract（参考訳）: 大規模言語モデルは、効率的な証明探索、漸進的な改善、慎重な検証にしばしば依存する数学的研究にますます寄与している。 検証エージェントを用いた並列証明エージェントを用いたマルチエージェントオープンソースシステムであるBolzanoについて述べる。 専門家が選択した問題に対する最初の手動使用は8つの結果となり、その証明はドメインの専門家によって確認された。 これらのケーススタディによって、我々は4つの論文から抽出された約3,800のオープン問題に対して、問題固有の人為的なガイダンスなしでボルザーノを実行し、約200のオープン問題を解決した。 ある実験では、理論計算機科学の最高会議STOC 2026に受け入れられた論文を使用した。 そこで著者らが確認した4つの質問に答えた。

関連論文リスト

• IdeaScientist: Orchestrating Agents for Grounded Scientific Ideation [53.38412637382984]
  本稿では,イデオロギーをギャップ発見,イノベーション,レポート作成に分解し,各役割を強化学習で訓練するIdeanScientistを紹介する。 これらの役割は、関連する作業の限界を特定し、類似した問題設定から解の直観を引き出し、それらの直観を完全な研究提案へと発展させる。 ドメイン間の洞察の発見を容易にするため、検索、トレーニング、時間的に制御された評価のための277万の研究思想のコーパスであるSvalbard Idea Vaultを構築した。
  論文  参考訳（メタデータ） (2026-10-02T21:35:55Z)
• Continual Graph Memory for Mathematical Research Agents [95.750048838182]
  Ansatzはグラフベースの、進化可能な、クロスプロブレムな数学的研究メモリシステムである。 証明探索プロセス全体を整理し、過去の問題の探索軌跡から情報を再利用する。 アンサッツは10の研究課題の全てを閉鎖し、長期の数学的探索を継続し再開する能力を示した。
  論文  参考訳（メタデータ） (2026-10-02T07:38:09Z)
• SearchAuditor: Auditing and Attributing Failures in Long-Horizon Search Agents [56.400332595452966]
  我々は、監査人が検索エージェントの障害をローカライズ、属性付け、修復できるかどうかを評価するベンチマークであるSearchAuditBenchを紹介する。 SearchAuditBenchは1,243の障害トラックで構成され、平均73.1メッセージと65.1Kトークンを5つのディープサーチベンチマークで8つのオープンウェイトモデルから収集している。 本稿では,検索エージェントの障害を効果的にローカライズ,属性,修復するマルチパースペクティブ監査フレームワークであるSearchAuditorを提案する。
  論文  参考訳（メタデータ） (2026-08-05T09:09:00Z)
• ProofCouncil: An LLM Agent for Solving Open Mathematical Problems [2.90620992303615]
  本稿では,著者批判アーキテクチャを用いてオープンな問題に対処する数学的エージェントProofCouncilを紹介する。 ProofCouncilは、エージェントが自律的に解決しなければならない10の現実の数学的問題からなるチャレンジであるFirstProofの第2バッチの提出として機能した。 人的フィードバックを受けた21のソリューションのうち、5は完全正当と判断され、さらに2つは有望な最終検証と判断され、さらに8つは有用な部分的な進歩を含んでいた。
  論文  参考訳（メタデータ） (2026-07-10T14:46:01Z)
• Harnessing the Collective Intelligence of AI Agents in the Wild for New Discoveries [35.87396515951979]
  EinsteinArenaは、オープンな分散研究と発見のためのエージェントネイティブプラットフォームである。 2026年5月時点で、EinsteinArenaのエージェントは、これまでの人間やAIソリューションよりも、12の最先端の結果を発見した。
  論文  参考訳（メタデータ） (2026-06-09T04:25:28Z)
• The Last Human-Written Paper: Agent-Native Research Artifacts [106.47848184955576]
  本稿では,物語紙を機械処理可能な研究パッケージに置き換えるプロトコルであるAgent-Native Research Artifact(ARA)を紹介する。 通常の開発において決定と終了をキャプチャするLive Research Manager、レガシPDFとリポジトリをARAに変換するARAコンパイラ、人間レビュアーが重要性、ノベルティ、味にフォーカスできるように客観的チェックを自動化するARAネイティブレビューシステムである。
  論文  参考訳（メタデータ） (2026-04-27T16:23:09Z)
• Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the Erdős Problems [22.064232024924422]
  我々はジェミニを用いて、ブルームのアーズ問題データベースに「オープン」とラベル付けされた700の予想を評価する。 データベースに'オープン'とマークされた13の問題に対処する。 以上の結果から,問題の「開放」状態は難易度よりも不明瞭度が原因であることが示唆された。
  論文  参考訳（メタデータ） (2026-01-29T23:15:36Z)
• Can Deep Research Agents Find and Organize? Evaluating the Synthesis Gap with Expert Taxonomies [57.11324429385405]
  72のコンピュータサイエンスサーベイから得られた診断ベンチマークであるTaxoBenchを紹介する。 我々は,3,815個の引用を根本的真理として正確に分類した分類木を手作業で抽出した。 ベストエージェントは、専門家が選択した論文の20.9%しかリコールせず、完璧なインプットであっても、最高のモデルは組織の0.31 ARIしか達成していない。
  論文  参考訳（メタデータ） (2026-01-18T11:57:09Z)

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

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