論文の概要: A Minimal Agent for Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2602.24273v1
• Date: Fri, 27 Feb 2026 18:43:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-02 19:48:24.568247
• Title: A Minimal Agent for Automated Theorem Proving
• Title（参考訳）: 自動定理証明のための最小エージェント
• Authors: Borja Requena Pozo, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro, Leopoldo Sarra,
• Abstract要約: この設計は、反復的証明改善、ライブラリ検索、コンテキスト管理といった最先端システム間で共有されるコア機能を実装している。 定性的に異なるベンチマークを用いてベースラインを評価し、様々な人気モデルと設計選択を比較した。
• 参考スコア（独自算出の注目度）: 0.3262230127283452
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative proof refinement, library search and context management. We evaluate our baseline using qualitatively different benchmarks and compare various popular models and design choices, and demonstrate competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture. Our results demonstrate consistent advantages of an iterative approach over multiple single-shot generations, especially in terms of sample efficiency and cost effectiveness. The implementation is released open-source as a candidate reference for future research and as an accessible prover for the community.
• Abstract（参考訳）: 本稿では,AIに基づく定理証明アーキテクチャの体系的比較を可能にする,最小限のエージェントベースラインを提案する。 この設計は、反復的証明改善、ライブラリ検索、コンテキスト管理といった最先端システム間で共有されるコア機能を実装している。 我々は、定性的に異なるベンチマークを用いてベースラインを評価し、様々な人気モデルと設計選択を比較し、最先端のアプローチと比較して競争性能を実証し、より単純なアーキテクチャを用いる。 以上の結果から,複数の単発世代に対して反復的アプローチが一貫した優位性を示し,特にサンプル効率とコスト効率について考察した。 この実装は、将来の研究の候補として、またコミュニティのアクセス可能な証明手段として、オープンソースとしてリリースされている。

関連論文リスト

• HEAS: Hierarchical Evolutionary Agent Simulation Framework for Cross-Scale Modeling and Multi-Objective Search [4.807104001943257]
  階層シミュレーションエージェント(Hierarchical Simulation Agent, HEAS)は、階層化されたエージェントベースのモデリングを進化的最適化とトーナメント評価で統合するPythonフレームワークである。 HEASは、共有コンテキストを読み書きする決定論的レイヤにスケジュールされた軽量プロセス(ストリーム)の階層としてモデルを表現する。 compact APIとCLIは、シングルオブジェクトとマルチオブジェクトの進化をシミュレートし、最適化し、評価します。
  論文  参考訳（メタデータ） (2025-08-21T13:35:46Z)
• Comparative Analysis of AI Agent Architectures for Entity Relationship Classification [1.6887793771613606]
  本研究では,3つの異なるAIエージェントアーキテクチャの比較分析を行い,関係分類を行う。 エージェントアーキテクチャは,(1)反射的自己評価,(2)階層的タスク分解,(3)新しいマルチエージェント動的サンプル生成機構を含む。 実験により,マルチエージェントの協調が標準のショットプロンプトより一貫して優れていることが実証された。
  論文  参考訳（メタデータ） (2025-06-03T04:19:47Z)
• EVA-MILP: Towards Standardized Evaluation of MILP Instance Generation [13.49043811341421]
  混合整数線形プログラミング(MILP)は、複雑な意思決定問題を解決するための基礎となる。 多様なデータセットに対する機械学習の需要により,MILPインスタンス生成手法の普及が加速し,標準化された評価手法が大幅に向上した。 本稿では,MILPインスタンス生成手法の体系的および客観的評価を目的とした総合ベンチマークフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-05-30T16:42:15Z)
• POGEMA: A Benchmark Platform for Cooperative Multi-Agent Pathfinding [76.67608003501479]
  POGEMAは、学習のための高速環境、問題インスタンスジェネレータ、可視化ツールキットを含む、総合的なツールセットである。 また、プライマリ評価指標に基づいて計算されるドメイン関連メトリクスの範囲を規定する評価プロトコルを導入し、定義する。 この比較の結果は、様々な最先端のMARL、検索ベース、ハイブリッド手法を含む。
  論文  参考訳（メタデータ） (2024-07-20T16:37:21Z)
• Explaining Modern Gated-Linear RNNs via a Unified Implicit Attention Formulation [54.50526986788175]
  効率的なシーケンスモデリングの最近の進歩は、Mamba、RWKV、および様々なゲートRNNのような注意のないレイヤーを生み出している。 我々はこれらのモデルの統一的なビューを示し、暗黙の因果自己注意層のような層を定式化する。 筆者らのフレームワークは,異なるレイヤに対する類似の基盤となるメカニズムを比較検討し,説明可能性の手法を直接適用する手段を提供する。
  論文  参考訳（メタデータ） (2024-05-26T09:57:45Z)
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving [13.374504717801061]
  本稿では,対話的定理証明における学習アプローチの公平かつ合理化された比較のためのフレームワークであるBAITを提案する。 BAITの機能を、いくつかのIPPベンチマークで詳細に比較して示す。 BAITはまた、インタラクティブ環境上に構築されたシステムのエンドツーエンドのパフォーマンスを評価することもできる。
  論文  参考訳（メタデータ） (2024-03-06T01:56:17Z)
• Hierarchical Ensemble-Based Feature Selection for Time Series Forecasting [0.0]
  非定常性のための階層的積み重ねに基づく特徴選択のための新しいアンサンブルアプローチを導入する。 当社のアプローチでは,階層構造を用いた機能間の共依存を利用しています。 このアプローチの有効性は、合成およびよく知られた実生活データセット上で実証される。
  論文  参考訳（メタデータ） (2023-10-26T16:40:09Z)
• Revisiting the Evaluation of Image Synthesis with GANs [55.72247435112475]
  本研究では, 合成性能の評価に関する実証的研究を行い, 生成モデルの代表としてGAN(Generative Adversarial Network)を用いた。 特に、表現空間におけるデータポイントの表現方法、選択したサンプルを用いた公平距離の計算方法、各集合から使用可能なインスタンス数など、さまざまな要素の詳細な分析を行う。
  論文  参考訳（メタデータ） (2023-04-04T17:54:32Z)
• Exploiting Temporal Structures of Cyclostationary Signals for Data-Driven Single-Channel Source Separation [98.95383921866096]
  単一チャネルソース分離(SCSS)の問題点について検討する。 我々は、様々なアプリケーション領域に特に適するサイクロ定常信号に焦点を当てる。 本稿では,最小MSE推定器と競合するU-Netアーキテクチャを用いたディープラーニング手法を提案する。
  論文  参考訳（メタデータ） (2022-08-22T14:04:56Z)
• HyperImpute: Generalized Iterative Imputation with Automatic Model Selection [77.86861638371926]
  カラムワイズモデルを適応的かつ自動的に構成するための一般化反復計算フレームワークを提案する。 既製の学習者,シミュレータ,インターフェースを備えた具体的な実装を提供する。
  論文  参考訳（メタデータ） (2022-06-15T19:10:35Z)
• Few-Shot Named Entity Recognition: A Comprehensive Study [92.40991050806544]
  マルチショット設定のモデル一般化能力を向上させるための3つの手法を検討する。 ラベル付きデータの比率の異なる10の公開nerデータセットについて経験的比較を行う。 マルチショットとトレーニングフリーの両方の設定で最新の結果を作成します。
  論文  参考訳（メタデータ） (2020-12-29T23:43:16Z)
• Probabilistic Case-based Reasoning for Open-World Knowledge Graph Completion [59.549664231655726]
  ケースベース推論(CBR)システムは,与えられた問題に類似した事例を検索することで,新たな問題を解決する。 本稿では,知識ベース(KB)の推論において,そのようなシステムが実現可能であることを示す。 提案手法は,KB内の類似エンティティからの推論パスを収集することにより,エンティティの属性を予測する。
  論文  参考訳（メタデータ） (2020-10-07T17:48:12Z)

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

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