paper-with-me

Papers

Autoformalizing Memory Specifications with Agents

2026-04-30 · Jan Ole Ernst, Dmitri Michelangelo Saberi, Derek Christ, Thomas Zimmermann, Rajath Salegame, Suhaas M. Bhat, Stanislav Levental, Thomas Dybdahl Ahle, Matthias Jung arxiv

The primary goal of Design Verification (DV) is to ensure that a proposed chip design implementation (either in code, or physical form) exactly matches its specification and is free of functional errors in order to avoid costly re-designs. Achieving this often demands extensive manual interpretation, translating the specification document into a formal, testable representation. While AI has made progress in DV, current approaches typically focus on narrow, isolated tasks rather than full end-to-end specification compliance of modern chip designs, failing to capture the complexity of real-world verification. Our method automatically formalizes natural language memory chip specifications, for industry relevant Dynamic Random Access Memory (DRAM) standards, into a formal representation called DRAMPyML that can be used for downstream DV tasks like the generation of SystemVerilog assertions, stimulus, and functional coverage. We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities (and new approaches) at hardware autoformalization.

📄 PDF Abstract BibTeX arXiv:2605.00058

Code (0)

등록된 구현이 없습니다.

Similar Papers 제목 키워드 기반

LTL Verification of Memoryful Neural Agents

2025-03-04 · Mehran Hosseini, Alessio Lomuscio, Nicola Paoletti

We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable enviro…

State Space Models

Autoformalizing Euclidean Geometry

2024-05-27 · Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li 외

Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and controllable domain for studying autoformaliz…

Math

Autoformalizing and Simulating Game-Theoretic Scenarios using LLM-augmented Agents

2024-12-11 · Agnieszka Mensfelt, Kostas Stathis, Vince Trencsenyi

Game-theoretic simulations are a versatile tool for exploring interactions of both natural and artificial agents. However, modelling real-world scenarios and developing simulations often require substantial human experti…

Distributed Differentially Private Control Synthesis for Multi-Agent Systems with Metric Temporal Logic Specifications

2022-10-04 · Nasim Baharisangari, Zhe Xu

In this paper, we propose a distributed differentially private receding horizon control (RHC) approach for multi-agent systems (MAS) with metric temporal logic (MTL) specifications. In the MAS considered in this paper, e…

Formalizing Mathematics at Scale

2026-05-28 · Ahmad Rammal, Niket Patel, Fabian Gloeckle, Amaury Hayat 외 arxiv

We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependen…