論文の概要: Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research
- arxiv url: http://arxiv.org/abs/2608.15052v2
- Date: Thu, 20 Aug 2026 15:44:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-21 14:00:35.323295
- Title: Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research
- Title（参考訳）: Andy: 厳密な証明と自律的な研究のための数学的エージェント
- Abstract要約: Andyは、数学の問題をトレース可能な証明に変える、自律的な数学的研究エージェントだ。
提案された問題を解いたり検証したりし、研究価値ゲートを通じて文学的な新しい問題を定式化し、証明構築と最終的な検証を行う。
実行可能DAGで証明ステップを編成し、各ステップを独立して検証し、その結果を証明書にバインドする。
- 参考スコア（独自算出の注目度）: 8.964774625644965
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Andy is an autonomous mathematical research agent that turns a mathematical problem into a traceable proof. It solves or verifies a submitted problem, formulates a literature-grounded new problem through a research-value gate, and carries it through proof construction and final verification. It organizes proof steps in an executable DAG, verifies each step independently and binds the result to a certificate, retains verified work whose interfaces remain unchanged during local repair, and records the full path from problem formulation to final proof. The system separates proof generation from correctness evaluation and can acquire, retain, retrieve, and reuse knowledge from existing results. Starting from a self-triggered impulsive consensus result, Andy formulates a global exponential leader-follower synchronization problem for delayed heterogeneous networks with switching communication topologies. The proposed hybrid control combines self-triggered impulses with execution delay and continuous feedback over a recovery window. After each delayed impulse, the feedback cancels the delayed error channel until the pre-impulse history leaves the active delay interval. Sufficient conditions for global exponential synchronization are established, Zeno behavior is excluded for both timing sequences, and a numerical example illustrates the result.
- Abstract（参考訳）: Andyは、数学の問題をトレース可能な証明に変える、自律的な数学的研究エージェントだ。
提案された問題を解いたり検証したりし、研究価値ゲートを通じて文学的な新しい問題を定式化し、証明構築と最終的な検証を行う。
実行可能DAG内の証明ステップを整理し、各ステップを独立して検証し、その結果を証明書にバインドし、局所的な修復中にインターフェースが変化しない検証作業を保持し、問題定式化から最終証明までの完全なパスを記録する。
このシステムは、正当性評価から証明生成を分離し、既存の結果から知識を取得し、保持し、回収し、再利用することができる。
自己トリガーインパルスコンセンサスの結果から始まり、アンディは通信トポロジを切り替えた遅延ヘテロジニアスネットワークに対するグローバル指数的リーダー-フォローラー同期問題を定式化する。
提案したハイブリッド制御は、自己トリガーインパルスと実行遅延とリカバリウィンドウ上での継続的なフィードバックを組み合わせたものである。
遅延インパルス毎にフィードバックは遅延エラーチャネルをキャンセルし、プレインパルス履歴はアクティブ遅延間隔を逸脱する。
グローバル指数同期のための十分条件が確立され、両方のタイミングシーケンスに対してゼノの挙動が除外され、数値的な例が結果を示す。
関連論文リスト
- ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving [31.00212239114582]
本稿では, 明示的, 正式に証明された記号的証明構造を進化させる, ニューロシンボリック・フレームワークProofEvolveを提案する。
それぞれの問題の中でProofEvolveは、振る舞いインデックス付きアーカイブで部分的なAND-OR証明DAGを進化させる。
この進化過程は不完全な試みから検証結果を保存し、後の証明に利用できるようにする。
論文 参考訳（メタデータ） (2026-08-26T19:15:27Z) - ScrambleToolBench: Agents Search Exhaustively Even When Their Own Map Points to the Next Step [74.83535434786145]
ScrambleToolBenchは,行動推論の分離を目的とした対話型端末ベンチマークである。
このベンチマークでは、エージェントがテストとエラーのインタラクションを通じて、隠されたツールの振る舞いを明らかにする必要がある。
現状の言語モデルに対する我々の評価は、初期発見が成功しても頑健な適応にはならないことを示している。
論文 参考訳（メタデータ） (2026-08-03T15:07:46Z) - When benchmark inferences do not compose: Projectibility in AI evaluation [0.0]
AIベンチマークの結果が1ステップで連続的なクレームに達することはめったにない。
評価者はそれをさらなるケースに一般化し、能力の証拠として解釈し、新しいタスクに外挿し、他のシステムやサイトへ輸送する。
保証リンクは保証チェーンを自動的に作らない。
論文 参考訳（メタデータ） (2026-07-28T18:07:04Z) - TwistedMerge: Certified Higher-Order Diagnostics and Abstention for Model Merging [0.48086260459837454]
我々は、チェックポイントが局所対象、アライメントマップが遷移、サイクル積が残留する有限降下問題としてマージを定式化する。
提案手法は, 定数エッジのNo-go結果, フリーズ・コンプレックスの3方向およびプレファミリーの誤差制御定理, 比較・複雑感度の精査試験である。
訓練された低ランク適応型監査では, 平均化係数は選択したGLr代表に依存するが, 大域的因子同期と高密度デルタSVDは安定である。
論文 参考訳（メタデータ） (2026-07-23T03:24:50Z) - Temporal-Causal Unity as an Operational Framework for Collective Dynamics: Causal-Progress Clocks, Synchronization, and Polarization [5.995482369040288]
本稿では,プロセス哲学的論文時間と因果変化の順序的展開を結びつける枠組みを開発する。
このフレームワークは意図的に3つの主張を分離する: 成立に関する解釈論、測定可能な因果関係座標、ネットワークモデル。
本論文は、因果関係と時系列モデルを比較するための、偽装可能な仮説とサンプル外プロトコルを導出する。
論文 参考訳（メタデータ） (2026-07-21T01:39:53Z) - One Reflection Is Not Enough: Self-Correcting Autonomous Research via Multi-Hypothesis Failure Attribution [85.65263343588026]
我々は,自己修正型,自律型,接地型実験機であるSAGEを提案する。
その中核的なメカニズムであるMHFA(Multi-Hypothesis Failure Attribution)は、回復を構造的因果診断として扱う。
12のトピック、5ドメインのベンチマークでは、SAGEは基準リフレクションでメトリクスを含むアウトプットを42%から92%に増やしている。
論文 参考訳（メタデータ） (2026-06-30T10:54:16Z) - AuditWeave: A Tamper-Evident, Auditor-Navigable Evidence Layer for AI-Assisted and Data-Transformation Workflows [0.0]
AuditWeaveは、AIアシストとデータ変換のステップを1つのハッシュチェーンの台帳に記録する軽量Pythonライブラリである。
本稿では,参照実装におけるオーバヘッド,拡張性,タンパー検出の正確さを設計し,評価する。
論文 参考訳（メタデータ） (2026-06-14T21:46:04Z) - LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - TopoEvo: A Topology-Aware Self-Evolving Multi-Agent Framework for Root Cause Analysis in Microservices [10.602349579405832]
根本原因分析(RCA)はノイズや異種多モード可観測性のために困難である。
近年のLCMをベースとしたRCAエージェントは、ツールグラウンドによる説明を生成できるが、トポロジーに依存しないことが多い。
グラフ表現学習を構造化されたトポロジ制約推論と組み合わせたトポロジ対応の自己進化型マルチエージェントである textbfTopoEvo を提案する。
論文 参考訳（メタデータ） (2026-05-15T04:45:44Z) - ArbGraph: Conflict-Aware Evidence Arbitration for Reliable Long-Form Retrieval-Augmented Generation [47.25596369834373]
ArbGraphは、長期RAGにおける前世代のエビデンス仲裁のためのフレームワークである。
ArbGraphは取得した文書をアトミックなクレームに分解し、それらをコンフリクト対応エビデンスグラフに整理する。
ArbGraphは、幻覚を低減し、検索ノイズに対する感度を低下させながら、ファクトリコールと情報密度を一貫して改善することを示す。
論文 参考訳（メタデータ） (2026-04-20T14:51:43Z) - Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving [13.446180044466324]
メカニック(Mechanic)は、謝罪駆動の形式的分解戦略を採用した新しいエージェントシステムである。
未解決のサブゴールを正確に分離するために、リーンの残念なプレースホルダーを活用することで、Mechanicは失敗するサブプロブレムを、クリーンで自己完結したコンテキストに抽出し、独立して解決する。
論文 参考訳（メタデータ） (2026-03-25T16:12:08Z) - ExDR: Explanation-driven Dynamic Retrieval Enhancement for Multimodal Fake News Detection [23.87220484843729]
マルチモーダルのフェイクニュースは 深刻な社会的脅威を引き起こします
Dynamic Retrieval-Augmented Generationはキーワードベースの検索をトリガーすることで、有望なソリューションを提供する。
マルチモーダルフェイクニュース検出のための説明駆動動的検索生成フレームワークであるExDRを提案する。
論文 参考訳（メタデータ） (2026-01-22T10:10:06Z) - Circular Reasoning: Understanding Self-Reinforcing Loops in Large Reasoning Models [66.11277323593475]
Circular Reasoningは、生成されたコンテンツが自身の再発の論理的前提として機能する自己強化トラップである。
機械学的には、円の推論は異なる境界を示す状態崩壊として特徴付けられる。
自己強化型V字型アテンション機構によって駆動される不自由なサイクルとして継続するループ開始を誘導する推論が阻害されることを明らかにする。
論文 参考訳（メタデータ） (2026-01-09T10:23:55Z) - Adversarial Yet Cooperative: Multi-Perspective Reasoning in Retrieved-Augmented Language Models [72.4149653187766]
本稿ではAdrialversa Reasoning RAG(ARR)というReasoner-Verifierフレームワークを提案する。
ReasonerとVerifierは、回収された証拠を推論し、プロセス認識の利点によってガイドされながら、互いの論理を批判する。
複数のベンチマーク実験により,本手法の有効性が示された。
論文 参考訳（メタデータ） (2026-01-08T06:57:03Z) - Althea: Human-AI Collaboration for Fact-Checking and Critical Reasoning [26.796186521236194]
本稿では,オンラインクレームのユーザ主導評価を支援するために,質問生成,証拠検索,構造化推論を統合した検索強化システムであるAltheaを紹介する。
AVeriTeCベンチマークでは、Altheaは0.44のマクロF1を達成し、標準的な検証パイプラインを上回り、サポートされたクレームと反証されたクレームの識別を改善している。
論文 参考訳（メタデータ） (2025-12-29T18:23:35Z) - Demystifying deep search: a holistic evaluation with hint-free multi-hop questions and factorised metrics [89.1999907891494]
We present WebDetective, a benchmark of hint-free multi-hop questions with a control Wikipedia sandbox。
25の最先端モデルに対する我々の評価は、すべてのアーキテクチャにまたがる体系的な弱点を明らかにしている。
私たちはエージェントワークフローであるEvidenceLoopを開発し、ベンチマークが特定する課題を明示的にターゲットしています。
論文 参考訳（メタデータ） (2025-10-01T07:59:03Z) - A Sample Efficient Conditional Independence Test in the Presence of Discretization [54.047334792855345]
離散化されたデータに直接条件付き独立テスト(CI)は、誤った結論につながる可能性がある。
最近の進歩は、観測データをバイナライズすることで、潜伏変数間の適切なCI関係を推測することを目指している。
そこで本研究では,バイナライゼーションプロセスに依存しないサンプル効率のCIテストを提案する。
論文 参考訳（メタデータ） (2025-06-10T12:41:26Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳（メタデータ） (2025-05-17T04:16:36Z) - Gated Recurrent Neural Networks with Weighted Time-Delay Feedback [55.596897987498174]
本稿では,重み付き時間遅延フィードバック機構を備えたゲートリカレントユニット(GRU)を導入し,時系列データの長期依存性をモデル化する手法を提案する。
提案したモデルである $tau$-GRU は、繰り返し単位の連続時間定式化の離散版であり、力学は遅延微分方程式(DDE)によって制御される。
論文 参考訳（メタデータ） (2022-12-01T02:26:34Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。