Fugu-MT 論文翻訳(概要): Towards Automated Readable Proofs of Ruler and Compass Constructions

論文の概要: Towards Automated Readable Proofs of Ruler and Compass Constructions

arxiv url: http://arxiv.org/abs/2401.13700v1
Date: Mon, 22 Jan 2024 12:48:51 GMT
ステータス: 処理完了
システム内更新日: 2024-01-26 17:02:45.069195
Title: Towards Automated Readable Proofs of Ruler and Compass Constructions
Title（参考訳）: 定規とコンパス構成の自動可読証明に向けて
Authors: Vesna Marinkovi\'c (Faculty of Mathematics, University of Belgrade), Tijana \v{S}ukilovi\'c (Faculty of Mathematics, University of Belgrade), Filip Mari\'c (Faculty of Mathematics, University of Belgrade)
Abstract要約: 本稿では,我々の三角形構成解法であるArgoTriCSが,一階述語論理とコヒーレント論理に対して,自動定理証明器とどのように協調するかを示す。これらの証明は現在、多くの高いレベルの補題に依存しており、我々のゴールは、幾何の基本的な公理からそれら全てを正式に示すことである。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Although there are several systems that successfully generate construction steps for ruler and compass construction problems, none of them provides readable synthetic correctness proofs for generated constructions. In the present work, we demonstrate how our triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic so that it generates construction correctness proofs, that are both human-readable and formal (can be checked by interactive theorem provers such as Coq or Isabelle/HOL). These proofs currently rely on many high-level lemmas and our goal is to have them all formally shown from the basic axioms of geometry.
Abstract（参考訳）: 定規およびコンパス構築問題に対する構築手順をうまく生成するシステムはいくつか存在するが、いずれも生成した構成に対して可読な合成正しさ証明を提供していない。本研究は,我々の三角形構成解法であるArgoTriCSが一階述語論理とコヒーレント論理の自動定理証明と協調して,人間の可読性および形式性の両方を持つ構成正当性証明(CoqやIsabelle/HOLのような対話的定理証明によって検証できる)を生成する方法を示す。これらの証明は現在、多くの高いレベルの補題に依存しており、我々の目標は、幾何の基本的な公理からそれらを全て正式に示すことである。

関連論文リスト

Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。自己形式化定理文の自動意味評価を行う。
論文参考訳（メタデータ） (2024-05-27T14:35:10Z)
ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
論文参考訳（メタデータ） (2024-05-05T02:06:37Z)
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文参考訳（メタデータ） (2024-02-14T05:57:58Z)
Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving [0.0]
不完全予想と不完全証明を完遂する枠組みを提案する。このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
論文参考訳（メタデータ） (2024-01-22T12:49:08Z)
Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文参考訳（メタデータ） (2023-11-16T11:26:21Z)
Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。 2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
論文参考訳（メタデータ） (2023-05-23T01:25:29Z)
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文参考訳（メタデータ） (2023-01-05T17:56:00Z)
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs [30.57062828812679]
本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
論文参考訳（メタデータ） (2022-10-21T22:37:22Z)
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving [0.0]
ここでは、自動一階述語証明に対する「証明構造としての組合せ項」のアプローチを紹介する。このアプローチは、凝縮した分枝に根付いた証明構造の項ビューと接続法に基づいて構築される。
論文参考訳（メタデータ） (2022-09-26T11:23:17Z)
Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
3,002の幾何学的問題と密接なアノテーションを形式言語に含む新しい大規模ベンチマークGeometry3Kを構築します。我々は、Interpretable Geometry Problemsolvr (Inter-GPS)と呼ばれる形式言語と記号推論を用いた新しい幾何学的解法を提案する。イントラGPSは定理の知識を条件付き規則として取り入れ、記号的推論を段階的に行う。
論文参考訳（メタデータ） (2021-05-10T07:46:55Z)
Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context [0.0]
我々は、Prologのエンコーディングから証明の完全なセットの生成に至るまで、我々が実装した中核的な概念を提示する。また、私たちが直面した主な問題と、選択したソリューションも提示します。
論文参考訳（メタデータ） (2020-02-28T05:23:16Z)

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