Steve is an AI career coaching platform that turns a resume and insights from an AI-enabled chat with a user into a personalized skill gap report and upskilling roadmap. The platform suggests a personalized course plan, supports continuous learning, and helps shape the user’s career trajectory. Steve is built around schema-constrained JSON artifacts and a configurable career-tree ontology. The system compares confirmed skills against role-specific requirements, prioritizes gaps (critical/important/beneficial), and translates the analysis into embedding-based queries over the course index. Steve has three personas (Interview Coach, Resume Evaluator, and Career Coach) that provide concise feedback tailored to the user’s goals and context. Steve also supports speech Input/Output (I/O) via Whisper-based speech-to-text and a dual-voice text-to-speech layer, enabling users to talk to Steve. The platform offers flexible adaptability across institutions, enabling them to configure deployments by substituting their own ontologies and course catalogs. Our demo uses STEM trajectories as a case study, but the pipeline is domain-agnostic by design. Users can edit inputs, check speech recognition accuracy, and observe consistent updates, illustrating a reproducible, human-in-the-loop pattern for deploying LLMs in career guidance. Steve is currently in its alpha stage and available for demonstration.

Formally verifying properties of software code has been a highly desirable task, especially with the emergence of LLM-generated code. In the same vein, they provide an interesting avenue for the exploration of formal verification and mechanistic interpretability. Since the introduction of code-specific models, despite their successes in generating code in Lean4 and Isabelle, the task of generalized theorem proving still remains far from being fully solved and will be a benchmark for reasoning capability in LLMs. In this work, we introduce a framework that generates whole proofs in a formal language to be used within systems that utilize the power of built-in tactics and off-the-shelf automated theorem provers. Our framework includes 3 components: generating natural language statements of the code to be verified, an LLM that generates formal proofs for the given statement, and a module employing heuristics for building the final proof. To train the LLM, we employ a 2-stage fine-tuning process, where we first use SFT-based training to enable the model to generate syntactically correct Isabelle code and then RL-based training that encourages the model to generate proofs verified by a theorem prover. We validate our framework using the miniF2F-test benchmark and the Isabelle proof assistant and design a use case to verify the correctness of the AWS S3 bucket access policy code. We also curate a dataset based on the FVEL\textsubscript{\textnormal{ER}} dataset for future training tasks.

An important consideration when deploying realtime applications such as IP Telephony is how to ensure that the network delivers the stringent QoS requirements of these applications. Prior to deployment, assessing whether an enterprise network can handle IP Telephony ensures a successful deployment. A network assessment approach recently introduced in the ExpertNetTMtool suite involves distributing small measurement devices in the network. These devices inject synthetic RTP traffic and collect end-to-end measurements that represent end-to-end call quality. In this approach, the placement of measurement devices impacts the network coverage and accuracy of the analysis. In this paper, we address the problem of how to place such measurement devices in a network to ensure a comprehensive analysis. Specifically, we focus on two issues: first where to place network measurement devices when the network topology is known and second how to estimate the number of such devices in the absence of network topology information. In this paper, we address the first problem by providing two heuristic algorithms for placing measurement devices in a given network. We evaluate these heuristics using synthetic networks. We address the second problem by proposing a technique to estimate the number of measurement devices using the size of a network. To evaluate the performance of our technique, we conducted a study on actual enterprise network topologies. Using our technique, we predicted the number of endpoints based on network size and compared these figures to the number of endpoints placed by the proposed algorithms using the network topology. Our results indicate that the predictions are comparable to the number of endpoints placed using the actual enterprise network topology.