Generative agents, capable of simulating human behavior and collaborating on complex tasks, have the potential to revolutionize the investigation of traffic accidents. In this study, we designed TAA (Traffic Accident Agents), an advanced framework based on extended large language models (LLMs) to digitally model urban accident handling procedures and stakeholder interactions. TAA formalizes the roles, responsibilities, and interactions of all stakeholders through natural language encoding, utilizing this knowledge base to orchestrate its execution workflows. Facilitates trusted agent interactions, generates comprehensive reports, and employs memory mechanisms to plan and optimize subsequent actions. We evaluated TAA performance across multiple versions of ChatGPT, focusing on its capabilities to generate reliable interactions, make context-sensitive decisions, maintain extended dialogues, and produce accurate reports in streamlined accident resolution scenarios. Our analysis included evaluations of token consumption and economic costs to ensure scalability and practicality, with TAA achieving 87.9% effectiveness on the GPT 4omini benchmark. Experimental results demonstrate TAA’s successful execution of urban accident handling workflows with maintained informational consistency. The framework shows broad applicability to accident investigation, reconstruction, and archival documentation. This work pioneers the use of generative agents as collaborative human proxies, offering a transformative pathway to advance the future of traffic accident management and investigation.

Optimization Modulo Theory (OMT) is an important extension of Satisfiability Modulo Theory (SMT), aiming to find models that satisfy constraints while optimizing objective functions. OMT naturally arises in program analysis and formal methods, making OMT solving an important and challenging task. OptiMathSAT is currently the state-of-the-art OMT solver supporting floating-point theories. It incrementally calls an SMT solver to prune the search space step by step until the optimal objective value is found. However, this frequent invocation of the SMT solver is highly inefficient. Therefore, this paper proposes a novel hybrid method consisting of two stages: coarse search and precise search. The coarse search stage quickly finds an approximate optimal model using an optimization search algorithm. The precise search stage then performs an SMT-based binary search starting from the approximate model to find the true optimal model (the OMT solution). Evidently, this hybrid approach reduces computational cost by rapidly shrinking the search space, thereby improving overall solving performance. We evaluated our method on benchmarks derived from SMT-LIB2 and real-world programs. Experimental results show that our method outperforms the current state-of-the-art in both effectiveness and efficiency.