Contact Us

Institutional Communications
Bureau of Mines Building, Room 137
Laramie, WY 82071
Phone: (307) 766-2929
Email: cbaldwin@uwyo.edu


Find us on Facebook (Link opens a new window) Find us on Twitter (Link opens a new window)

CEAS Logo

UW Professor, Student Contribute Pages to 2021 AI Index

Artificial intelligence (AI) is one of the major pillars of modern society and the economy, with research teams across the world working to build systems that seem like science fiction today.

So, it can be hard to keep up with what’s happening in AI, especially if you’re not working in the field. That’s where the AI Index comes in. And a University of Wyoming faculty member and student contributed to the 2021 version of the index, which was released March 3. 

Part of the AI Index’s mission is to evaluate the state of the art for solving hard AI problems.

Lars Kotthoff, an assistant professor in the UW Department of Computer Science, and Austin Stephen, a UW senior from Cheyenne majoring in computer science and statistics, performed computational experiments at UW’s Advanced Research Computing Center to do exactly that. Stephen is a Wyoming Research Scholar who has been working in Kotthoff’s lab since 2019.

“One of the classic problems in AI is that of Boolean satisfiability, where we want to find values such that a mathematical formula evaluates to a true statement,” Kotthoff explains. “This is a challenging problem with many practical applications. For example, in chip design, that has been used as a benchmark by the AI community for decades. Our computational experiments, run by Austin, showed how much faster it has become to solve these problems over the years.” 

In logic and computer science, the Boolean satisfiability problem is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values “true” or “false” in such a way that the formula evaluates to “true.” In addition to the computational data, the UW team also contributed a novel methodology for evaluating how well each AI system performs. The methodology was developed in collaboration with researchers in Canada, the Netherlands, Poland and Abu Dhabi, and published at one of the top AI conferences.

“Usually, people only have a look at what system is fastest. This misses subtle, but important nuances that are of interest to AI researchers,” Kotthoff says. “As an analogy, if an employer looks only at the 3.2 GPA of a student, they will miss that the student is actually an ‘A’ student in the subject that is most relevant to their business. Our new methodology is based on a well-known concept in economics, the Shapley value, and allows us to quantify performance in the context of the state of the art.” 

The AI Index gathers, analyzes and visualizes data relating to AI. The results are distilled into annual reports that give an overview of the “state of AI.” The AI Index is based at Stanford University and led by world experts in AI from academia and industry.

“Contributing to the AI Index is an important service to the AI community and beyond, and allows UW to show its strengths and international standing in AI,” Kotthoff says.

To view the relevant pages (72-74) contributed by Kotthoff and Stephen, go to https://aiindex.stanford.edu/wp-content/uploads/2021/03/2021-AI-Index-Report_Master.pdf.

To access the AI Index website, go to https://aiindex.stanford.edu/report/.

SAT Competition Winners on the SC2020 Benchmark Suite
Lars Kotthoff, an assistant professor in the UW Department of Computer Science, and Austin Stephen, a UW senior from Cheyenne majoring in computer science and statistics, contributed a few pages to the 2021 AI Index. This graph, relevant to a task the two solved, shows a comparison of how many problem instances different Boolean satisfiability solvers can solve in a given amount of time. The higher lines mean that more problem instances are solved in the same amount of time, and more problem instances are solved as the given amount of time increases. For example, Kissat-2020 solves about 175 problem instances within 1,000 seconds. (Graph courtesy of Kissat SAT Solver)

Contact Us

Institutional Communications
Bureau of Mines Building, Room 137
Laramie, WY 82071
Phone: (307) 766-2929
Email: cbaldwin@uwyo.edu


Find us on Facebook (Link opens a new window) Find us on Twitter (Link opens a new window)

CEAS Logo