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 20:50] – 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 184: Linia 196:
 A central component is LOGIMINE (Logic Mining and Verification Environment), a research platform supporting the complete pipeline from event logs to formal behavioral analysis. The platform integrates workflow discovery from execution traces, behavioral modeling using workflows and process trees, automatic generation of logical specifications, formal verification through automated theorem proving, process comparison, compliance checking, what-if analysis, and visual analytics for exploring behavioral structures and verification outcomes. A central component is LOGIMINE (Logic Mining and Verification Environment), a research platform supporting the complete pipeline from event logs to formal behavioral analysis. The platform integrates workflow discovery from execution traces, behavioral modeling using workflows and process trees, automatic generation of logical specifications, formal verification through automated theorem proving, process comparison, compliance checking, what-if analysis, and visual analytics for exploring behavioral structures and verification outcomes.
  
-Further technical details are available in the accompanying documentation: [[L3-LOGIMINE.pdf|LOGIMINE IDE Documentation]], [[L3-LOGIMINE2.pdf|LOGIMINE System Documentation]], and [[L3-LOGIMINE-ChurchGame.pdf|Digital Twin Game Documentation]].+Further technical details are available in the accompanying documentation:  
 +[[https://drive.google.com/file/d/1eSAquVISQSJHr_S_DQOnjosV1_gJbgfa/view?usp=drive_link|LOGIMINE IDE Documentation]],  
 +[[https://drive.google.com/file/d/1rdV_XF9o2KEY3QmGiXr-tQRx1P1vFruu/view?usp=drive_link|LOGIMINE System Documentation2]],  
 +and [[https://drive.google.com/file/d/1_mrYHZpD5cEyVDpC4Y9GDG19yIC5Zs9y/view?usp=drive_link|Digital Twin Game Documentation]]. 
 + 
 + 
 +<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 goes beyond conventional benchmark runners. Instead of relying exclusively on fixed collections of existing problems, it enables researchers to construct entire benchmark families with controllable structural and semantic properties. This makes it possible to investigate how particular characteristics of logical specifications influence the performance, scalability, robustness, and reliability of theorem provers, SAT/SMT solvers, and related reasoning engines. 
 + 
 +The platform supports logical problems concerning satisfiability, consistency, implication, redundancy, conflict detection, behavioral constraints, model evolution, modularity, safety and liveness properties, theorem proving, and logical relations between specifications. Generated problems are stored in the TPTP format together with metadata describing their parameters, generation seed, and benchmark configuration. 
 + 
 +**Systematic Benchmark Engineering** 
 + 
 +The central concept implemented by LOFT is **systematic benchmark engineering**. Benchmark problems are generated from parameterized templates rather than collected as unrelated individual examples. Each benchmark family isolates a selected structural or semantic factor and allows the researcher to control its intensity, scale, or distribution. 
 + 
 +This approach supports controlled experimentation. For example, a researcher can investigate how reasoning performance changes when: 
 +  * the number of clauses increases; 
 +  * clause lengths follow fixed, uniform, or probabilistic distributions; 
 +  * the ratio between safety and liveness constraints changes; 
 +  * formulas contain increasing levels of redundancy; 
 +  * selected clauses are removed or modified; 
 +  * logical conflicts are introduced at different depths; 
 +  * implication chains become longer; 
 +  * modules become increasingly coupled; 
 +  * the topology of atom co-occurrence changes; 
 +  * formulas move closer to the SAT/UNSAT phase-transition region. 
 + 
 +Because the benchmark parameters are explicitly recorded, experiments can be repeated using the same seed and configuration. LOFT therefore supports both exploratory experimentation and reproducible comparative studies. 
 + 
 +**Main Capabilities** 
 + 
 +LOFT integrates the following functionality within a single environment: 
 +  * **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; 
 +  * **Controlled randomization** – support for random or fixed seeds, enabling both diversity and reproducibility; 
 +  * **TPTP generation** – creation of benchmark problems in the standard TPTP representation; 
 +  * **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; 
 +  * **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; 
 +  * **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; 
 +  * **Comparative visualization** – interactive charts presenting how prover performance changes with benchmark parameters; 
 +  * **Result persistence** – storage of complete benchmark reports for later inspection and comparison. 
 + 
 +**Benchmark Families** 
 + 
 +The platform currently provides eighteen principal benchmark families, including two variants of Problem 9. Together, these families cover a wide spectrum of structural, semantic, and computational properties. 
 + 
 +**Formula Size and Clause Structure** 
 + 
 +Problems P01–P06 investigate how formula size, clause length, clause distributions, atom-to-clause ratios, and safety/liveness proportions affect reasoning performance. 
 + 
 +The generated specifications may use: 
 +  * fixed clause lengths; 
 +  * several predefined length groups; 
 +  * uniform distributions; 
 +  * Poisson-based distributions; 
 +  * different numbers of atoms; 
 +  * 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. 
 + 
 +**Logical Composition and Relations** 
 + 
 +Problem P07 studies the composition of several independently generated formulas using conjunction or disjunction. The resulting global specification is tested against additional logical requirements. 
 + 
 +Problems P08, P09a, and P09b investigate relations derived from logical squares, including contradiction, subcontrariety, and subalternation. They additionally allow researchers to study structural and semantic asymmetry between formulas of different sizes or different safety/liveness profiles. 
 + 
 +These benchmark families are particularly relevant to research on behavioral specification comparison, logical model relationships, and symbolic analysis of alternative system descriptions. 
 + 
 +**Behavioral Evolution and Redundancy** 
 + 
 +Problem P10 models the evolution of behavioral specifications. A base formula is modified by removing, adding, or replacing selected clauses, and the logical relationship between the original and modified specification is then analyzed. 
 + 
 +Problem P11 investigates controlled redundancy. Additional clauses may be exact duplicates, logically equivalent variants, or clauses related through literal inclusion. The benchmark can test whether redundancy preserves equivalence, strengthens or weakens the specification, or affects joint satisfiability. 
 + 
 +Problem P12 investigates the criticality of missing information by removing selected clauses from a formula. Removal may be random or biased toward safety or liveness constraints. This enables experiments on robustness, incomplete specifications, and the stability of inferred properties. 
 + 
 +**Graph Structure and Modularity** 
 + 
 +Problem P13 controls the topology of the atom co-occurrence graph. Supported structures include: 
 +  * sparse graphs; 
 +  * dense graphs; 
 +  * tree-like structures; 
 +  * modular structures; 
 +  * hub-centered structures. 
 + 
 +This makes it possible to investigate how structural organization of a logical specification affects theorem-proving performance. 
 + 
 +Problem P14 studies modularity and integration of behavioral models. Multiple modules can be generated with independent, weakly coupled, moderately coupled, or strongly coupled atom sets. The resulting global model supports evaluation of locality, global reasoning, and co-satisfiability. 
 + 
 +**Conflict and Inference Depth** 
 + 
 +Problem P15 introduces controlled local inconsistency. Conflicts may be direct, conditional, or behavioral, and their detection may require short or long inference chains. 
 + 
 +Problem P16 investigates implication depth by generating formulas containing chains of increasing length. Benchmarks can test both transitive derivation and contradiction arising from the combination of the first and last elements of the chain. 
 + 
 +These problem families support research on explanation depth, conflict localization, and the computational cost of indirect reasoning. 
 + 
 +**Horn Structure and Phase Transition** 
 + 
 +Problem P17 studies formulas containing different proportions of Horn clauses. Since Horn structure often enables more efficient reasoning, this benchmark family supports controlled investigation of the transition from Horn to non-Horn specifications. 
 + 
 +Problem P18 explores reasoning difficulty near the SAT/UNSAT phase-transition region by controlling the ratio between clauses and atoms. This enables experiments on potentially hard logical instances and comparison of solver behavior under increasing formula density. 
 + 
 +**Supported Provers and Solvers** 
 + 
 +LOFT provides a common execution environment for multiple automated reasoning engines: 
 +  * **Vampire**; 
 +  * **SPASS**; 
 +  * **E Prover**; 
 +  * **iProver**; 
 +  * **Prover9**; 
 +  * **Z3**; 
 +  * **CVC4**; 
 +  * **CVC5**; 
 +  * **Drodi**; 
 +  * **InKreSAT**. 
 + 
 +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: 
 +  * TPTP FOF to CNF for iProver; 
 +  * TPTP to LADR for Prover9; 
 +  * TPTP to SMT-LIB2 for Z3 and CVC5; 
 +  * TPTP to the native modal format used by InKreSAT. 
 + 
 +Converted files are cached to avoid repeated processing of identical benchmark instances. 
 + 
 +**Experimental Workspaces** 
 + 
 +Experiments are organized into separate **workspaces**. Each workspace stores: 
 +  * generator settings; 
 +  * random-seed configuration; 
 +  * prover timeout; 
 +  * generated benchmark problems; 
 +  * converted problem representations; 
 +  * benchmark results; 
 +  * 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. 
 + 
 +Workspaces allow researchers to maintain independent experimental configurations, compare different benchmark campaigns, and preserve complete execution histories. 
 + 
 +**Benchmark Execution and Results** 
 + 
 +The Benchmark module allows the user to select arbitrary combinations of problems and reasoning engines. Each pair consisting of one problem and one prover is treated as an individual benchmark cell. 
 + 
 +Benchmarks are executed asynchronously and may be processed in parallel. Results are streamed to the user interface in real time and saved in persistent JSON reports. 
 + 
 +For each benchmark cell, LOFT records: 
 + 
 +  * reasoning result; 
 +  * real execution time; 
 +  * system CPU time; 
 +  * peak memory consumption; 
 +  * conversion status; 
 +  * timeout or execution error. 
 + 
 +Supported result categories include: 
 + 
 +  * SATISFIABLE; 
 +  * UNSATISFIABLE; 
 +  * UNKNOWN; 
 +  * TIMEOUT; 
 +  * 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. 
 + 
 +**Reproducible Execution Environment** 
 + 
 +LOFT uses Docker and Nix to provide isolated and reproducible execution environments for individual reasoning engines. Each prover is packaged in a dedicated container derived from a shared base image. 
 + 
 +Provers are launched on demand rather than running continuously. This reduces resource consumption and avoids the need for a complex microservice architecture. The backend starts the required container, passes the problem through standard input, collects standard output and error streams, and records resource statistics using GNU Time. 
 + 
 +The use of fixed Nix package revisions strengthens reproducibility by preserving exact software dependencies and prover versions. It also facilitates rebuilding the experimental environment after long periods of time. 
 + 
 +**Web Application and Command-Line Interface** 
 + 
 +LOFT provides both a web-based interface and a command-line interface. 
 + 
 +The web application contains four main workspace views: 
 + 
 +  * **Settings** – configuration of the seed, prover timeout, and syntax checks; 
 +  * **Generator** – generation and management of benchmark problems; 
 +  * **Benchmark** – selection of problems and reasoning engines; 
 +  * **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. 
 + 
 +**System Architecture** 
 + 
 +The platform consists of the following main components: 
 + 
 +  * **Python backend** – implements benchmark generation, workspace management, prover orchestration, result processing, and the Web API; 
 +  * **React frontend** – provides the interactive experiment-management interface; 
 +  * **Problem generators** – implement the P01–P18 benchmark families; 
 +  * **Prover containers** – provide reproducible environments for individual reasoning engines; 
 +  * **Conversion tools** – translate TPTP problems into prover-specific formats; 
 +  * **Benchmark orchestrator** – coordinates parallel execution and real-time result streaming; 
 +  * **Visualization layer** – presents comparative performance charts and detailed reports; 
 +  * **Workspace storage** – preserves experimental configurations, generated problems, and results. 
 + 
 +**Research Scope** 
 + 
 +LOFT provides experimental infrastructure for research in automated theorem proving, SAT/SMT solving, formal verification, behavioral specification analysis, benchmark engineering, and empirical evaluation of reasoning technologies. 
 + 
 +The platform can support studies concerning:
  
 +  * scalability of theorem provers;
 +  * effects of logical structure on reasoning complexity;
 +  * robustness of verification methods;
 +  * comparison of symbolic reasoning paradigms;
 +  * behavioral specification evolution;
 +  * inconsistency and redundancy analysis;
 +  * modular and distributed specifications;
 +  * explainability and conflict localization;
 +  * reproducibility of automated-reasoning experiments.
  
-**LOFT**+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.
  
-Another key component is LOFT (Logical Framework and Testbench), a benchmark generation and experimentation environment for automated reasoning in software engineering. LOFT supports the generation and management of logical verification problems, including satisfiability, consistency, implication, redundancy, conflict detection, behavioral constraints, and theorem-proving tasks. The framework enables the construction of benchmark families with controllable structural properties, facilitating systematic evaluation of theorem provers, SAT/SMT solvers, and logic-based verification methods.+Further technical details are available in the accompanying documentation:  
 +[[https://drive.google.com/file/d/17A9aOnENue4-2rWLOmRKc76gvN97eza1/view?usp=drive_link]].
  
-**ATP Benchmark Collection** 
  
-The infrastructure further includes the ATP Benchmark Collection, a benchmark suite of automated theorem proving problems derived from software-engineering-oriented behavioral verification tasks, and the Logical Problem Catalog, a curated repository of logical verification problems involving behavioral models, workflow specifications, consistency checking, satisfiability analysis, property validation, implication reasoning, and behavioral diagnostics. Together, these platforms and resources provide an experimental foundation for advancing explainable and verifiable behavioral engineering through reproducible evaluation, benchmark-driven research, and prototype validation. 
  
 +<color red>**RE-IDE**</color>
  
-**RE-IDE** 
  
 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.1785610253.txt.gz · ostatnio zmienione: przez admin