Towards United Reasoning for Automatic Induction in Isabelle/HOL
- URL: http://arxiv.org/abs/2005.12737v1
- Date: Mon, 25 May 2020 08:30:05 GMT
- Title: Towards United Reasoning for Automatic Induction in Isabelle/HOL
- Authors: Yutaka Nagashima
- Abstract summary: We propose united reasoning, a novel approach to further automating inductive theorem proving.
After success, united reasoning takes the best of three schools of reasoning: deductive reasoning, inductive reasoning, and inductive reasoning.
- Score: 6.85316573653194
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Inductive theorem proving is an important long-standing challenge in computer
science. In this extended abstract, we first summarize the recent developments
of proof by induction for Isabelle/HOL. Then, we propose united reasoning, a
novel approach to further automating inductive theorem proving. Upon success,
united reasoning takes the best of three schools of reasoning: deductive
reasoning, inductive reasoning, and inductive reasoning, to prove difficult
inductive problems automatically.
Related papers
- Abductive Computational Systems: Creative Abduction and Future Directions [4.315465190486744]
Abductive reasoning is often mentioned in scientific, design-related and artistic contexts.<n>This paper reviews how abductive reasoning is discussed in theoretical science and design, and then analyses how various computational systems use abductive reasoning.
arXiv Detail & Related papers (2025-07-11T02:21:41Z) - Inductive or Deductive? Rethinking the Fundamental Reasoning Abilities of LLMs [99.76347807139615]
Reasoning encompasses two typical types: deductive reasoning and inductive reasoning.
Despite extensive research into the reasoning capabilities of Large Language Models (LLMs), most studies have failed to rigorously differentiate between inductive and deductive reasoning.
This raises an essential question: In LLM reasoning, which poses a greater challenge - deductive or inductive reasoning?
arXiv Detail & Related papers (2024-07-31T18:47:11Z) - Learning Guided Automated Reasoning: A Brief Survey [5.607616497275423]
We provide an overview of several automated reasoning and theorem proving domains and the learning and AI methods that have been so far developed for them.
These include premise selection, proof guidance in several settings, feedback loops iterating between reasoning and learning, and symbolic classification problems.
arXiv Detail & Related papers (2024-03-06T19:59:17Z) - Implicit Chain of Thought Reasoning via Knowledge Distillation [58.80851216530288]
Instead of explicitly producing the chain of thought reasoning steps, we use the language model's internal hidden states to perform implicit reasoning.
We find that this approach enables solving tasks previously not solvable without explicit chain-of-thought, at a speed comparable to no chain-of-thought.
arXiv Detail & Related papers (2023-11-02T17:59:49Z) - Phenomenal Yet Puzzling: Testing Inductive Reasoning Capabilities of Language Models with Hypothesis Refinement [92.61557711360652]
Language models (LMs) often fall short on inductive reasoning, despite achieving impressive success on research benchmarks.
We conduct a systematic study of the inductive reasoning capabilities of LMs through iterative hypothesis refinement.
We reveal several discrepancies between the inductive reasoning processes of LMs and humans, shedding light on both the potentials and limitations of using LMs in inductive reasoning tasks.
arXiv Detail & Related papers (2023-10-12T17:51:10Z) - Deductive Verification of Chain-of-Thought Reasoning [22.79166959432764]
Large Language Models (LLMs) benefit from Chain-of-Thought prompting in performing various reasoning tasks.
While CoT allows models to produce more comprehensive reasoning processes, its emphasis on intermediate reasoning steps can inadvertently introduce hallucinations and accumulated errors.
We propose Natural Program, a natural language-based deductive reasoning format.
arXiv Detail & Related papers (2023-06-06T17:18:56Z) - Abductive Commonsense Reasoning Exploiting Mutually Exclusive
Explanations [118.0818807474809]
Abductive reasoning aims to find plausible explanations for an event.
Existing approaches for abductive reasoning in natural language processing often rely on manually generated annotations for supervision.
This work proposes an approach for abductive commonsense reasoning that exploits the fact that only a subset of explanations is correct for a given context.
arXiv Detail & Related papers (2023-05-24T01:35:10Z) - MetaLogic: Logical Reasoning Explanations with Fine-Grained Structure [129.8481568648651]
We propose a benchmark to investigate models' logical reasoning capabilities in complex real-life scenarios.
Based on the multi-hop chain of reasoning, the explanation form includes three main components.
We evaluate the current best models' performance on this new explanation form.
arXiv Detail & Related papers (2022-10-22T16:01:13Z) - Maieutic Prompting: Logically Consistent Reasoning with Recursive
Explanations [71.2950434944196]
We develop Maieutic Prompting, which infers a correct answer to a question even from the noisy and inconsistent generations of language models.
Maieutic Prompting achieves up to 20% better accuracy than state-of-the-art prompting methods.
arXiv Detail & Related papers (2022-05-24T06:36:42Z) - Explaining AI as an Exploratory Process: The Peircean Abduction Model [0.2676349883103404]
Abductive inference has been defined in many ways.
Challenge of implementing abductive reasoning and the challenge of automating the explanation process are closely linked.
This analysis provides a theoretical framework for understanding what the XAI researchers are already doing.
arXiv Detail & Related papers (2020-09-30T17:10:37Z) - Smart Induction for Isabelle/HOL (System Description) [6.85316573653194]
smart_induct lists promising arguments for the induct tactic without relying on a search.
Our evaluation demonstrated smart_induct produces valuable recommendations across problem domains.
arXiv Detail & Related papers (2020-01-27T15:29:34Z)
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.