The Tactician’s Web of Large-Scale Formal Knowledge

要約

The Tactician’s Web は、機械学習、分析、証明エンジニアリング用に便利にパッケージ化された、強力に相互接続され、機械チェックされた正式な数学的知識の大規模なウェブを提供するプラットフォームです。
Coq 証明アシスタント上に構築されたこのプラットフォームは、定義、定理、証明用語、戦術、証明状態の網として提示される、さまざまな形式理論を含むデータセットをエクスポートします。
理論はセマンティック グラフ (下に表示) と人間が読めるテキストの両方としてエンコードされ、それぞれに独自の利点と欠点があります。
証明エージェントは、同じ豊富なデータ表現を通じて Coq と対話することができ、一連の定理に基づいて自動的にベンチマークを行うことができます。
Coq との緊密な統合により、エージェントを実用的なツールとして証明エンジニアが利用できる独自の可能性が得られます。

要約(オリジナル)

The Tactician’s Web is a platform offering a large web of strongly interconnected, machine-checked, formal mathematical knowledge conveniently packaged for machine learning, analytics, and proof engineering. Built on top of the Coq proof assistant, the platform exports a dataset containing a wide variety of formal theories, presented as a web of definitions, theorems, proof terms, tactics, and proof states. Theories are encoded both as a semantic graph (rendered below) and as human-readable text, each with a unique set of advantages and disadvantages. Proving agents may interact with Coq through the same rich data representation and can be automatically benchmarked on a set of theorems. Tight integration with Coq provides the unique possibility to make agents available to proof engineers as practical tools.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google