論文の概要: Abstraction boundaries and spec driven development in pure mathematics
- arxiv url: http://arxiv.org/abs/2309.14870v1
- Date: Tue, 26 Sep 2023 11:59:32 GMT
- ステータス: 処理完了
- システム内更新日: 2023-09-27 13:53:45.530449
- Title: Abstraction boundaries and spec driven development in pure mathematics
- Title(参考訳): 純粋数学における抽象境界と仕様駆動開発
- Authors: Johan Commelin and Adam Topaz
- Abstract要約: 本稿では,抽象境界が数学的研究の複雑さにどのように貢献するかを論じる。
対話的定理証明器の使用は、これらの概念の実装にさらなる質的な利点をもたらすと論じる。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this article we discuss how abstraction boundaries can help tame
complexity in mathematical research, with the help of an interactive theorem
prover. While many of the ideas we present here have been used implicitly by
mathematicians for some time, we argue that the use of an interactive theorem
prover introduces additional qualitative benefits in the implementation of
these ideas.
- Abstract(参考訳): 本稿では,インタラクティブな定理証明器を用いて,抽象境界が数学研究の複雑さを和らげる上でどのように役立つかについて議論する。
ここで提示する多くのアイデアは、しばらくの間数学者によって暗黙的に使われてきたが、対話的定理証明器の使用は、これらの概念の実装にさらなる質的利益をもたらすと論じている。
関連論文リスト
- A Concise Mathematical Description of Active Inference in Discrete Time [0.0]
本論文の主部は、アクション選択の理論を詳述した詳細な例を含む、このトピックの基本的紹介として機能する。
付録では、より微妙な数学的詳細が議論されている。
この部分は、既に活発な推論文学を研究しているが、数学的詳細や導出を理解するのに苦労している読者を対象としている。
論文 参考訳(メタデータ) (2024-06-11T21:09:45Z) - Machine learning and information theory concepts towards an AI
Mathematician [77.63761356203105]
人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。
このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。
興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
論文 参考訳(メタデータ) (2024-03-07T15:12:06Z) - math-PVS: A Large Language Model Framework to Map Scientific
Publications to PVS Theories [10.416375584563728]
本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。
我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
論文 参考訳(メタデータ) (2023-10-25T23:54:04Z) - Parmesan: mathematical concept extraction for education [0.5520082338220947]
本研究では,カテゴリー論の分野に焦点をあて,文脈における数学的概念の探索と定義を行うプロトタイプシステムの開発を行う。
このシステムは、概念抽出、関係抽出、定義抽出、エンティティリンクを含む自然言語処理コンポーネントに依存している。
また,ジャーナル記事やウィキページをベースとしたプロトタイプシステムを利用した2つのクリーンな数学的コーパスも提供する。
論文 参考訳(メタデータ) (2023-07-13T11:55:03Z) - Towards a Holistic Understanding of Mathematical Questions with
Contrastive Pre-training [65.10741459705739]
本稿では,数学的問題表現,すなわち QuesCo に対する対照的な事前学習手法を提案する。
まず、コンテンツレベルと構造レベルを含む2段階の質問強化を設計し、類似した目的で文字通り多様な質問ペアを生成する。
そこで我々は,知識概念の階層的情報を完全に活用するために,知識階層を意識したランク戦略を提案する。
論文 参考訳(メタデータ) (2023-01-18T14:23:29Z) - A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。
大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
論文 参考訳(メタデータ) (2022-12-20T18:46:16Z) - Open Geometry Prover Community Project [0.0]
Open Geometry Prover Community Projectは、共通な"umbrella"の下で、幾何自動定理プロバーの開発のための様々な取り組みを統合することを目的としている。
本稿では、そのような統合に必要なステップと、これらのステップの現在の実装について説明する。
論文 参考訳(メタデータ) (2022-01-03T09:27:23Z) - A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
本稿では,古典的高階論理へのエンコーディングに基づく抽象的議論フレームワークの表現手法を提案する。
対話型および自動推論ツールを用いた抽象的議論フレームワークのコンピュータ支援評価のための一様フレームワークを提供する。
論文 参考訳(メタデータ) (2021-10-18T10:45:59Z) - NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
数学的ステートメントの多領域コーパスであるNaturalProofsとその証明を開発した。
NaturalProofsは広範なカバレッジ、深いカバレッジ、低リソースの数学的ソースを統一する。
数式参照検索と生成タスクに関する強力なニューラルネットワーク手法をベンチマークする。
論文 参考訳(メタデータ) (2021-03-24T03:14:48Z) - Explaining Creative Artifacts [69.86890599471202]
生成物と構成的創造性を結合鎖に分解する逆問題定式化を開発する。
特に、当社の定式化は、アソシエイト要素の知識グラフを通じて、旅行セールスマン問題の解決として構成されている。
論文 参考訳(メタデータ) (2020-10-14T14:32:38Z) - Information-Theoretic Abstractions for Planning in Agents with
Computational Constraints [16.565205172451662]
本稿では,元空間の抽象化に関する問題を解くことで,環境内の経路計画問題を体系的に近似する方法を示す。
数値的な例を提示し, アプローチの有用性を示し, 理論的知見を裏付ける。
論文 参考訳(メタデータ) (2020-05-19T17:32:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。