Prolog Technology Reinforcement Learning Prover

• URL: http://arxiv.org/abs/2004.06997v1
• Date: Wed, 15 Apr 2020 10:52:04 GMT
• Title: Prolog Technology Reinforcement Learning Prover
• Authors: Zsolt Zombori, Josef Urban, Chad E. Brown
• Abstract summary: The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs.
• Score: 0.6445605125467572
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.

Related papers

• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but it is expensive. Recent research has used machine learning to automatically synthesize proofs, reducing verification effort, but these tools are able to prove only a fraction of the desired software properties. We introduce Cobblestone, a new proof-synthesis approach that improves on the state of the art by taking advantage of partial progress in proof synthesis attempts.
  arXiv  Detail & Related papers  (2024-10-25T19:25:00Z)
• To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoning [55.52872152909785]
  Chain-of-thought (CoT) via prompting is the de facto method for eliciting reasoning capabilities from large language models (LLMs) We show that CoT gives strong performance benefits primarily on tasks involving math or logic, with much smaller gains on other types of tasks.
  arXiv  Detail & Related papers  (2024-09-18T17:55:00Z)
• CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
  This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data.
  arXiv  Detail & Related papers  (2024-05-07T12:50:28Z)
• StepCoder: Improve Code Generation with Reinforcement Learning from Compiler Feedback [58.20547418182074]
  We introduce StepCoder, a novel framework for code generation, consisting of two main components. CCCS addresses the exploration challenge by breaking the long sequences code generation task into a Curriculum of Code Completion Subtasks. FGO only optimize the model by masking the unexecuted code segments to provide Fine-Grained Optimization. Our method improves the ability to explore the output space and outperforms state-of-the-art approaches in corresponding benchmarks.
  arXiv  Detail & Related papers  (2024-02-02T13:14:31Z)
• Generalized Convergence Analysis of Tsetlin Machines: A Probabilistic Approach to Concept Learning [20.519261060300302]
  This paper presents a comprehensive convergence analysis of Tsetlin automaton-based Machine Learning algorithms. We introduce a novel framework, referred to as Probabilistic Concept Learning (PCL), which simplifies the TM structure. We establish a theoretical proof confirming that, for any clause $C_k$, PCL converges to a conjunction of literals when $0.5p_k1$.
  arXiv  Detail & Related papers  (2023-10-03T12:21:41Z)
• Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis [0.0]
  We present a reinforcement-learning algorithm for SyGuS which uses Monte-Carlo Tree Search (MCTS) to search the space of candidate solutions. Our algorithm learns policy and value functions which, combined with the upper confidence bound for trees, allow it to balance exploration and exploitation.
  arXiv  Detail & Related papers  (2023-07-13T11:30:50Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. Existing methods are difficult to reproduce or build on, due to private code, data, and compute requirements. This paper introduces LeanDojo: an open-source Lean toolkit consisting of toolkits, data, models. We develop ReProver: an LLM-based prover augmented with retrieval for selecting premises from a vast math library.
  arXiv  Detail & Related papers  (2023-06-27T17:05:32Z)
• Evaluating and Improving Tool-Augmented Computation-Intensive Math Reasoning [75.74103236299477]
  Chain-of-thought prompting(CoT) and tool augmentation have been validated as effective practices for improving large language models. We propose a new approach that can deliberate the reasoning steps with tool interfaces, namely textbfDELI. Experimental results on CARP and six other datasets show that the proposed DELI mostly outperforms competitive baselines.
  arXiv  Detail & Related papers  (2023-06-04T17:02:59Z)
• CLAWSAT: Towards Both Robust and Accurate Code Models [74.57590254102311]
  We integrate contrastive learning (CL) with adversarial learning to co-optimize the robustness and accuracy of code models. To the best of our knowledge, this is the first systematic study to explore and exploit the robustness and accuracy benefits of (multi-view) code obfuscations in code models.
  arXiv  Detail & Related papers  (2022-11-21T18:32:50Z)
• Latte: Cross-framework Python Package for Evaluation of Latent-Based Generative Models [65.51757376525798]
  Latte is a Python library for evaluation of latent-based generative models. Latte is compatible with both PyTorch and/Keras, and provides both functional and modular APIs.
  arXiv  Detail & Related papers  (2021-12-20T16:00:28Z)
• PalmTree: Learning an Assembly Language Model for Instruction Embedding [8.74990895782223]
  We propose to pre-train an assembly language model called PalmTree for generating general-purpose instruction embeddings. PalmTree has the best performance for intrinsic metrics, and outperforms the other instruction embedding schemes for all downstream tasks.
  arXiv  Detail & Related papers  (2021-01-21T22:30:01Z)

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.