論文の概要: BAIT: Benchmarking (Embedding) Architectures for Interactive
Theorem-Proving
- arxiv url: http://arxiv.org/abs/2403.03401v1
- Date: Wed, 6 Mar 2024 01:56:17 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-07 16:21:46.509685
- Title: BAIT: Benchmarking (Embedding) Architectures for Interactive
Theorem-Proving
- Title（参考訳）: BAIT:インタラクティブな理論開発のためのベンチマーク(埋め込み)アーキテクチャ
- Authors: Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul
Montague
- Abstract要約: 本稿では,対話的定理証明における学習アプローチの公平かつ合理化された比較のためのフレームワークであるBAITを提案する。
BAITの機能を、いくつかのIPPベンチマークで詳細に比較して示す。
BAITはまた、インタラクティブ環境上に構築されたシステムのエンドツーエンドのパフォーマンスを評価することもできる。
- 参考スコア（独自算出の注目度）: 13.374504717801061
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Artificial Intelligence for Theorem Proving has given rise to a plethora of
benchmarks and methodologies, particularly in Interactive Theorem Proving
(ITP). Research in the area is fragmented, with a diverse set of approaches
being spread across several ITP systems. This presents a significant challenge
to the comparison of methods, which are often complex and difficult to
replicate. Addressing this, we present BAIT, a framework for fair and
streamlined comparison of learning approaches in ITP. We demonstrate BAIT's
capabilities with an in-depth comparison, across several ITP benchmarks, of
state-of-the-art architectures applied to the problem of formula embedding. We
find that Structure Aware Transformers perform particularly well, improving on
techniques associated with the original problem sets. BAIT also allows us to
assess the end-to-end proving performance of systems built on interactive
environments. This unified perspective reveals a novel end-to-end system that
improves on prior work. We also provide a qualitative analysis, illustrating
that improved performance is associated with more semantically-aware
embeddings. By streamlining the implementation and comparison of Machine
Learning algorithms in the ITP context, we anticipate BAIT will be a
springboard for future research.
- Abstract（参考訳）: Theorem Provingのための人工知能は、特にInteractive Theorem Proving (ITP)において、多くのベンチマークと方法論を生み出している。
この分野の研究は断片化されており、様々なアプローチがいくつかのITPシステムに分散している。
これは、しばしば複雑で複製が難しいメソッドの比較に重大な挑戦をもたらす。
そこで我々は,itp における学習アプローチを公平かつ合理的に比較するためのフレームワーク bait を提案する。
式埋め込み問題に適用可能な最先端アーキテクチャを,いくつかの itp ベンチマークで詳細に比較して bait の能力を示す。
構造認識変換器の動作は特に良好であり,元の問題集合に関連する技術の改善が期待できる。
BAITはまた、インタラクティブ環境上に構築されたシステムのエンドツーエンドのパフォーマンスを評価することもできる。
この統一的な視点は、以前の作業で改善される新しいエンドツーエンドシステムを明らかにする。
また,性能向上が意味論的に認識された埋め込みと関連していることを示す定性的な分析も提供する。
ITPコンテキストにおける機械学習アルゴリズムの実装と比較を合理化することによって、BAITが今後の研究の出発点になることを期待する。
関連論文リスト
- Boosting CNN-based Handwriting Recognition Systems with Learnable Relaxation Labeling [48.78361527873024]
本稿では,2つの異なる手法の強みを組み込んだ手書き文字認識手法を提案する。
本稿では,アルゴリズムの収束を加速し,システム全体の性能を向上させるスペーシフィケーション手法を提案する。
論文 参考訳（メタデータ） (2024-09-09T15:12:28Z) - POGEMA: A Benchmark Platform for Cooperative Multi-Agent Navigation [76.67608003501479]
主評価指標の基礎に基づいて計算された領域関連メトリクスの範囲を定義する評価プロトコルを導入・指定する。
このような比較の結果は、様々な最先端のMARL、検索ベース、ハイブリッド手法を含むものである。
論文 参考訳（メタデータ） (2024-07-20T16:37:21Z) - LInK: Learning Joint Representations of Design and Performance Spaces through Contrastive Learning for Mechanism Synthesis [15.793704096341523]
本稿では,性能と設計空間のコントラスト学習と最適化手法を統合する新しいフレームワークであるLInKを紹介する。
マルチモーダルおよび変換不変のコントラスト学習フレームワークを活用することで、LInKは複雑な物理学とメカニズムの設計表現をキャプチャする共同表現を学習する。
以上の結果から,LInKは機構設計の分野を進展させるだけでなく,他の工学分野へのコントラスト学習や最適化の適用性も拡大することが示された。
論文 参考訳（メタデータ） (2024-05-31T03:04:57Z) - Learning Interpretable Models Through Multi-Objective Neural
Architecture Search [0.9990687944474739]
本稿では,タスク性能と「イントロスペクタビリティ」の両方を最適化するフレームワークを提案する。
タスクエラーとイントロスペクタビリティを共同で最適化することは、エラー内で実行されるより不整合でデバッグ可能なアーキテクチャをもたらすことを実証する。
論文 参考訳（メタデータ） (2021-12-16T05:50:55Z) - Harnessing Heterogeneity: Learning from Decomposed Feedback in Bayesian
Modeling [68.69431580852535]
サブグループフィードバックを取り入れた新しいGPレグレッションを導入する。
我々の修正された回帰は、以前のアプローチと比べて、明らかにばらつきを減らし、したがってより正確な後続を減らした。
我々は2つの異なる社会問題に対してアルゴリズムを実行する。
論文 参考訳（メタデータ） (2021-07-07T03:57:22Z) - Towards Large Scale Automated Algorithm Design by Integrating Modular
Benchmarking Frameworks [0.9281671380673306]
本稿では,アルゴリズムフレームワークであるParadisEOと,自動アルゴリズム設定ツール irace と実験プラットフォーム IOHknownr の効率性を示す最初の概念実証例を提案する。
パイプラインの主な利点は、高速な評価時間、豊富なデータセットを生成する可能性、そしてサンプリングベースの最適化の非常に幅広いクラスをベンチマークするのに使用できる標準化されたインターフェースである。
論文 参考訳（メタデータ） (2021-02-12T10:47:00Z) - Investigating Bi-Level Optimization for Learning and Vision from a
Unified Perspective: A Survey and Beyond [114.39616146985001]
機械学習やコンピュータビジョンの分野では、モチベーションやメカニズムが異なるにもかかわらず、複雑な問題の多くは、一連の密接に関連するサブプロトコルを含んでいる。
本稿では,BLO(Bi-Level Optimization)の観点から,これらの複雑な学習と視覚問題を一様に表現する。
次に、値関数に基づく単一レベル再構成を構築し、主流勾配に基づくBLO手法を理解し、定式化するための統一的なアルゴリズムフレームワークを確立する。
論文 参考訳（メタデータ） (2021-01-27T16:20:23Z) - Improving the Effectiveness of Traceability Link Recovery using
Hierarchical Bayesian Networks [21.15456830607455]
We implement a HierarchiCal Probabilistic Model for SoftwarE Traceability (Comet)
彗星は、テキスト類似性の複数の尺度の相補的な観察能力を組み合わせることで、人工物間の関係をモデル化することができる。
我々は、最適に設定されたベースラインのセットに対する改善を示す、Cometの包括的な経験的評価を行う。
論文 参考訳（メタデータ） (2020-05-18T19:38:29Z) - A Dependency Syntactic Knowledge Augmented Interactive Architecture for
End-to-End Aspect-based Sentiment Analysis [73.74885246830611]
エンドツーエンドABSAのためのマルチタスク学習を用いた対話型アーキテクチャを新たに提案する。
このモデルは、よく設計された依存性関係埋め込みグラフ畳み込みネットワーク(DreGcn)を活用することで、構文知識(依存性関係と型)を完全に活用することができる。
3つのベンチマークデータセットの大規模な実験結果から,本手法の有効性が示された。
論文 参考訳（メタデータ） (2020-04-04T14:59:32Z) - Image Matching across Wide Baselines: From Paper to Practice [80.9424750998559]
局所的な特徴とロバストな推定アルゴリズムの包括的なベンチマークを導入する。
パイプラインのモジュール構造は、さまざまなメソッドの容易な統合、構成、組み合わせを可能にします。
適切な設定で、古典的な解決策は依然として芸術の知覚された状態を上回る可能性があることを示す。
論文 参考訳（メタデータ） (2020-03-03T15:20:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。