-
General-purpose foundation models for increased autonomy in robot-assisted surgery
Authors:
Samuel Schmidgall,
Ji Woong Kim,
Alan Kuntz,
Ahmed Ezzat Ghazi,
Axel Krieger
Abstract:
The dominant paradigm for end-to-end robot learning focuses on optimizing task-specific objectives that solve a single robotic problem such as picking up an object or reaching a target position. However, recent work on high-capacity models in robotics has shown promise toward being trained on large collections of diverse and task-agnostic datasets of video demonstrations. These models have shown i…
▽ More
The dominant paradigm for end-to-end robot learning focuses on optimizing task-specific objectives that solve a single robotic problem such as picking up an object or reaching a target position. However, recent work on high-capacity models in robotics has shown promise toward being trained on large collections of diverse and task-agnostic datasets of video demonstrations. These models have shown impressive levels of generalization to unseen circumstances, especially as the amount of data and the model complexity scale. Surgical robot systems that learn from data have struggled to advance as quickly as other fields of robot learning for a few reasons: (1) there is a lack of existing large-scale open-source data to train models, (2) it is challenging to model the soft-body deformations that these robots work with during surgery because simulation cannot match the physical and visual complexity of biological tissue, and (3) surgical robots risk harming patients when tested in clinical trials and require more extensive safety measures. This perspective article aims to provide a path toward increasing robot autonomy in robot-assisted surgery through the development of a multi-modal, multi-task, vision-language-action model for surgical robots. Ultimately, we argue that surgical robots are uniquely positioned to benefit from general-purpose models and provide three guiding actions toward increased autonomy in robot-assisted surgery.
△ Less
Submitted 1 January, 2024;
originally announced January 2024.
-
Analyzing Alloy Formulas using an SMT Solver: A Case Study
Authors:
Aboubakr Achraf El Ghazi,
Mana Taghdiri
Abstract:
This paper describes how Yices, a modern SAT Modulo theories solver, can be used to analyze the address-book problem expressed in Alloy, a first-order relational logic with transitive closure. Current analysis of Alloy models - as performed by the Alloy Analyzer - is based on SAT solving and thus, is done only with respect to finitized types. Our analysis generalizes this approach by taking advant…
▽ More
This paper describes how Yices, a modern SAT Modulo theories solver, can be used to analyze the address-book problem expressed in Alloy, a first-order relational logic with transitive closure. Current analysis of Alloy models - as performed by the Alloy Analyzer - is based on SAT solving and thus, is done only with respect to finitized types. Our analysis generalizes this approach by taking advantage of the background theories available in Yices, and avoiding type finitization when possible. Consequently, it is potentially capable of proving that an assertion is a tautology - a capability completely missing from the Alloy Analyzer. This paper also reports on our experimental results that compare the performance of our analysis to that of the Alloy Analyzer for various versions of the address book problem.
△ Less
Submitted 4 May, 2015;
originally announced May 2015.
-
A Dual-Engine for Early Analysis of Critical Systems
Authors:
Aboubakr Achraf El Ghazi,
Ulrich Geilmann,
Mattias Ulbrich,
Mana Taghdiri
Abstract:
This paper presents a framework for modeling, simulating, and checking properties of critical systems based on the Alloy language -- a declarative, first-order, relational logic with a built-in transitive closure operator. The paper introduces a new dual-analysis engine that is capable of providing both counterexamples and proofs. Counterexamples are found fully automatically using an SMT solver,…
▽ More
This paper presents a framework for modeling, simulating, and checking properties of critical systems based on the Alloy language -- a declarative, first-order, relational logic with a built-in transitive closure operator. The paper introduces a new dual-analysis engine that is capable of providing both counterexamples and proofs. Counterexamples are found fully automatically using an SMT solver, which provides a better support for numerical expressions than the existing Alloy Analyzer. Proofs, however, cannot always be found automatically since the Alloy language is undecidable. Our engine offers an economical approach by first trying to prove properties using a fully-automatic, SMT-based analysis, and switches to an interactive theorem prover only if the first attempt fails. This paper also reports on applying our framework to Microsoft's COM standard and the mark-and-sweep garbage collection algorithm.
△ Less
Submitted 4 August, 2014;
originally announced August 2014.
-
Reducing the Complexity of Quantified Formulas via Variable Elimination
Authors:
Aboubakr Achraf El Ghazi,
Mattias Ulbrich,
Mana Taghdiri,
Mihai Herda
Abstract:
We present a general simplification of quantified SMT formulas using variable elimination. The simplification is based on an analysis of the ground terms occurring as arguments in function applications. We use this information to generate a system of set constraints, which is then solved to compute a set of sufficient ground terms for each variable. Universally quantified variables with a finite s…
▽ More
We present a general simplification of quantified SMT formulas using variable elimination. The simplification is based on an analysis of the ground terms occurring as arguments in function applications. We use this information to generate a system of set constraints, which is then solved to compute a set of sufficient ground terms for each variable. Universally quantified variables with a finite set of sufficient ground terms can be eliminated by instantiating them with the computed ground terms. The resulting SMT formula contains potentially fewer quantifiers and thus is potentially easier to solve. We describe how a satisfying model of the resulting formula can be modified to satisfy the original formula. Our experiments show that in many cases, this simplification considerably improves the solving time, and our evaluations using Z3 and CVC4 indicate that the idea is not specific to a particular solver, but can be applied in general.
△ Less
Submitted 4 August, 2014;
originally announced August 2014.
