More Like this

1. Learning to find proofs and theorems by learning to refine search strategies

   Laurent, Jonathan; Platzer, André (November 2022, Advances in neural information processing systems)

   Agarwal, Alekh; Belgrave, Danielle; Cho, Kyunghyun; Oh, Alice (Ed.)

   We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard to synthesize. As a specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies. 

   more » « less
2. Learning to Prove Theorems via Interacting with Proof Assistants

   Yang, Kaiyu; Deng, Jia (June 2019, International Conference on Machine Learning)
3. Sparse Representer Theorems for Learning in Reproducing Kernel Banach Spaces

   Wang, Rui; Xu, Yuesheng; Yan, Mingsong (February 2024, Journal of machine learning research)

   Sparsity of a learning solution is a desirable feature in machine learning. Certain reproducing kernel Banach spaces (RKBSs) are appropriate hypothesis spaces for sparse learning methods. The goal of this paper is to understand what kind of RKBSs can promote sparsity for learning solutions. We consider two typical learning models in an RKBS: the minimum norm interpolation (MNI) problem and the regularization problem. We first establish an explicit representer theorem for solutions of these problems, which represents the extreme points of the solution set by a linear combination of the extreme points of the subdifferential set, of the norm function, which is data-dependent. We then propose sufficient conditions on the RKBS that can transform the explicit representation of the solutions to a sparse kernel representation having fewer terms than the number of the observed data. Under the proposed sufficient conditions, we investigate the role of the regularization parameter on sparsity of the regularized solutions. We further show that two specific RKBSs, the sequence space l_1(N) and the measure space, can have sparse representer theorems for both MNI and regularization models. 

   more » « less
4. Is it Easier to Prove Theorems that are Guaranteed to be True?

   https://doi.org/10.1109/FOCS46700.2020.00119  

   Pass, Rafael; Venkitasubramaniam, Muthuramakrishnan (November 2020, FOCS'20)

   null (Ed.)
5. Is it Easier to Prove Theorems that are Guaranteed to be True?

   Pass, Rafael Pass; Venkitasubramaniam, Muthuramakrishnan (January 2020, IEEE Symposium on Foundations of Computer Science)

   null (Ed.)

   Consider the following two fundamental open problems in complexity theory: • Does a hard-on-average language in NP imply the existence of one-way functions? • Does a hard-on-average language in NP imply a hard-on-average problem in TFNP (i.e., the class of total NP search problem)? Our main result is that the answer to (at least) one of these questions is yes. Both one-way functions and problems in TFNP can be interpreted as promise-true distributional NP search problems—namely, distributional search problems where the sampler only samples true statements. As a direct corollary of the above result, we thus get that the existence of a hard-on-average distributional NP search problem implies a hard-on-average promise-true distributional NP search problem. In other words, It is no easier to find witnesses (a.k.a. proofs) for efficiently-sampled statements (theorems) that are guaranteed to be true. This result follows from a more general study of interactive puzzles—a generalization of average-case hardness in NP—and in particular, a novel round-collapse theorem for computationallysound protocols, analogous to Babai-Moran’s celebrated round-collapse theorem for informationtheoretically sound protocols. As another consequence of this treatment, we show that the existence of O(1)-round public-coin non-trivial arguments (i.e., argument systems that are not proofs) imply the existence of a hard-on-average problem in NP/poly. 

   more » « less