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

• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Reassessing Large Language Model Boolean Query Generation for Systematic Reviews [33.74979207094165]
  Large Language Models (LLMs) have been developed to assist in the development of complex queries.<n>This work systematically reproduces two studies that overlooked key aspects of the original work.<n>Our results show that query effectiveness varies significantly across models and prompt designs.<n>Our findings highlight the importance of model- and prompt-specific optimisations.
  arXiv  Detail & Related papers  (2025-05-12T00:15:02Z)
• Theoretical Foundations of Conformal Prediction [15.884682750072399]
  Conformal prediction and related inferential techniques are useful in a diverse array of tasks. Conformal prediction's main appeal is its ability to provide formal, finite-sample guarantees. The goal of this book is to teach the reader about the fundamental technical arguments that arise when researching conformal prediction.
  arXiv  Detail & Related papers  (2024-11-18T18:44:00Z)
• Graph Stochastic Neural Process for Inductive Few-shot Knowledge Graph Completion [63.68647582680998]
  We focus on a task called inductive few-shot knowledge graph completion (I-FKGC) Inspired by the idea of inductive reasoning, we cast I-FKGC as an inductive reasoning problem. We present a neural process-based hypothesis extractor that models the joint distribution of hypothesis, from which we can sample a hypothesis for predictions. In the second module, based on the hypothesis, we propose a graph attention-based predictor to test if the triple in the query set aligns with the extracted hypothesis.
  arXiv  Detail & Related papers  (2024-08-03T13:37:40Z)
• 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)
• 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)
• 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.