Papers for
scientific simulation developers
Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.
E-Ledger improves safe tool use in complex workflows with persistent tracking
Safe, Persistent, and Evolving Agent Harness for Understanding Partially Observable Worlds
Abstract: Large language model agents can invoke tools fluently, but enterprise workflows demand more than selecting the right tools: actions must strictly comply with organizational policies, tool feedback often conceals hidden side effects under partial observability, and long-horizon tasks require persistent state tracking across multiple records. To address these challenges, we introduce E-Ledger, a multi-agent harness for safe and persistent execution. E-Ledger employs a code approval layer that checks every proposed action against policy before execution, and maintains a world ledger of verified hidden rules alongside evidence-backed dynamic state. Because hidden rules are typically unknown a priori, we further propose WorldAbduct, an abductive, world-model-driven harness evolution framework. WorldAbduct diagnoses execution trajectories across four complementary views (state consistency, world-observation gap, policy-gate correctness, and goal judgment) to hypothesize latent rules, and verifies them through targeted abductive interactions before integrating them into the ledger. On the enterprise benchmark World of Workflows, E-Ledger with WorldAbduct improves safe task completion across four LLM backbones, outperforming the strongest evolution baseline by 5--15 percentage points. Experiments in ScienceWorld and DiscoveryWorld further show that abductive harness evolution carries over to scientific environments. Our code is available at https://github.com/HKUST-KnowComp/E-LEDGER-WorldAbduct.
Verifying numerical simulation algorithms early with model checking
Developing a Numerical Algorithm with CIVL Model Checking in the Loop
Abstract: Verifying a numerical algorithm in a large scientific simulation framework is challenging: the framework is too big to model-check, and the unit tests exercise only sampled inputs. We report a case study in which we developed a new cloud-in-cell (CIC) deposition algorithm for Flash-X, a large-scale multiphysics simulation framework, keeping the CIVL model checker in the development loop. Rather than verify the algorithm within Flash-X's hefty infrastructure, we extract only the interfaces that the algorithm needs into a small, self-contained C model, which abstracts away implementation details of the Flash-X infrastructure that are unrelated to the new algorithm. The new algorithm is then built and checked within this C model. The CIVL model checker enables verification of the required physical properties of the CIC deposition algorithm using symbolic values for the particle positions. It proves two physical properties---mass conservation and the deposition location---for the continuum of admissible positions in the simulation domain. CIVL also verifies the algorithm's memory safety and freedom from MPI deadlocks and data race conditions over all rank distributions within specified bounds. Writing the verifying properties first and continuously checking them at each stage of the bottom-up prototyping workflow turned CIVL into a design guardrail that greatly increased confidence in the extended algorithm. During our case study, CIVL surfaced a concurrency defect in the algorithm that our random-seed-based tests failed to exercise. This paper shows our workflow, with the goal of helping readers understand its benefits, cost, and tradeoffs compared with testing.