論文の概要: Towards a Geometry Automated Provers Competition
- arxiv url: http://arxiv.org/abs/2002.12556v1
- Date: Fri, 28 Feb 2020 05:24:29 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-28 02:30:09.199352
- Title: Towards a Geometry Automated Provers Competition
- Title（参考訳）: 幾何自動プローバーコンペティションに向けて
- Authors: Nuno Baeta (University of Coimbra), Pedro Quaresma (University of
Coimbra), Zolt\'an Kov\'acs (The Private University College of Education of
the Diocese of Linz)
- Abstract要約: GATPの競争により、GATP開発者が既存のものを改善し、新しいものを提案するためのテストベンチを作成することができる。
また、特定の用途に最適な実装を選択するために、"クライアント"(例えば教育用eラーニングシステムの開発者)が使用可能なGATPのランキングを確立することもできる。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The geometry automated theorem proving area distinguishes itself by a large
number of specific methods and implementations, different approaches
(synthetic, algebraic, semi-synthetic) and different goals and applications
(from research in the area of artificial intelligence to applications in
education).
Apart from the usual measures of efficiency (e.g. CPU time), the possibility
of visual and/or readable proofs is also an expected output against which the
geometry automated theorem provers (GATP) should be measured.
The implementation of a competition between GATP would allow to create a test
bench for GATP developers to improve the existing ones and to propose new ones.
It would also allow to establish a ranking for GATP that could be used by
"clients" (e.g. developers of educational e-learning systems) to choose the
best implementation for a given intended use.
- Abstract（参考訳）: 幾何自動定理証明領域は、多くの特定の方法と実装、異なるアプローチ(合成、代数、半合成)、異なる目的と応用(人工知能分野の研究から教育への応用まで)によって自らを区別する。
通常の効率(CPU時間など)の測度とは別に、視覚的および/または可読性証明の可能性もまた、幾何学的自動定理プローバー(GATP)を測るべき予想出力である。
GATPの競合の実装により、GATP開発者が既存のものを改善し、新しいものを提案するためのテストベンチを作成することができる。
また、特定の用途に最適な実装を選択するために、"クライアント"(例えば教育用eラーニングシステムの開発者)が使用可能なGATPのランキングを確立することもできる。
関連論文リスト
- Searching Latent Program Spaces [0.0]
本研究では,連続空間における潜伏プログラム上の分布を学習し,効率的な探索とテスト時間適応を可能にするプログラム誘導アルゴリズムを提案する。
テスト時間適応機構を利用して、トレーニング分布を超えて一般化し、目に見えないタスクに適応できることを示す。
論文 参考訳（メタデータ） (2024-11-13T15:50:32Z) - Nonparametric independence tests in high-dimensional settings, with applications to the genetics of complex disease [55.2480439325792]
遺伝子データの支持空間における適切な事前測定構造の定義が,このような検査に新たなアプローチをもたらすことを示す。
各問題に対して、数学的結果、シミュレーションおよび実データへの適用を提供する。
論文 参考訳（メタデータ） (2024-07-29T01:00:53Z) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳（メタデータ） (2023-10-16T08:42:39Z) - Self-Supervised Learning with Lie Symmetries for Partial Differential
Equations [25.584036829191902]
我々は、自己教師付き学習(SSL)のための共同埋め込み手法を実装することにより、PDEの汎用表現を学習する。
我々の表現は、PDEの係数の回帰などの不変タスクに対するベースラインアプローチよりも優れており、また、ニューラルソルバのタイムステッピング性能も向上している。
提案手法がPDEの汎用基盤モデルの開発に有効であることを期待する。
論文 参考訳（メタデータ） (2023-07-11T16:52:22Z) - AdaNPC: Exploring Non-Parametric Classifier for Test-Time Adaptation [64.9230895853942]
ドメインの一般化は、ターゲットのドメイン情報を活用することなく、任意に困難にすることができる。
この問題に対処するためにテスト時適応(TTA)手法が提案されている。
本研究では,テスト時間適応(AdaNPC)を行うためにNon-Parametricを採用する。
論文 参考訳（メタデータ） (2023-04-25T04:23:13Z) - A Rule Based Theorem Prover: an Introduction to Proofs in Secondary
Schools [0.0]
中学校における自動推論システムの導入は、いくつかのボトルネックに直面している。
幾何学的自動定理プローバーの結果と学校での推論と証明の通常の実践との間の不一致は、教育環境においてそのようなツールを広く使用する上で大きな障壁となる。
授業計画が提示され、その目標は幾何学的定理を証明する公式なデモンストレーションの導入であり、その目標に学生を動機付けようとすることである。
論文 参考訳（メタデータ） (2023-03-10T11:36:10Z) - Self-Supervised Learning to Prove Equivalence Between Straight-Line
Programs via Rewrite Rules [9.1570563482476]
2つのプログラムは、1つのプログラムをもう1つのプログラムに書き換える、書き換え規則の一連の適用が存在する場合と同値である。
本稿では,プログラムペア間の等価性の証明を生成するために,トランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。
我々のシステムであるS4Eqは、1万対の等価プログラムをキュレートしたデータセット上で97%の証明成功を達成した。
論文 参考訳（メタデータ） (2021-09-22T01:37:08Z) - An Extensible Benchmark Suite for Learning to Simulate Physical Systems [60.249111272844374]
我々は、統一されたベンチマークと評価プロトコルへの一歩を踏み出すために、一連のベンチマーク問題を導入する。
本稿では,4つの物理系と,広く使用されている古典的時間ベースおよび代表的なデータ駆動手法のコレクションを提案する。
論文 参考訳（メタデータ） (2021-08-09T17:39:09Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z) - Learning Reasoning Strategies in End-to-End Differentiable Proving [50.9791149533921]
条件付き定理プローバーは勾配に基づく最適化により最適規則選択戦略を学習する。
条件付き定理プローサは拡張性があり、CLUTRRデータセット上で最先端の結果が得られることを示す。
論文 参考訳（メタデータ） (2020-07-13T16:22:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。