Chalmers Open Digital Repository

Välkommen till Chalmers öppna digitala arkiv!

Här hittar du:

Studentarbeten utgivna på lärosätet, såväl kandidatarbeten som examensarbeten på grund- och masternivå
Digitala specialsamlingar, som t ex Chalmers modellkammare
Utvalda projektrapporter

Forskningspublikationer, rapporter och avhandlingar hittar du i research.chalmers.se

Enheter i Chalmers ODR

Välj en enhet för att se alla samlingar.

Visar 1 - 2 av 2

Senast inlagda

Oatlog: A high-performance e-graph engine

(2025) Gustafsson, Loke; Magnusson, Erik

Modern software development depends on efficient and reliable optimizing compilers. Traditional compilers apply a sequence of transformations to a single version of a program, with the final result being dependent on the order in which optimizations are applied. However, no single ordering can capture all beneficial optimizations for all programs, a limitation known as the phase ordering problem. This motivates equality saturation, a technique in which the compiler compactly represents many program variants using e-graphs and later extracts the optimal representation using a global profitability heuristic. Equality saturation can improve code quality while simplifying compiler development. Despite these advantages, the adoption of e-graphs in compilers and other domains is limited by performance challenges. These arise from a combinatorial explosion in rewrite possibilities, requiring sophisticated e-graph engines and motivating research into e-graph technology. We introduce Oatlog, an ahead-of-time compiling e-graph engine that significantly outperforms egglog, the currently fastest mainstream e-graph engine. Oatlog achieves speedups over 100x for very small e-graphs, gradually decreasing to a 2x speedup at 106 e-nodes and roughly matches egglog’s performance beyond 107 e-nodes. Oatlog implements a subset of the egglog language and can itself be seen as a compiler from egglog to Rust. As a Rust procedural macro, it complements egglog by focusing on being embeddable within applications rather than on interactive use. We primarily attribute Oatlog’s performance gain to careful programming and performance engineering, but it also benefits from two novel techniques. The first, invariant permutations, exploits commutative relations to optimize queries and reduce memory usage. The second, trie query planning, amortizes index lookups across rewrite rules during e-matching.

AI-driven Player Experience Modeling in Serious Games for Software Engineering

(2025) Dahlberg, Julia

Serious games offer great potential for enhancing software engineering education, yet the use of AI-driven Player Experience Modelling (PEM) remains under-explored in this context. This study investigates how AI-enhanced adaptive features such as difficulty adjustment and dynamic guidance affect player engagement and skill acquisition in the programming game Elara. By comparing AI-driven and traditional versions of the game, the research highlights the benefits of personalized gameplay for supporting learning and motivation. The study demonstrates the promise of AI in tailoring educational experiences and calls for future work to incorporate automated player profiling, larger datasets, and emotional state recognition to further improve adaptive learning in serious games.

Greedy Matching Algorithms in Semi-Streaming Environments for Large Bipartite Graphs

(2025) Djärv, Mattias; Ewing, Gustav

The maximum weight bipartite matching and the related assignment problem become computationally challenging for large-scale graphs due to the high memory and time demands of optimal algorithms. This thesis investigates the viability of greedy matching algorithms within a semi-streaming environment as a practical approach for such scenarios. Several variations of greedy algorithms, including the ℓ-Local Greedy and the ℓ-Local Double Greedy, were implemented and adapted for the semi-streaming model. Their performance, in terms of solution quality, execution time, and memory requirements, were evaluated against a naive random matching algorithm and the optimal solution. Experiments were mainly conducted using generated bipartite graphs of varying sizes, with a focus on how dividing the data into chunks or shards for semi-streaming impacts performance. The results indicate that greedy algorithms, particularly when adapted for semi-streaming, offer nearoptimal solutions with significantly reduced resource consumption. This means the greedy algorithms are viable for large bipartite graphs where optimal algorithms are infeasible. In conclusion, the ℓ-Local Double Greedy algorithm and especially the ℓ-Local Greedy algorithm are robust, scalable, and give near-optimal solutions for maximum weight bipartite matching in a semi-streaming environment, making them highly valuable tools for large-scale data processing and analysis.

Autoformalization for Agda via Fine-tuning Large Language Models

(2025) Huang, Pei

Autoformalization, translating informal mathematical statements into fully formal machine-checkable code, has recently attracted interest thanks to advances in large language models (LLMs). However, progress has been hindered by the lack of highquality parallel corpora pairing natural language with formal code, especially for less-popular systems such as Agda. We address this gap by introducing SMAD (Synthetic Multilanguage Autoformalization Dataset), a 400K 4-to-3 parallel corpus covering four formal languages (Dedukti, Agda, Coq, Lean) and three natural languages (English, French, Swedish), generated via the Informath project. We finetune the open-source Qwen2.5-7B-Instruct model on SMAD and achieve substantial gains: BLEU-4 improves from 32.90 to 76.16, and Agda syntax error rate falls from 98.43 % to under 8 %. We further explore joint training across multiple formal and natural languages, demonstrating that multilingual and multi-formal regimes yield notable improvements in low-resource Agda settings. Our work establishes the first LLM-based Agda autoformalization system and provides systematic insights into model scaling, multilinguality, and dataset construction for future research.

Gauss-Newton Optimizer for 3D Gaussian Splatting Reconstruction

(2025) Alsrup, Tom; Almryd, Rasmus

Recent advancements in neural rendering have enabled highly realistic and efficient representations of 3D scenes from multi-view images. Among these, 3D Gaussian Splatting (3DGS) has emerged as a promising technique that represents scenes using a collection of 3D Gaussian primitives. Since it is a new and active field of research, progress has been made in terms of reducing reconstruction time. We present a new method of optimizing 3DGS by replacing ADAM with a Gauss-Newton (GN) optimizer integrated with the differentiable rasterizer. To save on memory, we introduce custom CUDA kernels that cache radiance and transmittance instead of explicitly storing all gradients. In addition, we introduce a sparsity-aware memory scheme that allows us to store more relevant data while minimizing waste. In each GN iteration, we compute update directions from multiple image subsets using several kernels and aggregate them through a weighted mean. Finally, a line search algorithm is used to determine the optimal update step length based on the sum of squared residuals objective function. Our optimizer converges significantly faster than ADAM per iteration, but comes with a high memory footprint. Due to GN’s computational complexity, it requires more execution time to reach a similar quality level as the original ADAM optimizer. Our GN optimizer demonstrates encouraging results during training, and with further improvements and research detailed in this paper, we believe it could become a strong competitor to ADAM.