Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)

• URL: http://arxiv.org/abs/2104.13645v1
• Date: Wed, 28 Apr 2021 09:09:20 GMT
• Title: Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)
• Authors: Christoph Wernhard and Wolfgang Bibel
• Abstract summary: This paper studies global features in selected problems and their proofs. The studied problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)"
• Score: 4.111899441919164
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)". The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by {\L}ukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.

Related papers

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Evaluating Human Alignment and Model Faithfulness of LLM Rationale [66.75309523854476]
  We study how well large language models (LLMs) explain their generations through rationales. We show that prompting-based methods are less "faithful" than attribution-based explanations.
  arXiv  Detail & Related papers  (2024-06-28T20:06:30Z)
• Class-wise Activation Unravelling the Engima of Deep Double Descent [0.0]
  Double descent presents a counter-intuitive aspect within the machine learning domain. In this study, we revisited the phenomenon of double descent and discussed the conditions of its occurrence.
  arXiv  Detail & Related papers  (2024-05-13T12:07:48Z)
• A Survey on Deep Learning for Theorem Proving [16.28502772608166]
  Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. Deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving.
  arXiv  Detail & Related papers  (2024-04-15T17:07:55Z)
• Seeing Unseen: Discover Novel Biomedical Concepts via Geometry-Constrained Probabilistic Modeling [53.7117640028211]
  We present a geometry-constrained probabilistic modeling treatment to resolve the identified issues. We incorporate a suite of critical geometric properties to impose proper constraints on the layout of constructed embedding space. A spectral graph-theoretic method is devised to estimate the number of potential novel classes.
  arXiv  Detail & Related papers  (2024-03-02T00:56:05Z)
• Machine learning assisted exploration for affine Deligne-Lusztig varieties [3.7863170254779335]
  This paper presents a novel, interdisciplinary study that leverages a Machine Learning (ML) assisted framework to explore the geometry of affine Deligne-Lusztig varieties (ADLV) The primary objective is to investigate the nonemptiness pattern, dimension and enumeration of irreducible components of ADLV. We provide a full mathematical proof of a newly identified problem concerning a certain lower bound of dimension.
  arXiv  Detail & Related papers  (2023-08-22T11:12:53Z)
• Rethinking Complex Queries on Knowledge Graphs with Neural Link Predictors [58.340159346749964]
  We propose a new neural-symbolic method to support end-to-end learning using complex queries with provable reasoning capability. We develop a new dataset containing ten new types of queries with features that have never been considered. Our method outperforms previous methods significantly in the new dataset and also surpasses previous methods in the existing dataset at the same time.
  arXiv  Detail & Related papers  (2023-04-14T11:35:35Z)
• Investigations into Proof Structures [0.8287206589886879]
  We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to Lukasiewicz.
  arXiv  Detail & Related papers  (2023-02-14T12:29:39Z)
• Full-Text Argumentation Mining on Scientific Publications [3.8754200816873787]
  We introduce a sequential pipeline model combining ADUR and ARE for full-text SAM. We provide a first analysis of the performance of pretrained language models (PLMs) on both subtasks. Our detailed error analysis reveals that non-contiguous ADUs as well as the interpretation of discourse connectors pose major challenges.
  arXiv  Detail & Related papers  (2022-10-24T10:05:30Z)
• Alchemy: A structured task distribution for meta-reinforcement learning [52.75769317355963]
  We introduce a new benchmark for meta-RL research, which combines structural richness with structural transparency. Alchemy is a 3D video game, which involves a latent causal structure that is resampled procedurally from episode to episode. We evaluate a pair of powerful RL agents on Alchemy and present an in-depth analysis of one of these agents.
  arXiv  Detail & Related papers  (2021-02-04T23:40:44Z)
• Summarizing Text on Any Aspects: A Knowledge-Informed Weakly-Supervised Approach [89.56158561087209]
  We study summarizing on arbitrary aspects relevant to the document. Due to the lack of supervision data, we develop a new weak supervision construction method and an aspect modeling scheme. Experiments show our approach achieves performance boosts on summarizing both real and synthetic documents.
  arXiv  Detail & Related papers  (2020-10-14T03:20:46Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.