首页 > 其他分享 >ECE598HZ: Advanced Topics in Machine Learning

ECE598HZ: Advanced Topics in Machine Learning

时间:2024-09-23 18:13:37浏览次数:11  
标签:training network Topics ECE598HZ feature Machine problem your SAT

ECE598HZ: Advanced Topics in Machine Learning and Formal Methods

Fall 2024

Homework 1

Due Sep 23 11:59pm CT

Typeset your solutions using LATEX, create a single zip file including your solutions (in a single

PDF file), your code, and instructions to run your code. Name your zip file as netid-598-F24 . zip and upload this file through Canvas.

Problem 1: Boolean Satisfiability Problem and DPLL (30pts)

Suppose you are working as an intern in an e-commerce company. You are building a machine learning model to predict whether a customer will buy a product based on a very large datasest with six features: A,B,C,D,E, and F. However, due to computational constraints, your manager asks you to only use three features in your final model.

You have the following information about the features:

• If feature A is selected, theneither feature B or feature C must also be selected.

• Feature C and feature D cannot be selected together.

• If feature E is selected, then feature F must not be selected.

• At least one of features B,C, or D must be selected.

• If feature F is selected, theneither feature A or feature E must also be selected.

1. Formulate this feature selection problem as a Boolean satisfiability problem. (15pts)

2. Use the DPLL algorithm to find a  代 写ECE598HZ: Advanced Topics in Machine Learning  satisfying assignment that represents a valid selection of three features. If such an assignment does not exist, report that the solution does not exist. Show your steps. (15pts)

Problem 2: 4-SAT, 3-SAT, and 2-SAT problems (20pts)

1. A 4-SAT problem inCNF form. has 4 literals in each clause. An example 4-SAT problem is given below:

φ4-SAT  := (x1∨ x2∨ x3∨ x4) Λ (¬x1∨ ¬x2∨ x3∨ ¬x4) Λ (x1∨ ¬x2∨ ¬x3∨ x4)

Convert this 4-SAT problem to an equivalent 3-SAT problem, i.e., find a 3-SAT formula φ3-SAT which is satisfiable if and only if φ4-SAT is satisfiable (hint: you may introduce additional variables) (5 pts)

2. Discussion how to convert any 4-SAT problem to a 3-SAT problem. If the 4-SAT problem has m variables and n clauses, what is the worst-case number of variables and clauses in your converted 3-SAT problem? (5pts)

3. Convert the following 3-SAT problem to a 2-SAT problem. You may have an arbitrary number of clauses in your 2-SAT problem, but don’t introduce any new variables (use x1, x2, x3  and their negations only in each clause). If such a conversion is not possible, provide a proof of the impos- sibility. (10pts)

ϕ3  := (x1V x2V x3)

Problem 3: SMT and Machine Learning Coding Problem (50pts)

You are given a set of points labeled as class +1 or class -1.  Your task is to find a small neural network with ReLU activation that classifies the points correctly.

The network has two input features x1  and x2, one hidden layer with ReLU activation function, and a single output y. Mathematically, it is defined as:

h1 = ReLU(w11 · x1 + w12 · x2 + b1)                          (1)

h2 = ReLU(w21 · x1 + w22 · x2 + b2)                          (2)

y = v1 · h1 + v2 · h2 + c                                            (3)

Here w11 , w12 , w21 , w22 are the weights of the first linear layer, v1 , v2  are the weights of the second linear layer. b1 , b2 are the biases of the first linear layer, and c is the bias of the second linear layer. The network classifies the input as +1 when y > 0, and -1 when y < 0.

You are given two sets of training data points, presented in Table 1 and Table 2.

Point

x1

x2

Label

P1

1

1

+1

P2

1

-1

-1

P3

-1

1

-1

P4

-1

-1

+1

Table 1: Training set 1

In this problem, we will consider solving the neural network using an SMT formulation as well as using a regular machine learning approach (e.g., gradient descent). Complete the following tasks:

1. First, consider only the points P1 and P2 from training set 1.  Write the problem of finding one solution of neural network parameters w11 , w12 , w21 , w22 , v1 , v2 ,c to classify P1 and P2

 

Point

x1

x2

Label

P1

0.1

0.1

+1

P2

0.2

0.1

-1

P3

0.3

0.2

+1

P4

0.4

0.3

-1

P5

-0.1

-0.1

+1

P6

-0.2

-0.1

-1

P7

-0.3

-0.2

+1

P8

-0.4

-0.3

-1

P9

0.5

0.4

+1

P10

-0.5

-0.4

-1

 

Table 2: Training set 2

correctly as an SMT problem. You can use nonlinear functions such as ReLU in your formu- lation. (Hint: think the process of finding neural network parameters that classify P1 and P2 correctly as finding a satisfiable solution of an SMT formula) (10pts)

2. Now consider all points in each training set. Write a Python program to call the SMT solver Z3. For each training set, use Z3 to solve the network parameters such that all points in each training set are classified correctly. Report that no solution exists if Z3 reportsUNSAT for the SMT problem. A program template (z3nn template.py) has been given to you. (15pts)

3. Using any machine learning framework (such as PyTorch), create the neural network defined in this problem (equations (1) to (3)). If you obtained a solution for w11 , w12 , w21 , w22 , v1 , v2 , c in the previous task (Z3 does not report UNSAT), plug these parameters in your network and report the training set accuracy on the corresponding training set. (5pts)

4. Train two networks for the two training sets using regular cross-entropy loss for classifi- cation and optimize the loss with gradient descent (any gradient-based optimizer, such as Adam, can be used). Initialize your neural networks randomly. Tune hyperparameters with your best effort. Plot loss function values vs. the number of optimization iterations. Can the training loss be reduced to 0 for each dataset? Report the training accuracy on the two networks you obtained on the two training sets, respectively. (10pts)

5. Based on your experience when solving tasks 2 and 4, discuss the strengths and weaknesses of solving a neural network using Z3 vs. typical machine learning approaches such as gra- dient descent. (10pts)

For tasks 2,3 and 4, please submit your programs and also a README file containing instructions to run your code. Be sure that you have good instructions.

Resources: First install Z3 in your computer. This is a very quick process. On Linux and MacOS pip  install  z3-solver does it in less than a minute (using a virutal Python environment like

venv or condais suggested.). You can find more instructions about z3 from:

https://github.com/Z3Prover/z3. There is a lot of help available online for installation related issues. Some tutorials that you may find useful are listed below:

• https://ericpony.github.io/z3py-tutorial/guide-examples.htm

• https://github.com/philzook58/z3_tutorial/blob/master/Z3%20Tutorial. ipynb

If you need a tutorial on PyTorch for training neural networks, you can refer to these tutorials:

• https://weiliu2k.github.io/CITS4012/pytorch/nn_oop.html

• https://gist.github.com/santi-pdp/d0e9002afe74db04aa5bbff6d076e8fe

• https://courses.cs.washington.edu/courses/cse446/18wi/sections/section8/ XOR-Pytorch.html

 

标签:training,network,Topics,ECE598HZ,feature,Machine,problem,your,SAT
From: https://www.cnblogs.com/WX-codinghelp/p/18427597

相关文章

  • [HKEY_LOCAL_MACHINE\SYSTEM\ControlSet001\Services\partmgr\Parameters] "SanP
    WindowsRegistryEditorVersion5.00;关闭windowstogo特性[HKEY_LOCAL_MACHINE\SYSTEM\ControlSet001\Control]"PortableOperatingSystem"=dword:00000000 [HKEY_LOCAL_MACHINE\SYSTEM\ControlSet001\Services\partmgr\Parameters]"SanPolicy"=......
  • COMP5328 - Advanced Machine Learning
    COMP5328-AdvancedMachineLearningAssignment1Due:19/09/2024,11:59PMThisassignmentistobecompletedingroupsof3to4students.Itisworth25%ofyourtotalmark.1ObjectiveTheobjectiveofthisassignmentistoimplementNon-negativeMatri......
  • Suspense and Fiber- The Intricate Machinery Behind React&#s Rendering Elegance
    reactfiber是react并发渲染的核心,它使框架能够将任务分解为更小的单元,并优先处理更重要的任务,从而实现更流畅、响应更灵敏的用户界面。当与suspense配合使用时,它允许react“暂停”渲染,在等待数据获取或计算等任务完成时显示后备ui。fiber是一个javascript对象,代表rea......
  • 【USB3.0协议学习】Topic4·USB3.0的Port Connect State Machine和设备枚举
    上一节的文章【USB3.0协议学习】Topic2·USB3.0的LTSSM分析中我们详细分析了USB3.0协议中的链路训练状态机(LTSSM)的各状态和跳转条件,覆盖了所有LTSSM状态。本文我们将从Roothubport和DevicePort的角度讨论其PortConnect状态机。该状态机相比LTSSM,是更高层次的状态机,取决于具体......
  • [设计模式] Cola-StateMachine : 一个轻量实用的Java状态机框架
    1概述:状态机1.0状态机vs工作流在介绍状态机之前,先介绍一个工作流(WorkFlow),初学者通常容易将两个概念混淆。工作流(WorkFlow),大体是指业务过程(整体或者部分)在计算机应用环境下的自动化,是对工作流程及其各操作步骤之间业务规则的描述。在计算机系统中,工作流属于计算机支持的......
  • JVM(Java Virtual Machine,Java 虚拟机)
    JVM(JavaVirtualMachine,Java虚拟机)是Java程序运行的虚拟计算机,它是一个抽象计算机的概念,为Java程序提供了一个与平台无关的执行环境。JVM负责加载Java类文件,执行字节码,并提供运行时环境,包括内存管理、垃圾回收等。JVM主要由四大部分组成:ClassLoader(类加载器):负责加载......
  • 第四届机械制造与智能控制国际学术会议(ICMMIC 2024) 2024 4th International Conferenc
    文章目录一、会议详情二、重要信息三、大会介绍四、出席嘉宾五、征稿主题六、咨询一、会议详情二、重要信息大会官网:https://ais.cn/u/vEbMBz提交检索:EICompendex、IEEEXplore、Scopus会议时间:2024年9月27-29日三、大会介绍2024年第四届机械制造与智能控制国......
  • BISM7255 UML VendWise Solutions Vending Machines
    UML Assignment–Semester2,2024BISM7255AdigitalsolutionforVendWiseSolutionsVending MachinesAssignmentOverviewAssessmentWeight:40%IndividualorGroupwork:Either–yourchoiceMaximumgroupsize:2Due Date:13......
  • 《DNK210使用指南 -CanMV版 V1.0》第二十一章 machine.UART类实验
    第二十一章machine.UART类实验1)实验平台:正点原子DNK210开发板2)章节摘自【正点原子】DNK210使用指南-CanMV版V1.03)购买链接:https://detail.tmall.com/item.htm?&id=7828013987504)全套实验源码+手册+视频下载地址:http://www.openedv.com/docs/boards/k210/ATK-DNK210.html......
  • Nomachine_虚拟桌面_调整虚拟桌面分辨率
    使用虚拟桌面安装基础组件sudoapt-getinstallxserver-xorg-core-hwe-18.04sudoapt-getinstallxserver-xorg-video-dummy-hwe-18.04--fix-missing修改配置文件,以创建一个虚拟桌面vim/usr/share/X11/xorg.conf.d/xorg.conf写入以下内容Section"Monitor"Ide......