Fugu-MT 論文翻訳(概要): The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction

論文の概要: The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction

arxiv url: http://arxiv.org/abs/2509.15116v1
Date: Thu, 18 Sep 2025 16:19:41 GMT
ステータス: 翻訳完了
システム内更新日: 2025-09-19 17:26:53.327011
Title: The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
Title（参考訳）: 多段階Proj構成のリーン形式化による科学の機械化
Authors: Arnaud Mayeux, Jujian Zhang,
Abstract要約: 我々はLean4における多階化Projの構成を定式化し、機械化数学と形式化を図示した。この記事はSymbolic Interaction誌に初めて掲載された。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.
Abstract（参考訳）: 我々はLean4における多階化Projの構成を定式化し、機械化数学と形式化を図示した。

関連論文リスト

Geoint-R1: Formalizing Multimodal Geometric Reasoning with Dynamic Auxiliary Constructions [26.491034237276764]
Geoint-R1はテキスト記述と視覚図から検証可能な幾何学的解を生成するために設計された多モード推論フレームワークである。形式的幾何学的推論を体系的に評価し,先進的に進めるために,1,885個の厳密な注釈付き幾何学的問題を含むGeointベンチマークを提案する。 Geoint-R1は既存のマルチモーダルおよび数学固有の推論モデルを大きく上回る。
論文参考訳（メタデータ） (2025-08-05T07:29:58Z)
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文参考訳（メタデータ） (2025-06-05T03:16:08Z)
From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs [25.69931278771869]
本稿では,形式的推論の即時適用シナリオである形式的検証に焦点を当てる。我々は5つの形式仕様言語で18kの高品質な命令応答ペアを構築した。フォーマルなデータによる微調整は、数学、推論、コーディング能力も強化する。
論文参考訳（メタデータ） (2025-01-27T17:00:56Z)
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文参考訳（メタデータ） (2024-10-21T08:04:21Z)
Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
論文参考訳（メタデータ） (2024-09-09T18:21:28Z)
A process algebraic framework for multi-agent dynamic epistemic systems [55.2480439325792]
本稿では,マルチエージェント,知識ベース,動的システムのモデリングと解析のための統合フレームワークを提案する。モデリング側では,このようなフレームワークを実用的な目的に使いやすくするプロセス代数的,エージェント指向の仕様言語を提案する。
論文参考訳（メタデータ） (2024-07-24T08:35:50Z)
Parrot Mind: Towards Explaining the Complex Task Reasoning of Pretrained Large Language Models with Template-Content Structure [66.33623392497599]
テンプレート・コンテント構造(T-C構造)と呼ばれる構造は指数レベルから線形レベルへの可能な空間を減少させることができることを示す。モデルがタスク構成を達成でき、線形から対数への学習に必要なスペースをさらに削減できることを実証する。
論文参考訳（メタデータ） (2023-10-09T06:57:45Z)
Formal Mathematics Statement Curriculum Learning [64.45821687940946]
同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
論文参考訳（メタデータ） (2022-02-03T00:17:00Z)
A refinement of Reznick's Positivstellensatz with applications to quantum information theory [72.8349503901712]
ヒルベルトの17番目の問題において、アルティンはいくつかの変数の任意の正定値が2つの平方和の商として書けることを示した。レズニックはアルティンの結果の分母は常に変数の平方ノルムの$N$-次パワーとして選択できることを示した。
論文参考訳（メタデータ） (2019-09-04T11:46:26Z)

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