Radosław Klimek

Narzędzia użytkownika

Narzędzia witryny

opus31

Różnice

Różnice między wybraną wersją a wersją aktualną.

Odnośnik do tego porównania

Poprzednia rewizja po obu stronachPoprzednia wersja
Nowa wersja		Poprzednia wersja
opus31 [2026/08/01 21:28] – adminopus31 [2026/09/05 22:04] (aktualna) – admin
Linia 52: Linia 52:
 [Kli 26d] Radoslaw Klimek "AI-Assisted Behavioural Modelling from Logical Squares".  [Kli 26d] Radoslaw Klimek "AI-Assisted Behavioural Modelling from Logical Squares". 
 Title changed to "Reasoning Scaffolds for AI-Assisted Behavioural Modelling: A Logical-Square Instantiation".  Title changed to "Reasoning Scaffolds for AI-Assisted Behavioural Modelling: A Logical-Square Instantiation". 
-Available: https://drive.google.com/file/d/13UpfESRf0Lc_BKVmmwIeuiqYNuT2GVdk/view?usp=drive_link. +Available: https://drive.google.com/file/d/1NfuY7yZas993QiVlwNq-sPOXHCtUF-h5/view?usp=sharing. 
 <color #CC6600>**ACCEPTED**</color> <color #CC6600>**ACCEPTED**</color>
 Conference paper, MODELS 2026 (Rank A, 140 MNiSW points).  Conference paper, MODELS 2026 (Rank A, 140 MNiSW points). 
 Acceptance notification: https://drive.google.com/file/d/1ZCM-jHR01vMIH-sOkXksY8ikYh4AcmxU/view?usp=drive_link. Acceptance notification: https://drive.google.com/file/d/1ZCM-jHR01vMIH-sOkXksY8ikYh4AcmxU/view?usp=drive_link.
 +List of accepted papers: https://conf.researchr.org/track/models-2026/models-2026-nier#event-overview
  
  
Linia 67: Linia 68:
 Execution Logs: The Dead-End Phenomenon".  Execution Logs: The Dead-End Phenomenon". 
 Title changed to "Dead-End Ratio: A Behavioral Model Quality Metric for Constraint-Aware Runtime Verification". Title changed to "Dead-End Ratio: A Behavioral Model Quality Metric for Constraint-Aware Runtime Verification".
-Available at: https://drive.google.com/file/d/1iGBrCVeVksMM0Q756ZMEzfaKy9vDM6NU/view?usp=drive_link. +Available at: https://drive.google.com/file/d/1ZaSoLkqn521gbJKhuSs_rruhXlYtDe2A/view?usp=sharing. 
-Workshop Flagship conference paper, Core Rank A*, 200 pkt MNiSW, under review.+<color #CC6600>**ACCEPTED**</color> 
 +Warokshop paper at ASE 2026 (ASE is a flagship conference Core Rank A*, 200 MNiSW points).
  
  
Linia 80: Linia 82:
 Acceptance notification: https://drive.google.com/file/d/1jR-GT5LYMa7f6Vnon_D183MkQAcbwfih/view?usp=drive_link. Acceptance notification: https://drive.google.com/file/d/1jR-GT5LYMa7f6Vnon_D183MkQAcbwfih/view?usp=drive_link.
 See conference program: https://conf.researchr.org/track/ase-2026/ase-2026-nier See conference program: https://conf.researchr.org/track/ase-2026/ase-2026-nier
 +
 +
 +[Kli 26f] Radoslaw Klimek „Prompt-to-Feature Attribution for Explainable LLM-Based Software Generation”. 
 +Available at: https://drive.google.com/file/d/1erB_Iz6Kcymm10nw3Lb4TPwN-n1G7jPY/view?usp=sharing.
 +<color #CC6600>**ACCEPTED**</color>
 +Workshop paper at ASE 2026 (ASE is a flagship conference Core Rank A*, 200 MNiSW points).
 +
  
 [Kli 26] Radoslaw Klimek "Toward Defensible System Behavior in AI-Assisted Software Engineering".  [Kli 26] Radoslaw Klimek "Toward Defensible System Behavior in AI-Assisted Software Engineering". 
 Title changed to "Toward Defensible System Behavior for AI-Generated Software Artifacts" Title changed to "Toward Defensible System Behavior for AI-Generated Software Artifacts"
-Available at: https://drive.google.com/file/d/1Siu6l0XGr0qsdpUewYlFhHhhwRjn_qIo/view?usp=drive_link. +Available at: https://drive.google.com/file/d/1WEZGiLEQTk2CVMqgtl0_vYGFaX0pkhX-/view?usp=sharing. 
-Workshop Flagship conference paper, Rank A*, 200 pkt  pkt MNiSW, under review.+<color #CC6600>**ACCEPTED**</color> 
 +Workshop paper at ASE 2026, (ASE is a flagship conference, Rank A*, 200 pkt  pkt MNiSW). 
 +List of accepted papers: https://conf.researchr.org/home/ase-2026/rase-2026#event-overview
  
 [Klo Kli 26] Michał Klos, Radoslaw Klimek "Learning System Behavior from Logs: Graph-Based Anomaly [Klo Kli 26] Michał Klos, Radoslaw Klimek "Learning System Behavior from Logs: Graph-Based Anomaly
Linia 103: Linia 114:
 [Kli 26c] Radoslaw Klimek "A Workflow-Based LLM Assistant for Iterative and Verified Requirements Engineering".  [Kli 26c] Radoslaw Klimek "A Workflow-Based LLM Assistant for Iterative and Verified Requirements Engineering". 
 Title changed to: "A Workflow-Driven Multi-Agent Architecture for Requirements Engineering". Title changed to: "A Workflow-Driven Multi-Agent Architecture for Requirements Engineering".
-Available at: https://drive.google.com/file/d/16SyfChWHyUOVj-OqM9Heznidq3ytD_7R/view?usp=drive_link. +Available at: https://drive.google.com/file/d/1B_g15sM43HLliKHjzsyioi1HL0dYRXx4/view?usp=sharing. 
-Workshop Flagship conference paper, Rank A*, 200 pkt  pkt MNiSW, under review.+<color #CC6600>**ACCEPTED**</color> 
 +Workshop paper at ASE 2026, (ASE is a flagship conference, Rank A*, 200 pkt  pkt MNiSW).
  
  
Linia 123: Linia 135:
  
  
-<color #663399>**LOGIMINE**</color>+<color red>**LOGIMINE**</color>
  
 LOGIMINE ('''Log'''ic '''Mine'''ing and Verification Environment) is a research platform implementing the concept of '''Logic Mining''', an approach that combines process mining, formal methods, automated theorem proving, and AI-assisted software engineering within a unified behavioral reasoning environment. The central idea is to transform process execution data into formal logical representations that can be automatically analyzed, verified, compared, and explained using mature reasoning technologies. LOGIMINE ('''Log'''ic '''Mine'''ing and Verification Environment) is a research platform implementing the concept of '''Logic Mining''', an approach that combines process mining, formal methods, automated theorem proving, and AI-assisted software engineering within a unified behavioral reasoning environment. The central idea is to transform process execution data into formal logical representations that can be automatically analyzed, verified, compared, and explained using mature reasoning technologies.
Linia 190: Linia 202:
  
  
-<color #663399>**LOFT**</color>+<color red>**LOFT**</color>
  
 **LOFT (Logical Framework and Testbench)** is a research platform for systematic benchmark engineering and experimental evaluation of automated reasoning methods. The platform supports the generation, management, execution, and analysis of logical verification problems used in software engineering, formal verification, behavioral reasoning, and automated theorem proving. **LOFT (Logical Framework and Testbench)** is a research platform for systematic benchmark engineering and experimental evaluation of automated reasoning methods. The platform supports the generation, management, execution, and analysis of logical verification problems used in software engineering, formal verification, behavioral reasoning, and automated theorem proving.
Linia 219: Linia 231:
  
 LOFT integrates the following functionality within a single environment: LOFT integrates the following functionality within a single environment:
-* **Parameterized problem generation** – construction of logical benchmark families from configurable generators; +  * **Parameterized problem generation** – construction of logical benchmark families from configurable generators; 
-* **Preset management** – use of predefined configurations such as short, medium, long, weak, strong, or domain-specific benchmark variants; +  * **Preset management** – use of predefined configurations such as short, medium, long, weak, strong, or domain-specific benchmark variants; 
-* **Controlled randomization** – support for random or fixed seeds, enabling both diversity and reproducibility; +  * **Controlled randomization** – support for random or fixed seeds, enabling both diversity and reproducibility; 
-* **TPTP generation** – creation of benchmark problems in the standard TPTP representation; +  * **TPTP generation** – creation of benchmark problems in the standard TPTP representation; 
-* **Syntax checking** – optional validation of generated TPTP files before benchmark execution; +  * **Syntax checking** – optional validation of generated TPTP files before benchmark execution; 
-* **Workspace management** – organization of problems, settings, converted files, and results into separate experimental workspaces; +  * **Workspace management** – organization of problems, settings, converted files, and results into separate experimental workspaces; 
-* **Multi-prover orchestration** – parallel execution of multiple theorem provers and solvers on selected benchmark collections; +  * **Multi-prover orchestration** – parallel execution of multiple theorem provers and solvers on selected benchmark collections; 
-* **Format conversion** – automatic conversion of TPTP problems into formats required by individual reasoning engines; +  * **Format conversion** – automatic conversion of TPTP problems into formats required by individual reasoning engines; 
-* **Result streaming** – real-time delivery of benchmark results through WebSocket communication; +  * **Result streaming** – real-time delivery of benchmark results through WebSocket communication; 
-* **Performance measurement** – recording of real execution time, system time, peak memory use, and solver status; +  * **Performance measurement** – recording of real execution time, system time, peak memory use, and solver status; 
-* **Comparative visualization** – interactive charts presenting how prover performance changes with benchmark parameters; +  * **Comparative visualization** – interactive charts presenting how prover performance changes with benchmark parameters; 
-* **Result persistence** – storage of complete benchmark reports for later inspection and comparison.+  * **Result persistence** – storage of complete benchmark reports for later inspection and comparison.
  
 **Benchmark Families** **Benchmark Families**
Linia 241: Linia 253:
  
 The generated specifications may use: The generated specifications may use:
-* fixed clause lengths; +  * fixed clause lengths; 
-* several predefined length groups; +  * several predefined length groups; 
-* uniform distributions; +  * uniform distributions; 
-* Poisson-based distributions; +  * Poisson-based distributions; 
-* different numbers of atoms; +  * different numbers of atoms; 
-* controlled proportions of safety and liveness clauses.+  * controlled proportions of safety and liveness clauses.
  
 These families support systematic scalability studies and analysis of how basic syntactic properties influence execution time and memory consumption. These families support systematic scalability studies and analysis of how basic syntactic properties influence execution time and memory consumption.
Linia 269: Linia 281:
  
 Problem P13 controls the topology of the atom co-occurrence graph. Supported structures include: Problem P13 controls the topology of the atom co-occurrence graph. Supported structures include:
-* sparse graphs; +  * sparse graphs; 
-* dense graphs; +  * dense graphs; 
-* tree-like structures; +  * tree-like structures; 
-* modular structures; +  * modular structures; 
-* hub-centered structures.+  * hub-centered structures.
  
 This makes it possible to investigate how structural organization of a logical specification affects theorem-proving performance. This makes it possible to investigate how structural organization of a logical specification affects theorem-proving performance.
Linia 296: Linia 308:
  
 LOFT provides a common execution environment for multiple automated reasoning engines: LOFT provides a common execution environment for multiple automated reasoning engines:
-* **Vampire**; +  * **Vampire**; 
-* **SPASS**; +  * **SPASS**; 
-* **E Prover**; +  * **E Prover**; 
-* **iProver**; +  * **iProver**; 
-* **Prover9**; +  * **Prover9**; 
-* **Z3**; +  * **Z3**; 
-* **CVC4**; +  * **CVC4**; 
-* **CVC5**; +  * **CVC5**; 
-* **Drodi**; +  * **Drodi**; 
-* **InKreSAT**.+  * **InKreSAT**.
  
 These tools differ in accepted input formats, reasoning paradigms, and implementation strategies. LOFT hides much of this heterogeneity behind a common benchmark interface. These tools differ in accepted input formats, reasoning paradigms, and implementation strategies. LOFT hides much of this heterogeneity behind a common benchmark interface.
  
 Problems are generated primarily in the TPTP format. Where necessary, the platform automatically invokes dedicated converters: Problems are generated primarily in the TPTP format. Where necessary, the platform automatically invokes dedicated converters:
-* TPTP FOF to CNF for iProver; +  * TPTP FOF to CNF for iProver; 
-* TPTP to LADR for Prover9; +  * TPTP to LADR for Prover9; 
-* TPTP to SMT-LIB2 for Z3 and CVC5; +  * TPTP to SMT-LIB2 for Z3 and CVC5; 
-* TPTP to the native modal format used by InKreSAT.+  * TPTP to the native modal format used by InKreSAT.
  
 Converted files are cached to avoid repeated processing of identical benchmark instances. Converted files are cached to avoid repeated processing of identical benchmark instances.
Linia 320: Linia 332:
  
 Experiments are organized into separate **workspaces**. Each workspace stores: Experiments are organized into separate **workspaces**. Each workspace stores:
-* generator settings; +  * generator settings; 
-* random-seed configuration; +  * random-seed configuration; 
-* prover timeout; +  * prover timeout; 
-* generated benchmark problems; +  * generated benchmark problems; 
-* converted problem representations; +  * converted problem representations; 
-* benchmark results; +  * benchmark results; 
-* execution statistics.+  * execution statistics.
  
 A fixed seed can be used to reproduce exactly the same benchmark families, while a random seed supports exploratory generation of new instances. A fixed seed can be used to reproduce exactly the same benchmark families, while a random seed supports exploratory generation of new instances.
Linia 340: Linia 352:
 For each benchmark cell, LOFT records: For each benchmark cell, LOFT records:
  
-* reasoning result; +  * reasoning result; 
-* real execution time; +  * real execution time; 
-* system CPU time; +  * system CPU time; 
-* peak memory consumption; +  * peak memory consumption; 
-* conversion status; +  * conversion status; 
-* timeout or execution error.+  * timeout or execution error.
  
 Supported result categories include: Supported result categories include:
  
-* SATISFIABLE; +  * SATISFIABLE; 
-* UNSATISFIABLE; +  * UNSATISFIABLE; 
-* UNKNOWN; +  * UNKNOWN; 
-* TIMEOUT; +  * TIMEOUT; 
-* UNCONVERTED.+  * UNCONVERTED.
  
 The result interface presents both detailed tables and interactive charts. Researchers can select a benchmark parameter for the horizontal axis and compare execution time or memory consumption across multiple provers. This is particularly useful for scalability analysis and identification of solver-specific performance patterns. The result interface presents both detailed tables and interactive charts. Researchers can select a benchmark parameter for the horizontal axis and compare execution time or memory consumption across multiple provers. This is particularly useful for scalability analysis and identification of solver-specific performance patterns.
Linia 371: Linia 383:
 The web application contains four main workspace views: The web application contains four main workspace views:
  
-* **Settings** – configuration of the seed, prover timeout, and syntax checks; +  * **Settings** – configuration of the seed, prover timeout, and syntax checks; 
-* **Generator** – generation and management of benchmark problems; +  * **Generator** – generation and management of benchmark problems; 
-* **Benchmark** – selection of problems and reasoning engines; +  * **Benchmark** – selection of problems and reasoning engines; 
-* **Results** – inspection, comparison, visualization, renaming, and deletion of benchmark reports.+  * **Results** – inspection, comparison, visualization, renaming, and deletion of benchmark reports.
  
 The command-line interface supports rapid testing, automated scripts, and integration with external experimental workflows. Core operations include problem generation, syntax checking, and benchmark execution. The command-line interface supports rapid testing, automated scripts, and integration with external experimental workflows. Core operations include problem generation, syntax checking, and benchmark execution.
Linia 382: Linia 394:
 The platform consists of the following main components: The platform consists of the following main components:
  
-* **Python backend** – implements benchmark generation, workspace management, prover orchestration, result processing, and the Web API; +  * **Python backend** – implements benchmark generation, workspace management, prover orchestration, result processing, and the Web API; 
-* **React frontend** – provides the interactive experiment-management interface; +  * **React frontend** – provides the interactive experiment-management interface; 
-* **Problem generators** – implement the P01–P18 benchmark families; +  * **Problem generators** – implement the P01–P18 benchmark families; 
-* **Prover containers** – provide reproducible environments for individual reasoning engines; +  * **Prover containers** – provide reproducible environments for individual reasoning engines; 
-* **Conversion tools** – translate TPTP problems into prover-specific formats; +  * **Conversion tools** – translate TPTP problems into prover-specific formats; 
-* **Benchmark orchestrator** – coordinates parallel execution and real-time result streaming; +  * **Benchmark orchestrator** – coordinates parallel execution and real-time result streaming; 
-* **Visualization layer** – presents comparative performance charts and detailed reports; +  * **Visualization layer** – presents comparative performance charts and detailed reports; 
-* **Workspace storage** – preserves experimental configurations, generated problems, and results.+  * **Workspace storage** – preserves experimental configurations, generated problems, and results.
  
 **Research Scope** **Research Scope**
Linia 397: Linia 409:
 The platform can support studies concerning: The platform can support studies concerning:
  
-* scalability of theorem provers; +  * scalability of theorem provers; 
-* effects of logical structure on reasoning complexity; +  * effects of logical structure on reasoning complexity; 
-* robustness of verification methods; +  * robustness of verification methods; 
-* comparison of symbolic reasoning paradigms; +  * comparison of symbolic reasoning paradigms; 
-* behavioral specification evolution; +  * behavioral specification evolution; 
-* inconsistency and redundancy analysis; +  * inconsistency and redundancy analysis; 
-* modular and distributed specifications; +  * modular and distributed specifications; 
-* explainability and conflict localization; +  * explainability and conflict localization; 
-* reproducibility of automated-reasoning experiments.+  * reproducibility of automated-reasoning experiments.
  
 By combining controlled benchmark generation, heterogeneous solver execution, reproducible infrastructure, and comparative analytics, LOFT provides a unified environment for systematic empirical research on logical reasoning methods. By combining controlled benchmark generation, heterogeneous solver execution, reproducible infrastructure, and comparative analytics, LOFT provides a unified environment for systematic empirical research on logical reasoning methods.
Linia 414: Linia 426:
  
  
-**RE-IDE**+<color red>**RE-IDE**</color> 
  
 Workflow-driven requirements engineering environment supporting structured model generation, clarification, validation, and preparation of artifacts for formal verification. Workflow-driven requirements engineering environment supporting structured model generation, clarification, validation, and preparation of artifacts for formal verification.
opus31.1785612498.txt.gz · ostatnio zmienione: przez admin