Real-rootedness of rook-Eulerian polynomials
Authors:
Per Alexandersson,
Aryaman Jal,
Maena Quemener
Abstract:
We introduce rook-Eulerian polynomials, a generalization of the classical Eulerian polynomials arising from complete rook placements on Ferrers boards, and prove that they are real-rooted. We show that a natural context in which to interpret these rook placements is as lower intervals of $312$-avoiding permutations in the Bruhat order. We end with some variations and generalizations along this the…
▽ More
We introduce rook-Eulerian polynomials, a generalization of the classical Eulerian polynomials arising from complete rook placements on Ferrers boards, and prove that they are real-rooted. We show that a natural context in which to interpret these rook placements is as lower intervals of $312$-avoiding permutations in the Bruhat order. We end with some variations and generalizations along this theme.
△ Less
Submitted 9 February, 2025;
originally announced February 2025.
CoProver: A Recommender System for Proof Construction
Authors:
Eric Yeh,
Briland Hitaj,
Sam Owre,
Maena Quemener,
Natarajan Shankar
Abstract:
Interactive Theorem Provers (ITPs) are an indispensable tool in the arsenal of formal method experts as a platform for construction and (formal) verification of proofs. The complexity of the proofs in conjunction with the level of expertise typically required for the process to succeed can often hinder the adoption of ITPs. A recent strain of work has investigated methods to incorporate machine le…
▽ More
Interactive Theorem Provers (ITPs) are an indispensable tool in the arsenal of formal method experts as a platform for construction and (formal) verification of proofs. The complexity of the proofs in conjunction with the level of expertise typically required for the process to succeed can often hinder the adoption of ITPs. A recent strain of work has investigated methods to incorporate machine learning models trained on ITP user activity traces as a viable path towards full automation. While a valuable line of investigation, many problems still require human supervision to be completed fully, thus applying learning methods to assist the user with useful recommendations can prove more fruitful.
Following the vein of user assistance, we introduce CoProver, a proof recommender system based on transformers, capable of learning from past actions during proof construction, all while exploring knowledge stored in the ITP concerning previous proofs. CoProver employs a neurally learnt sequence-based encoding of sequents, capturing long distance relationships between terms and hidden cues therein. We couple CoProver with the Prototype Verification System (PVS) and evaluate its performance on two key areas, namely: (1) Next Proof Action Recommendation, and (2) Relevant Lemma Retrieval given a library of theories. We evaluate CoProver on a series of well-established metrics originating from the recommender system and information retrieval communities, respectively. We show that CoProver successfully outperforms prior state of the art applied to recommendation in the domain. We conclude by discussing future directions viable for CoProver (and similar approaches) such as argument prediction, proof summarization, and more.
△ Less
Submitted 1 March, 2023;
originally announced April 2023.
