論文の概要: Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration
- arxiv url: http://arxiv.org/abs/2607.27705v1
- Date: Thu, 30 Jul 2026 05:41:44 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-31 21:37:00.406758
- Title: Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration
- Title（参考訳）: Albilich:LCMに基づくCAS統合数学研究のためのステアブルな状態オーケストレーション
- Authors: Ting Gong, Michael Ruofan Zeng, Yong Yang,
- Abstract要約: 本稿では,自動検索のためのオープンソースのエージェントハーネスであるAlbilichを紹介する。
ロングホライズン推論、コンピュータ代数システム、文学検索、永続的文脈管理を組み合わせている。
これは、CASのないRealMathとCASのない9/10で10/10の問題を解決する。
- 参考スコア（独自算出の注目度）: 7.983427507667177
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models can contribute useful ideas to mathematical research, yet long-horizon proof attempts remain difficult to coordinate, evaluate, and reproduce. We present Albilich, an open-source agentic harness for autoresearch in mathematics that combines long-horizon reasoning, computer algebra systems (CAS), literature retrieval, and persistent SQLite-based context management. We evaluate Albilich on the RealMath benchmark (Zhang et al. 2025) and on open problems in group theory from the Kourovka Notebook (Khukhro and Mazurov 2026). It solved 10/10 problems on RealMath with CAS and 9/10 with no CAS. On the Kourovka problems, Albilich produced a counterexample to Problem 21.142 and a proof of a strengthening of Problem20.2. Anablation on Problem 17.91 demonstrates 32.0% token reduction when CAS is enabled. An ablation on Problem 21.142 demonstrates higher verifier-rejection rate and failure to synthesize proof routes in the absence of the advisor agent. These results support Albilich as a human-steerable, CAS-boosted environment for scalable AI-assisted mathematical research.
- Abstract（参考訳）: 大規模言語モデルは数学研究に有用なアイデアを貢献することができるが、長い水平証明の試みは調整、評価、再現が難しいままである。
本稿では,長軸推論,計算機代数システム(CAS),文献検索,永続的SQLiteベースのコンテキスト管理を組み合わせた,数学の自動検索のためのオープンソースのエージェントハーネスであるAlbilichを紹介する。
我々は、Albilich on the RealMath benchmark (Zhang et al 2025) and on open problem in group theory from the Kourovka Notebook (Khukhro and Mazurov 2026)。
これはCASのないRealMathとCASのない9/10で10/10の問題を解決した。
クーロヴカ問題に関して、アルビリッヒは21.142問題に対する反例と、20.2号の強化の証明を作成した。
問題17.91はCASを有効にすると32.0%のトークン還元を示す。
問題21.142のアブレーションは、より高いバリデーション・リジェクション率を示し、アドバイザ・エージェントの欠如による証明経路の合成に失敗する。
これらの結果は、スケーラブルなAI支援数学研究のための、人間の操縦可能なCASブースト環境として、Albilichを支援している。
関連論文リスト
- LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Iteris: Agentic Research Loops for Computational Mathematics [7.052820770689716]
本稿では,計算数学におけるオープンな問題に対するエージェント研究システムであるイテリスを紹介する。
我々は最近のSimons Workshopコレクションからイテリスを2つのオープンな問題に適用した。
イテリスは数値的な証拠、建設、証明の草案を作成し、専門家のレビューと修正を経て、検証結果に繋がった。
論文 参考訳（メタデータ） (2026-06-01T16:54:31Z) - Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics [9.38309744591661]
フォーマル・コンジェクチャ(Formal Conjectures)は、Lean 4.0で形式化された2615の数学的問題文の進化ベンチマークである。
このデータセットは、数学的な証明発見のためのゼロ汚染ベンチマークを提供する1029のオープンリサーチ予想を特徴としている。
我々は,これらの形式化の正しさを保証するためのアプローチを,アクティブなコミュニティからのコントリビューションを生かしたオープンソースプロジェクトとして紹介する。
論文 参考訳（メタデータ） (2026-05-13T08:33:15Z) - Towards Autonomous Mathematics Research [48.29504087871558]
Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。
具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。
我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
論文 参考訳（メタデータ） (2026-02-10T18:50:15Z) - Achieving Olympia-Level Geometry Large Language Model Agent via Complexity Boosting Reinforcement Learning [66.79506488139707]
大規模言語モデル(LLM)エージェントは強力な数学的問題解決能力を示す。
本研究では,メダリストレベルのメダリストレベルのLLMエージェントの構築とインターンジオメトリの紹介を行う。
InternGeometryは、命題と補助的な構成を反復的に提案することで幾何学の限界を克服し、それらを記号エンジンで検証する。
InternThinker-32BをベースとしたInternGeometryは、50 IMOの幾何学的問題の44を解き、平均金メダリストスコア(40.9)を超える。
論文 参考訳（メタデータ） (2025-12-11T11:05:04Z) - O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis [5.6900369690933195]
大規模言語モデルは、最近、IMOとPutnamの問題を解決する高度な能力を実証した。
主な困難は検証である: 提案は妥当に見えるが、厳密なチェックなしには信頼できない。
コンピュータ代数システムとフロンティア LLM を結合する LLM+CAS というフレームワークを提案する。
論文 参考訳（メタデータ） (2025-10-14T10:07:53Z) - Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。
創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか?
本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。
ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
論文 参考訳（メタデータ） (2025-05-24T03:52:25Z) - PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
本稿では,高品質なオリンピアードレベルの数学問題を自動生成する新しい手法であるPromptCoTを紹介する。
提案手法は,問題構築の背景にある数学的概念と理論的根拠に基づいて複雑な問題を合成する。
提案手法は, GSM8K, MATH-500, AIME2024などの標準ベンチマークで評価され, 既存の問題生成手法を一貫して上回っている。
論文 参考訳（メタデータ） (2025-03-04T06:32:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。