Graph2Tac: Online Representation Learning of Formal Math Concepts

• URL: http://arxiv.org/abs/2401.02949v3
• Date: Sun, 23 Jun 2024 13:54:33 GMT
• Title: Graph2Tac: Online Representation Learning of Formal Math Concepts
• Authors: Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun,
• Abstract summary: In proof, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance. We show that this locality property can be exploited through online learning techniques to obtain solving agents that far surpass offline learners. We benchmark two such online solvers implemented in the Tactician platform for the Coq proof assistant.
• Score: 0.6597195879147557
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In proof assistants, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance. Furthermore, lemmas with close proximity regularly exhibit similar proof structures. We show that this locality property can be exploited through online learning techniques to obtain solving agents that far surpass offline learners when asked to prove theorems in an unseen mathematical setting. We extensively benchmark two such online solvers implemented in the Tactician platform for the Coq proof assistant: First, Tactician's online $k$-nearest neighbor solver, which can learn from recent proofs, shows a $1.72\times$ improvement in theorems proved over an offline equivalent. Second, we introduce a graph neural network, Graph2Tac, with a novel approach to build hierarchical representations for new definitions. Graph2Tac's online definition task realizes a $1.5\times$ improvement in theorems solved over an offline baseline. The $k$-NN and Graph2Tac solvers rely on orthogonal online data, making them highly complementary. Their combination improves $1.27\times$ over their individual performances. Both solvers outperform all other general-purpose provers for Coq, including CoqHammer, Proverbot9001, and a transformer baseline by at least $1.48\times$ and are available for practical use by end-users.

Related papers

• Efficient Solution of Point-Line Absolute Pose [52.775981113238046]
  We revisit certain problems of pose estimation based on 3D--2D correspondences between features which may be points or lines. We show experimentally that the resulting solvers are numerically stable and fast.
  arXiv  Detail & Related papers  (2024-04-25T12:09:16Z)
• Efficient Methods for Non-stationary Online Learning [67.3300478545554]
  We present efficient methods for optimizing dynamic regret and adaptive regret, which reduce the number of projections per round from $mathcalO(log T)$ to $1$. Our technique hinges on the reduction mechanism developed in parameter-free online learning and requires non-trivial twists on non-stationary online methods.
  arXiv  Detail & Related papers  (2023-09-16T07:30:12Z)
• Reduction Algorithms for Persistence Diagrams of Networks: CoralTDA and PrunIT [27.411830935369498]
  High computational costs remain the primary roadblock hindering the successful application of topological data analysis. We develop two new, remarkably simple but effective algorithms to compute the exact persistence diagrams of large graphs. Our experiments on large networks show that our novel approach can achieve computational gains up to 95%.
  arXiv  Detail & Related papers  (2022-11-24T16:52:48Z)
• PDE-Based Optimal Strategy for Unconstrained Online Learning [40.61498562988079]
  We present a framework that generates time-varying potential functions by solving a Partial Differential Equation (PDE) Our framework recovers some classical potentials, and more importantly provides a systematic approach to design new ones. This is the first parameter-free algorithm with optimal leading constant.
  arXiv  Detail & Related papers  (2022-01-19T22:21:21Z)
• Training Free Graph Neural Networks for Graph Matching [103.45755859119035]
  TFGM is a framework to boost the performance of Graph Neural Networks (GNNs) based graph matching without training. Applying TFGM on various GNNs shows promising improvements over baselines.
  arXiv  Detail & Related papers  (2022-01-14T09:04:46Z)
• Provably Efficient Generative Adversarial Imitation Learning for Online and Offline Setting with Linear Function Approximation [81.0955457177017]
  In generative adversarial imitation learning (GAIL), the agent aims to learn a policy from an expert demonstration so that its performance cannot be discriminated from the expert policy on a certain reward set. We study GAIL in both online and offline settings with linear function approximation, where both the transition and reward function are linear in the feature maps.
  arXiv  Detail & Related papers  (2021-08-19T16:16:00Z)
• Online Machine Learning Techniques for Coq: A Comparison [2.9412498294532856]
  We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs.
  arXiv  Detail & Related papers  (2021-04-12T05:12:35Z)
• Online Apprenticeship Learning [58.45089581278177]
  In Apprenticeship Learning (AL), we are given a Markov Decision Process (MDP) without access to the cost function. The goal is to find a policy that matches the expert's performance on some predefined set of cost functions. We show that the OAL problem can be effectively solved by combining two mirror descent based no-regret algorithms.
  arXiv  Detail & Related papers  (2021-02-13T12:57:51Z)
• Learning Bayesian Networks Under Sparsity Constraints: A Parameterized Complexity Analysis [7.99536002595393]
  We study the problem of learning the structure of an optimal Bayesian network when additional constraints are posed on the network or on its moralized graph. We show that learning an optimal network with at most $k$ edges in the moralized graph presumably has no $f(k)cdot |I|O(1)$-time algorithm.
  arXiv  Detail & Related papers  (2020-04-30T12:31:13Z)
• Geometrically Principled Connections in Graph Neural Networks [66.51286736506658]
  We argue geometry should remain the primary driving force behind innovation in the emerging field of geometric deep learning. We relate graph neural networks to widely successful computer graphics and data approximation models: radial basis functions (RBFs) We introduce affine skip connections, a novel building block formed by combining a fully connected layer with any graph convolution operator.
  arXiv  Detail & Related papers  (2020-04-06T13:25: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.