arXiv subjects

Alessandro Sosso

Publications and source records attributed to Alessandro Sosso.

3 recordsLinked to original sources

arXiv2026

Agentic Proving for Program Verification

Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification, we evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation. Our results show that Claude generates arguably valid specifications for 98.8% of problems (with 81.3% also accepted by CLEVER's isomorphism-based scoring on the correct portion of the benchmark), certifies implementations against correct ground-truth specifications for 87.5% of problems, and reaches a 98.1% success rate on the end-to-end program generation and verification pipeline over entries with self-consistent premises. Across all stages, Claude further provides high-quality feedback on its own attempts (as confirmed under manual review), identifying underlying causes of failure and lingering bugs in the dataset. These findings highlight a growing mismatch between the difficulty of existing program verification benchmarks and the capabilities of modern agentic provers, and point to the need for more rigorous, bug-resilient evaluation methodologies, and in particular for alternatives to isomorphism-based scoring of generated specifications. More broadly, our results provide empirical evidence that tight compiler-in-the-loop agentic paradigms are currently the most effective approach for foundational program verification.

cs.AI↗

arXiv2025

The Cloven Traveling Salesman: Cycle Covers and the Integrality Gap of Small ATSP Instances

This work proposes a novel enumeration algorithm for computing the integrality gap of small instances of the subtour elimination formulation for the Asymmetric Traveling Salesman Problem (ATSP).The core idea is to enumerate pairs of cycle covers that can be filtered and mapped to half-integer vertices of the subtour elimination polytope. The two-cycle covers are encoded as lexicographically ordered partitions of $n$ numbers, with an encoding that prevents the generation of several isomorphic vertices. However, since not every cycle cover pair can be mapped to a vertex of the subtour elimination polytope, we have designed an efficient property-checking procedure to control whether a given point is a vertex of the asymmetric subtour elimination polytope. The proposed approach turns upside down the algorithms presented in the literature that first generate every possible vertex and later filter isomorphic vertices. With our approach, we can replicate state-of-the-art results for n<=9 in a tiny fraction of time, and we compute for the first time the exact integrality gap of half-integer vertices of the asymmetric subtour elimination polytope for n=10, 11, 12.

math.OC↗

arXiv2025

Faster Algorithms for the Least-Core value and the Nucleolus in Convex Games

The nucleolus is a central solution concept in cooperative game theory. While its computation is NP-hard in general, it can be computed in polynomial time for convex games; however, the only published polynomial-time algorithm relies on the ellipsoid method. We develop a combinatorial alternative based on reduced games and iterative least-core value computations. Leveraging submodular function minimization and polyhedral structure in a novel way, we obtain a faster combinatorial algorithm for computing the least-core value, improving the oracle complexity by a factor $n^3$ over previous approaches. As a consequence, we obtain a new strongly polynomial-time and combinatorial algorithm for computing the nucleolus in convex games. Preliminary analysis indicates an improved oracle complexity compared to the ellipsoid-based algorithm.

cs.GT↗