論文の概要: Theorem prover Arend

• arxiv url: http://arxiv.org/abs/2610.27264v2
• Date: Wed, 21 Oct 2026 12:15:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-23 00:40:06.083844
• Title: Theorem prover Arend
• Title（参考訳）: 定理証明者アーレン
• Abstract要約: 本論文はJetBrains Researchで開発された定理証明器 Arend の展示である。 アレンド言語は、一価基礎の枠組みの中で数学の形式化を促進するように設計されている。 メインのArendライブラリには、構成代数、トポロジー、合成ホモトピー理論の形式化が含まれている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the framework of univalent foundations and with the focus on constructive mathematics. It is based on a variant of homotopy type theory with cubical syntax that is more closely aligned with Martin-Löf Type Theory (MLTT) than fully computational cubical type theories, while still retaining some of their computational properties useful in practice. Among the most notable features of the Arend language is its powerful system of classes and records supporting subsumptive subtyping, partial implementations and anonymous extensions, which provides extensive flexibility for constructing hierarchies of definitions. Formalization in Arend is streamlined by the IntelliJ Arend plugin, which transforms IntelliJ IDEA into a full-fledged integrated development environment (IDE) for the Arend language. The main Arend library arend-lib includes formalizations in constructive algebra, topology and synthetic homotopy theory.
• Abstract（参考訳）: 本論文はJetBrains Researchで開発された定理証明器 Arend の展示である。 アレンド言語は、一価基礎の枠組みの中で数学の形式化を促進するために設計され、建設数学に焦点が当てられている。 これは、完全に計算された立方体型理論よりも、マルティン=レーフ型理論(MLTT)とより密に整合した立方体構文を持つホモトピー型理論の変種に基づいているが、実際には計算的性質のいくつかを保っている。 Arend言語の最も注目すべき特徴は、サブサブタイプ、部分実装、匿名拡張をサポートする強力なクラスとレコードのシステムである。 Arendの形式化はIntelliJ Arendプラグインによって合理化され、IntelliJ IDEAをArend言語用の本格的な統合開発環境(IDE)に変換する。 メインのArendライブラリのアレンド・リブは、構成代数、トポロジー、合成ホモトピー理論の形式化を含む。

関連論文リスト

• An Algebraic View of the Expressivity of Recurrent Language Models [50.88598486616582]
  本稿では、繰り返しニューラルネットワークの表現性に関する統一的代数的記述法を開発する。 同じアーキテクチャでは、浮動小数点反復が強制されると偶モジュラーカウンタを実装することはできないが、符号付き整数量子化の下ではすべての偶モジュラーカウンタを実現する。
  論文  参考訳（メタデータ） (2026-06-01T06:47:58Z)
• Power Term Polynomial Algebra for Boolean Logic [10.458069629518985]
  直交正規形(CNF)と代数正規形(ANF)を橋渡しするために設計されたブール公式の表現言語であるパワー項代数を導入する。 直接CNF->ANF変換は、式が小さな断片に分解されない限り指数的な爆発を引き起こす。 我々のフレームワークは、CNF節を直接表現しながら、モノミアルの構造化されたファミリーをコンパクトに符号化する、表現自体におけるこのミスマッチに対処する。
  論文  参考訳（メタデータ） (2026-03-14T09:22:52Z)
• Jet Functors and Weil Algebras in Automatic Differentiation: A Geometric Analysis [0.0]
  ジェットバンドルとワイル代数を用いた自動微分(AD)の幾何学的定式化を提案する。 正確さ、安定性、複雑さに関する簡潔な言明を導き出す。 この枠組みは、微分幾何学のレンズを通してAD理論を解釈する。
  論文  参考訳（メタデータ） (2025-10-16T06:25:24Z)
• Topos Theory for Generative AI and LLMs [3.0316063849624477]
  トポス理論を用いた新しい分類型生成型AIアーキテクチャ(GAIA)の設計を提案する。 大規模言語モデル (LLM) のカテゴリは,集合のようなカテゴリーであるトポを形成することを示す。 LLMトポスアーキテクチャの実装の可能性を定義するために,バックプロパゲーションのファンクリアルな特徴付けを用いる。
  論文  参考訳（メタデータ） (2025-08-05T20:00:06Z)
• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価する。 3つのニューラルアーキテクチャに対して、チョムスキー階層の様々な言語について結果を提供する。 我々の貢献は、将来の研究において、言語認識の主張を理論的に健全に検証するのに役立つだろう。
  論文  参考訳（メタデータ） (2024-11-11T16:33:25Z)
• Non-determinsitic algebraic rewriting as adjunction [0.0]
  我々は、通常の収束と終了の仮定を超越した書き直しのための一般的なモデル理論的意味論を開発する。 これは、多くのソート代数を拡張するモデル理論である事前順序代数に基づいている。
  論文  参考訳（メタデータ） (2022-04-26T07:55:09Z)
• Learning Algebraic Representation for Systematic Generalization in Abstract Reasoning [109.21780441933164]
  推論における体系的一般化を改善するためのハイブリッドアプローチを提案する。 我々はRaven's Progressive Matrices (RPM) の抽象的空間時間課題に対する代数的表現を用いたプロトタイプを紹介する。 得られた代数的表現は同型によって復号化して解を生成することができることを示す。
  論文  参考訳（メタデータ） (2021-11-25T09:56:30Z)
• Learning Algebraic Recombination for Compositional Generalization [71.78771157219428]
  合成一般化のための代数的組換え学習のためのエンドツーエンドニューラルモデルLeARを提案する。 主要な洞察は、意味解析タスクを潜在構文代数学と意味代数学の間の準同型としてモデル化することである。 2つの現実的・包括的構成一般化の実験は、我々のモデルの有効性を実証している。
  論文  参考訳（メタデータ） (2021-07-14T07:23:46Z)
• Neural Proof Nets [0.8379286663107844]
  本稿では,Sinkhorn ネットワークをベースとした証明ネットのニューラルバリアントを提案する。 AEThelでは,テキスト文の正しい書き起こしを線形ラムダ計算の証明や用語として70%の精度で行うことができる。
  論文  参考訳（メタデータ） (2020-09-26T22:48:47Z)

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

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