arXiv subjects

Benjamin Breen

Publications and source records attributed to Benjamin Breen.

5 recordsLinked to original sources

arXiv2026

AxDafny: Agentic Verified Code Generation in Dafny

We study agentic code generation in Dafny, where a model must generate both executable code and the proof artifacts for verification. We present AxDafny, a verifier-guided repair framework that iteratively generates implementations, invariants, assertions, and termination arguments. We also introduce LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny), a benchmark of 250 competition-style programming problems translated into Dafny with formal specifications and a verifier-based evaluation harness. On LCB-Pro-Dafny, AxDafny substantially improves verification success over baseline GPT-5.5 performance. On DafnyBench, AxDafny achieves 92.7\% verification success, outperforming the strongest previously reported proof-hint baseline by 6.5 percentage points. Lastly, we show that verification success and runtime test performance measure different aspects of generated code.

cs.AI↗

arXiv2025

Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

We present Ax-Prover, a multi-agent system for automated theorem proving in Lean that can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts. To achieve this, Ax-Prover approaches scientific problem solving through formal proof generation, a process that demands both creative reasoning and strict syntactic rigor. Ax-Prover meets this challenge by equipping Large Language Models (LLMs), which provide knowledge and reasoning, with Lean tools via the Model Context Protocol (MCP), which ensure formal correctness. To evaluate its performance as an autonomous prover, we benchmark our approach against frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks we introduce in the fields of abstract algebra and quantum theory. On public datasets, Ax-Prover is competitive with state-of-the-art provers, while it largely outperforms them on the new benchmarks. This shows that, unlike specialized systems that struggle to generalize, our tool-based agentic theorem prover approach offers a generalizable methodology for formal verification across diverse scientific domains. Furthermore, we demonstrate Ax-Prover's assistant capabilities in a practical use case, showing how it enabled an expert mathematician to formalize the proof of a complex cryptography theorem.

cs.AI↗

arXiv2021

The 2-Selmer group of $S_n$-number fields of even degree

This paper is an extension of the work of Dummit and Voight on modeling the 2-Selmer group of number fields. We extend their model to $S_n$-number fields of even degree and develop heuristics on the difference in the 2-ranks between the class group and narrow class group.

math.NT↗

arXiv2019

On unit signatures and narrow class groups of odd degree abelian number fields

For an abelian number field of odd degree, we study the structure of its 2-Selmer group as a bilinear space and as a Galois module. We prove structural results and make predictions for the distribution of unit signature ranks and narrow class groups in families where the degree and Galois group are fixed.

math.NT↗

arXiv2015

Wild ramification in a family of low-degree extensions arising from iteration

This article gives a first look at wild ramification in a family of iterated extensions. For integer values of c, we consider the splitting field of $(x^2 + c)^2 + c$, the second iterate of $x^2 + c$. We give complete information on the factorization of the ideal (2) as c varies, and find a surprisingly complicated dependence of this factorization on the parameter c. We show that 2 ramifies (necessarily wildly) in all these extensions except when c = 0, and we describe the higher ramification groups in some totally ramified cases.

math.NT↗