論文の概要: 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（参考訳）: 合成幾何学における文と証明の自動補完:制約解法に基づくアプローチ
• 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種類のタスクすべてに対して柔軟で,私たちの知る限り,ユニークなアプローチである。

関連論文リスト

• ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
  我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。 ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。 実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
  論文  参考訳（メタデータ） (2026-06-09T06:50:15Z)
• A Theoretical Framework for Self-Play Theorem Proving Algorithms [7.702779307300836]
  定理証明のための自己表現アルゴリズムの自己改善能力を理解するための理論的枠組みを提供する。 定理の基底グラフが十分に連結であれば、導出アルゴリズムが可逆ランダムウォークに基づいて証明された定理の集合を指数関数的に成長させるのに十分であることを示す。
  論文  参考訳（メタデータ） (2026-06-01T08:12:47Z)
• Learning to Reason with Insight for Informal Theorem Proving [50.054221663394195]
  この研究では、非公式な定理における主要なボトルネックを洞察の欠如として証明する。 我々は,この本質的な推論スキルを育成し,LLMが洞察に富んだ推論を行うことを可能にする新しいフレームワークを提案する。 問題となる数学ベンチマークの実験では、この洞察・認識型生成戦略がベースラインを著しく上回ることを示した。
  論文  参考訳（メタデータ） (2026-04-17T17:36:21Z)
• Automated Conjecture Resolution with Formal Verification [21.763678203045973]
  本研究では,研究レベルの数学的問題に対処するためのフレームワークを提案する。 我々のフレームワークは、非公式な推論エージェントであるRethlasと、正式な検証エージェントであるArchonの2つのコンポーネントで構成されている。 このフレームワークを使用することで、可換代数におけるオープンな問題を自動で解決し、人間による関与なしにLean 4における結果の証明を正式に検証します。
  論文  参考訳（メタデータ） (2026-04-04T16:35:16Z)
• LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving [6.220998637943786]
  LeanConjecturerは、Large Language Models(LLMs)を使用して、Lean 4で大学レベルの数学予想を自動的に生成するパイプラインである。 反復生成と評価により、LeanConjecturerは40のMathlibシードファイルから12,289の予想を生成し、3,776は構文的に有効で非自明であると同定された。
  論文  参考訳（メタデータ） (2025-06-27T08:17:18Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• 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)
• Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference [0.16317061277457]
  自然言語推論の基礎となる推論過程をモデル化できる推論フレームワークを提案する。 このフレームワークは、形式論理におけるよく研究された証明システムであるセマンティック・テーブルー法に基づいている。 本稿では、自然言語推論タスクを構造化された説明で定義する方法について述べる。
  論文  参考訳（メタデータ） (2023-11-15T01:24:09Z)
• 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)

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

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