論文の概要: Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving
- arxiv url: http://arxiv.org/abs/2401.11898v1
- Date: Mon, 22 Jan 2024 12:49:08 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-23 14:11:09.884380
- Title: Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving
- Title（参考訳）: 合成幾何学における文と証明の自動補完:制約解法に基づくアプローチ
- Authors: Salwa Tabet Gonzalez (University of Strasbourg), Predrag Jani\v{c}i\'c
(University of Belgrade), Julien Narboux (University of Strasbourg)
- Abstract要約: 不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。
また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Conjecturing and theorem proving are activities at the center of mathematical
practice and are difficult to separate. In this paper, we propose a framework
for completing incomplete conjectures and incomplete proofs. The framework can
turn a conjecture with missing assumptions and with an under-specified goal
into a proper theorem. Also, the proposed framework can help in completing a
proof sketch into a human-readable and machine-checkable proof. Our approach is
focused on synthetic geometry, and uses coherent logic and constraint solving.
The proposed approach is uniform for all three kinds of tasks, flexible and, to
our knowledge, unique such approach.
- Abstract（参考訳）: 導出と定理証明は数学的実践の中心にある活動であり、分離することは困難である。
本稿では,不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、仮定が不足し、未特定の目標を持つ予想を適切な定理に変えることができる。
また、提案フレームワークは、証明スケッチを人間の可読かつ機械チェック可能な証明に仕上げるのに役立つ。
我々のアプローチは合成幾何学に重点を置いており、コヒーレント論理と制約解を用いる。
提案手法は,3種類のタスクすべてに対して柔軟で,私たちの知る限り,ユニークなアプローチである。
関連論文リスト
- Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。
制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。
我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
論文 参考訳（メタデータ） (2024-06-30T13:34:54Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - Towards Automated Readable Proofs of Ruler and Compass Constructions [0.0]
本稿では,我々の三角形構成解法であるArgoTriCSが,一階述語論理とコヒーレント論理に対して,自動定理証明器とどのように協調するかを示す。
これらの証明は現在、多くの高いレベルの補題に依存しており、我々のゴールは、幾何の基本的な公理からそれら全てを正式に示すことである。
論文 参考訳（メタデータ） (2024-01-22T12:48:51Z) - Plan, Verify and Switch: Integrated Reasoning with Diverse X-of-Thoughts [65.15322403136238]
我々は,多種多様な推論の思考をLCMに促すことにより,総合的な問題解決フレームワーク XoT を提案する。
各質問に対して、XoTは常に最も適切なメソッドを選択して始まり、各メソッドを反復的に実行する。
各イテレーション内で、XoTは生成された回答の有効性を積極的にチェックし、外部エグゼクタからのフィードバックを取り入れます。
論文 参考訳（メタデータ） (2023-10-23T07:02:20Z) - A Measure-Theoretic Axiomatisation of Causality [55.6970314129444]
我々は、コルモゴロフの確率の測度理論的公理化を因果関係の公理化への出発点とすることを好んで論じる。
提案するフレームワークは測度理論に厳格に根ざしているが,既存のフレームワークの長期的制限にも光を当てている。
論文 参考訳（メタデータ） (2023-05-19T13:15:48Z) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳（メタデータ） (2023-02-24T03:28:46Z) - TacticZero: Learning to Prove Theorems from Scratch with Deep
Reinforcement Learning [6.764610878007278]
深層強化学習を用いた対話型定理証明(ITP)の新しい手法を提案する。
我々は、各状態が潜在的な導出経路の集合を表すマルコフ決定プロセス(MDP)としてITPのプロセスを定式化する。
このフレームワークは、人間の専門家を使ったアプローチに匹敵するパフォーマンスを提供する。
論文 参考訳（メタデータ） (2021-02-19T06:08:39Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z) - Geometric Formulation for Discrete Points and its Applications [0.0]
離散点上の幾何学の新しい定式化を導入する。
これは普遍微分計算に基づいており、関数の代数による離散集合の幾何学的記述を与える。
論文 参考訳（メタデータ） (2020-02-07T01:12:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。