arXiv subjects

Nilay Patel

Publications and source records attributed to Nilay Patel.

4 recordsLinked to original sources

arXiv2026

Patterned fronts in the wake of a parameter ramp in the complex Ginzburg Landau equation

We study of the formation of pattern-forming fronts in the presence of a rigidly-propagating parameter ramp which is slowly-varying in space. In the context of the prototypical supercritical complex Ginzburg-Landau equation, we show that not only the leading order front interface, but also the selected spatial wave number is governed by the transition of the ramp between absolute and convective instability. The slow ramp then induces a further delay of the front interface and perturbation of the selected wave number, controlled by the slow passage near a complex fold of strong- and weak-stable eigenspaces. To analyze the behavior near this fold, we perform a multiple scales analysis to predict the higher-order front interface delay in terms of zeros and poles of a complex Airy quotient inner solution. We confirm these predictions with numerical continuation of heteroclinics in the associated traveling wave equation. We also numerically characterize their spectral stability, finding accumulation of eigenvalues consistent with previous results on slow absolute spectrum. We then show the leading-order absolute/convective instability heuristic accurately describes selected wave numbers in an analogous slowly-ramped Swift-Hohenberg equation.

nlin.PS↗

arXiv2026

MathAtlas: A Benchmark for Autoformalization in the Wild

Current autoformalization benchmarks are largely focused on olympiad or undergraduate mathematics, while graduate and research-level mathematics remains underexplored. In this paper, we introduce MathAtlas, the first large-scale autoformalization benchmark of in the wild graduate-level mathematics, containing ~52k theorems, definitions, exercises, examples, and proofs extracted from 103 graduate mathematics textbooks. MathAtlas is enriched with a mathematical dependency graph containing ~178k relations, and is the first autoformalization benchmark to include such relations, facilitating evaluation and development of dependency-aware autoformalization systems. Our extensive experiments show that MathAtlas is high quality but extremely challenging: strong baselines achieve at most 9.8% correctness on theorem statements and 16.7% on definitions. Furthermore, we find performance of state-of-the-art models degrades substantially with dependency depth: on MA-Hard, a subset of 700 entities with the deepest dependency trees, the best model achieves only 2.6% correctness for autoformalization on this challenging dataset. We release MathAtlas to the community as a benchmark set for large-scale autoformalization of graduate-level mathematics in the wild.

cs.AI↗

arXiv2023

A New Approach Towards Autoformalization

Verifying mathematical proofs is difficult, but can be automated with the assistance of a computer. Autoformalization is the task of automatically translating natural language mathematics into a formal language that can be verified by a program. This is a challenging task, and especially for higher-level mathematics found in research papers. Research paper mathematics requires large amounts of background and context. In this paper, we propose an avenue towards tackling autoformalization for research-level mathematics, by breaking the task into easier and more approachable subtasks: unlinked formalization (formalization with unlinked definitions and theorems), entity linking (linking to the proper theorems and definitions), and finally adjusting types so it passes the type checker. In addition, we present arXiv2Formal, a benchmark dataset for unlinked formalization consisting of 50 theorems formalized for the Lean theorem prover sampled from papers on arXiv.org. We welcome any contributions from the community to future versions of this dataset.

cs.CL↗

arXiv2023

Forming Trees with Treeformers

Human language is known to exhibit a nested, hierarchical structure, allowing us to form complex sentences out of smaller pieces. However, many state-of-the-art neural networks models such as Transformers have no explicit hierarchical structure in its architecture -- that is, they don't have an inductive bias toward hierarchical structure. Additionally, Transformers are known to perform poorly on compositional generalization tasks which require such structures. In this paper, we introduce Treeformer, a general-purpose encoder module inspired by the CKY algorithm which learns a composition operator and pooling function to construct hierarchical encodings for phrases and sentences. Our extensive experiments demonstrate the benefits of incorporating hierarchical structure into the Transformer and show significant improvements in compositional generalization as well as in downstream tasks such as machine translation, abstractive summarization, and various natural language understanding tasks.

cs.CL↗