ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving

• URL: http://arxiv.org/abs/2502.04671v2
• Date: Sat, 15 Feb 2025 08:02:36 GMT
• Title: ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving
• Authors: Amitayush Thakur, George Tsoukalas, Greg Durrett, Swarat Chaudhuri,
• Abstract summary: $rm Psmall ROOFWsmall ALA$ allows interaction between neural theorem-provers and two established interactive proof assistants (ITPs)<n>We show that a model trained on a mix of $rm Psmall ROOFWsmall ALA$-generated Coq and Lean data outperforms Lean-only and Coq-only models on the standard prove-at-$k$ metric.
• Score: 53.67926215943612
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural networks have shown substantial promise at automatic theorem-proving in interactive proof assistants (ITPs) like Lean and Coq. However, most neural theorem-proving models are restricted to specific ITPs, leaving out opportunities for cross-lingual $\textit{transfer}$ between ITPs. We address this weakness with a multilingual proof framework, ${\rm P{\small ROOF}W{\small ALA}}$, that allows a standardized form of interaction between neural theorem-provers and two established ITPs (Coq and Lean). It enables the collection of multilingual proof step data -- data recording the result of proof actions on ITP states -- for training neural provers. ${\rm P{\small ROOF}W{\small ALA}}$ allows the systematic evaluation of a model's performance across different ITPs and problem domains via efficient parallel proof search algorithms. We show that multilingual training enabled by ${\rm P{\small ROOF}W{\small ALA}}$ can lead to successful transfer across ITPs. Specifically, a model trained on a mix of ${\rm P{\small ROOF}W{\small ALA}}$-generated Coq and Lean data outperforms Lean-only and Coq-only models on the standard prove-at-$k$ metric. We open source all code including code for the ${\rm P{\small ROOF}W{\small ALA}}$ Framework (https://github.com/trishullab/proof-wala), and the Multilingual ITP interaction framework (https://github.com/trishullab/itp-interface).

Related papers

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a novel theorem proving method that enjoys superior sample efficiency. Our method is validated on the miniF2F-test benchmark using the open-source deepseek-math-7b-base model and the Isabelle proof assistant.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• Certifiably Robust Model Evaluation in Federated Learning under Meta-Distributional Shifts [8.700087812420687]
  We provide guarantees for the model's performance on a different, unseen network "B"<n>We show how the principled vanilla DKW bound enables certification of the model's true performance on unseen clients within the same (source) network.
  arXiv  Detail & Related papers  (2024-10-26T18:45:15Z)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  We introduce a novel approach for traversing the problem space using task decompositions.<n>We use the Large Language Models to plan a solution, soft-formalise the query into facts and predicates using a logic programming code.<n>Our method allows us to compute the faithfulness of the reasoning process w.r.t. the generated code and analyse the steps of the multi-hop search without relying on external solvers.
  arXiv  Detail & Related papers  (2024-10-14T19:39:11Z)
• Transfer Q Star: Principled Decoding for LLM Alignment [105.89114186982972]
  Transfer $Q*$ estimates the optimal value function for a target reward $r$ through a baseline model. Our approach significantly reduces the sub-optimality gap observed in prior SoTA methods.
  arXiv  Detail & Related papers  (2024-05-30T21:36:12Z)
• LAMPAT: Low-Rank Adaption for Multilingual Paraphrasing Using Adversarial Training [19.173992333194683]
  Paraphrases are texts that convey the same meaning while using different words or sentence structures. Previous studies have leveraged the knowledge from the machine translation field, forming a paraphrase through zero-shot machine translation in the same language. We propose the first unsupervised multilingual paraphrasing model, LAMPAT, by which monolingual dataset is sufficient enough to generate a human-like and diverse sentence.
  arXiv  Detail & Related papers  (2024-01-09T04:19:16Z)
• Blessing of Class Diversity in Pre-training [54.335530406959435]
  We prove that when the classes of the pre-training task are sufficiently diverse, pre-training can significantly improve the sample efficiency of downstream tasks. Our proof relies on a vector-form Rademacher complexity chain rule for composite function classes and a modified self-concordance condition.
  arXiv  Detail & Related papers  (2022-09-07T20:10:12Z)
• Learning (Very) Simple Generative Models Is Hard [45.13248517769758]
  We show that no-time algorithm can solve problem even when output coordinates of $mathbbRdtobbRd'$ are one-hidden-layer ReLU networks with $mathrmpoly(d)$ neurons. Key ingredient in our proof is an ODE-based construction of a compactly supported, piecewise-linear function $f$ with neurally-bounded slopes such that the pushforward of $mathcalN(0,1)$ under $f$ matches all low-degree moments of $mathcal
  arXiv  Detail & Related papers  (2022-05-31T17:59:09Z)
• Chunk-based Nearest Neighbor Machine Translation [7.747003493657217]
  We introduce a textitchunk-based $k$NN-MT model which retrieves chunks of tokens from the datastore, instead of a single token. Experiments on machine translation in two settings, static domain adaptation and on-the-fly'' adaptation, show that the chunk-based model leads to a significant speed-up (up to 4 times) with only a small drop in translation quality.
  arXiv  Detail & Related papers  (2022-05-24T17:39:25Z)
• Distributed Sparse Feature Selection in Communication-Restricted Networks [6.9257380648471765]
  We propose and theoretically analyze a new distributed scheme for sparse linear regression and feature selection. In order to infer the causal dimensions from the whole dataset, we propose a simple, yet effective method for information sharing in the network.
  arXiv  Detail & Related papers  (2021-11-02T05:02:24Z)
• Inconsistent Few-Shot Relation Classification via Cross-Attentional Prototype Networks with Contrastive Learning [16.128652726698522]
  We propose Prototype Network-based cross-attention contrastive learning (ProtoCACL) to capture the rich mutual interactions between the support set and query set. Experimental results demonstrate that our ProtoCACL can outperform the state-of-the-art baseline model under both inconsistent $K$ and inconsistent $N$ settings.
  arXiv  Detail & Related papers  (2021-10-13T07:47:13Z)
• On the Power of Multitask Representation Learning in Linear MDP [61.58929164172968]
  This paper presents analyses for the statistical benefit of multitask representation learning in linear Markov Decision Process (MDP) We first discover a emphLeast-Activated-Feature-Abundance (LAFA) criterion, denoted as $kappa$, with which we prove that a straightforward least-square algorithm learns a policy which is $tildeO(H2sqrtfrackappa mathcalC(Phi)2 kappa dNT+frackappa dn)
  arXiv  Detail & Related papers  (2021-06-15T11:21:06Z)
• Pre-training Multilingual Neural Machine Translation by Leveraging Alignment Information [72.2412707779571]
  mRASP is an approach to pre-train a universal multilingual neural machine translation model. We carry out experiments on 42 translation directions across a diverse setting, including low, medium, rich resource, and as well as transferring to exotic language pairs.
  arXiv  Detail & Related papers  (2020-10-07T03:57:54Z)
• Improving Robustness and Generality of NLP Models Using Disentangled Representations [62.08794500431367]
  Supervised neural networks first map an input $x$ to a single representation $z$, and then map $z$ to the output label $y$. We present methods to improve robustness and generality of NLP models from the standpoint of disentangled representation learning. We show that models trained with the proposed criteria provide better robustness and domain adaptation ability in a wide range of supervised learning tasks.
  arXiv  Detail & Related papers  (2020-09-21T02:48:46Z)
• Complementary Language Model and Parallel Bi-LRNN for False Trigger Mitigation [9.960986677222358]
  False trigger mitigation (FTM) is a process to detect the false trigger events and respond appropriately to the user. We propose a novel solution by introducing a parallel ASR decoding process with a special language model trained from "out-of-domain" data sources.
  arXiv  Detail & Related papers  (2020-08-18T18:21:33Z)

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.