Boldly Going Where No Prover Has Gone Before

• URL: http://arxiv.org/abs/1912.12958v1
• Date: Mon, 30 Dec 2019 15:14:10 GMT
• Title: Boldly Going Where No Prover Has Gone Before
• Authors: Giles Reger (University of Manchester)
• Abstract summary: I argue that the most interesting goal facing researchers in automated reasoning is being able to solve problems that cannot currently be solved by existing tools and methods. This may appear obvious, and is clearly not an original thought, but focusing on this as a primary goal allows us to examine other goals in a new light.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: I argue that the most interesting goal facing researchers in automated reasoning is being able to solve problems that cannot currently be solved by existing tools and methods. This may appear obvious, and is clearly not an original thought, but focusing on this as a primary goal allows us to examine other goals in a new light. Many successful theorem provers employ a portfolio of different methods for solving problems. This changes the landscape on which we perform our research: solving problems that can already be solved may not improve the state of the art and a method that can solve a handful of problems unsolvable by current methods, but generally performs poorly on most problems, can be very useful. We acknowledge that forcing new methods to compete against portfolio solvers can stifle innovation. However, this is only the case when comparisons are made at the level of total problems solved. We propose a movement towards focussing on unique solutions in evaluation and competitions i.e. measuring the potential contribution to a portfolio solver. This state of affairs is particularly prominent in first-order logic, which is undecidable. When reasoning in a decidable logic there can be a focus on optimising a decision procedure and measuring average solving times. But in a setting where solutions are difficult to find, average solving times lose meaning, and whilst improving the efficiency of a technique can move potential solutions within acceptable time limits, in general, complementary strategies may be more successful.

Related papers

• Optimisation Is Not What You Need [4.13365552362244]
  We show that optimisation methods share some fundamental flaws that impede them to become a true artificial cognition.<n>Specifically, the field have identified catastrophic forgetting as a fundamental problem to develop such cognition.<n>This paper formally proves that this problem is inherent to optimisation methods, and as such it will always limit approaches that try to solve the Artificial General Intelligence problem as an optimisation problem.
  arXiv  Detail & Related papers  (2025-07-03T08:50:20Z)
• Creativity or Brute Force? Using Brainteasers as a Window into the Problem-Solving Abilities of Large Language Models [28.791905315055974]
  We introduce a benchmark based on brainteasers written in long narrative form to probe more deeply into the types of reasoning strategies that models use.<n>Brainteasers can be solved with multiple approaches, such as a few-step solution that uses a creative insight or a longer solution that uses more brute force.
  arXiv  Detail & Related papers  (2025-05-16T04:23:34Z)
• Thoughts Are All Over the Place: On the Underthinking of o1-Like LLMs [86.79757571440082]
  Large language models (LLMs) such as OpenAI's o1 have demonstrated remarkable abilities in complex reasoning tasks. We identify a phenomenon we term underthinking, where o1-like LLMs frequently switch between different reasoning thoughts. We propose a decoding strategy with thought switching penalty TIP that discourages premature transitions between thoughts.
  arXiv  Detail & Related papers  (2025-01-30T18:58:18Z)
• Learning Multiple Initial Solutions to Optimization Problems [52.9380464408756]
  Sequentially solving similar optimization problems under strict runtime constraints is essential for many applications. We propose learning to predict emphmultiple diverse initial solutions given parameters that define the problem instance. We find significant and consistent improvement with our method across all evaluation settings and demonstrate that it efficiently scales with the number of initial solutions required.
  arXiv  Detail & Related papers  (2024-11-04T15:17:19Z)
• BloomWise: Enhancing Problem-Solving capabilities of Large Language Models using Bloom's-Taxonomy-Inspired Prompts [59.83547898874152]
  We introduce BloomWise, a new prompting technique, inspired by Bloom's taxonomy, to improve the performance of Large Language Models (LLMs) The decision regarding the need to employ more sophisticated cognitive skills is based on self-evaluation performed by the LLM. In extensive experiments across 4 popular math reasoning datasets, we have demonstrated the effectiveness of our proposed approach.
  arXiv  Detail & Related papers  (2024-10-05T09:27:52Z)
• Exploring the Performance-Reproducibility Trade-off in Quality-Diversity [7.858994681440057]
  Quality-Diversity (QD) algorithms have exhibited promising results across many domains and applications. However, uncertainty in fitness and behaviour estimations of solutions remains a major challenge when QD is used in complex real-world applications. We propose four new a-priori QD algorithms that find optimal solutions for given preferences over the trade-offs.
  arXiv  Detail & Related papers  (2024-09-20T08:20:31Z)
• Divide-or-Conquer? Which Part Should You Distill Your LLM? [38.62667131299918]
  We devise a similar strategy that breaks down reasoning tasks into a problem decomposition phase and a problem solving phase. We show that the strategy is able to outperform a single stage solution.
  arXiv  Detail & Related papers  (2024-02-22T22:28:46Z)
• Efficient anytime algorithms to solve the bi-objective Next Release Problem [2.8148957592979422]
  Next Release Problem consists in selecting a subset of requirements to develop in the next release of a software product. We propose five new methods that maintain a well-spread set of solutions at any time during the search.
  arXiv  Detail & Related papers  (2024-02-07T05:03:31Z)
• Attention-based Reinforcement Learning for Combinatorial Optimization: Application to Job Shop Scheduling Problem [2.024210754085351]
  This study proposes an innovative attention-based reinforcement learning method specifically designed for the category of job shop scheduling problems. A key finding of this research is the ability of our trained learners within the proposed method to be repurposed for larger-scale problems that were not part of the initial training set.
  arXiv  Detail & Related papers  (2024-01-29T21:31:54Z)
• Thought Propagation: An Analogical Approach to Complex Reasoning with Large Language Models [62.96551299003463]
  We propose textbftextitThought Propagation (TP) to enhance the complex reasoning ability of Large Language Models. TP first prompts LLMs to propose and solve a set of analogous problems that are related to the input one. TP reuses the results of analogous problems to directly yield a new solution or derive a knowledge-intensive plan for execution to amend the initial solution obtained from scratch.
  arXiv  Detail & Related papers  (2023-10-06T01:40:09Z)
• Light Unbalanced Optimal Transport [69.18220206873772]
  Existing solvers are either based on principles or heavy-weighted with complex optimization objectives involving several neural networks. We show that our solver provides a universal approximation of UEOT solutions and obtains its generalization bounds.
  arXiv  Detail & Related papers  (2023-03-14T15:44:40Z)
• On solving decision and risk management problems subject to uncertainty [91.3755431537592]
  Uncertainty is a pervasive challenge in decision and risk management. This paper develops a systematic understanding of such strategies, determine their range of application, and develop a framework to better employ them.
  arXiv  Detail & Related papers  (2023-01-18T19:16:23Z)
• A Framework for Inherently Interpretable Optimization Models [0.0]
  Solution of large-scale problems that seemed intractable decades ago are now a routine task. One major barrier is that the optimization software can be perceived as a black box. We propose an optimization framework to derive solutions that inherently come with an easily comprehensible explanatory rule.
  arXiv  Detail & Related papers  (2022-08-26T10:32:00Z)
• Learning Proximal Operators to Discover Multiple Optima [66.98045013486794]
  We present an end-to-end method to learn the proximal operator across non-family problems. We show that for weakly-ized objectives and under mild conditions, the method converges globally.
  arXiv  Detail & Related papers  (2022-01-28T05:53:28Z)
• A Mutual Information Maximization Approach for the Spurious Solution Problem in Weakly Supervised Question Answering [60.768146126094955]
  Weakly supervised question answering usually has only the final answers as supervision signals. There may exist many spurious solutions that coincidentally derive the correct answer, but training on such solutions can hurt model performance. We propose to explicitly exploit such semantic correlations by maximizing the mutual information between question-answer pairs and predicted solutions.
  arXiv  Detail & Related papers  (2021-06-14T05:47:41Z)
• Learning by Fixing: Solving Math Word Problems with Weak Supervision [70.62896781438694]
  Previous neural solvers of math word problems (MWPs) are learned with full supervision and fail to generate diverse solutions. We introduce a textitweakly-supervised paradigm for learning MWPs. Our method only requires the annotations of the final answers and can generate various solutions for a single problem.
  arXiv  Detail & Related papers  (2020-12-19T03:10:21Z)

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.